Dependent types in OCaml

13
votes

There's a lot of information about dependent types in Haskell and Scala. For OCaml, not so much. Is anyone skilled enough to provide a coding example on how to achieve this in OCaml (if it's possible at all)? There is of course (the abandoned) Dependent ML, but it seems not possible to incorporate such stuff in "regular" OCaml code.

Basically, what I want to do is to remove code like assert(n > 0) and check it at compile time.

EDIT

As a side note, it's worth mentioning the OCaml Hybrid Contract Checking branch, that could fill some of the needs of a dependent type system. Instead of assert(n > 0) you would then write a contract:

contract f = {x : x > 0} -> int
let f x = x + 1
let dummy_variable = f (-1) (* Won't compile *)

Edit 2: For anyone reading this, I think F* is an interesting ML-like language with dependent types.

1
typesocaml
May I ask where is this "lot of information about dependent types in Haskell and Scala"? Despite having a reasonable overview of the Haskell community, I don't know what you are referring to. (I would definitely consider the UPenn work on Dependently-Typed Haskell as relevant, but that's extremely researchy rather than practical, and maybe not "a lot" in volume). I have no idea what you're thinking of for Scala -- except maybe the relation to path-dependent types? – gasche
Ehm, on stackoverflow, I was thinking. Maybe I was fooled by Scalas path-dependent types. – Olle Härstedt

1 Answers

12
votes

A reference link is Oleg's lightweight dependent typing pages, with examples (in OCaml or that you can translate to OCaml) of dependent-like techniques used in ML languages. His paper on Lighweight static capabilities (PDF) with Chung-chieh Shan in 2007 is especially relevant.

Edit: Since version 4.00 (released after the document above was written), OCaml has GADTs, which allow to streamline a few techniques for refined static information (previously relying on phantom type techniques), in particular the "singleton types" pattern demonstrated in Omega. It has been shown that they're not essential to get strong typeful programming, but they may still be used by a variety of examples found in the wild.