Are there something like Haskell type families in Ocaml?

Learning
1

I was studying the possibilities of GADTs to emulate dependently typed language features. I basically found that Ocaml and Haskell have rather similar possibilities to define types indexed by types (i.e. GADTs).

The singleton types are rather equivalent as well. I.e. I can have a runtime representation of a type to make runtime decisions.

However I have found no equivalent of Haskell’s type families in Ocaml. My question: Is there a way to use singleton types to do type computation in Ocaml?

Thanks for any hint.

2

Good interesting question!)

In Haskell type families are type level functions - function from types to types.
In Ocaml we keep types in distinct modules: Your_module.t , Another_module.t, etc. And Ocaml has functions from modules to modules. It is called functors. Functors have enough expressive power. They can be recursive, generative or applicative, first-class…

1 Like
3

Haskell has a Functor typeclass. With one commonly used function, fmap; it maps functions, is the way they put it. So for example, using their Maybe data type, like OCaml’s option – Maybe is already an instance of Functor - I can “map” +1 to int option values.

fmap ((+) 1) (Just 1) --> Just 2
fmap ((+) 1) Nothing --> Nothing

Of course this is classic Haskell, while type families are an extension, and obviously don’t serve the same purpose. There’s obviously some parallel between the Haskell and OCaml Functor, though limited by the differences between typeclass and module. [edit - I see that here, for my example, the same functionality is simply supplied by OCaml ad hoc in Option.map. ]

4

I do not yet see, how functors have the same expressive power as type families. E.g. I have tried to express the following Haskell code snippet in Ocaml and I did not succeed.

data Color :: * where
    R :: Color
    B :: Color

data Nat = Z | S Nat

type family Incr (c :: Color) (x :: Nat) :: Nat where
    Incr R x = x
    Incr B x = S x

You can find the complete Haskell code here

Can you express this little Haskell snippet in Ocaml?

5

OCaml does not support kinds or type families. Sometimes GADTs are enough. Typically, they are enough for Red Black trees. In fact, they should be enough for translating the code that you linked since the Incr family does not seem really useful (it is used to merge two constructors but it requires to introduce two singleton types).

6

I don’t get it :smiley: image

7

Type Families are implemented in GHC with type equality proofs which is essentially what GADTs are. Simple use cases for Type Families can probably be encoded in OCaml with a clever use of GADTs.

1 Like
8

Hi, can you please post text, instead of screenshots? Text is more accessible. Thanks.

1 Like
9

sure ^^

type color = R | B
type nat   = Z | S of nat

let incr c x = match c with
  | R -> x
  | B -> S x
;;

typechecks fine:

type color = R | B
type nat = Z | S of nat
val incr : color -> nat -> nat = <fun>
10

Haskell has the convention that uppercase identifier is a type constructor, so Incr is actually mean to be used at type level (function & pattern match at type level!), while the incr you defined is not a type level function in OCaml.

The rationale of type level function is that the GHC type checker can use this to reduce usually very complex type expressions, and its usage is always involved with GADT.

While gaga is right, “a clever use” probably means writing human incomprehensible type expressions, abusing the type checker as a theorem prover, which I’m personally against.

Playing with type expressions usually won’t make the programming language having more expressive power (in terms of Turing completeness), it only extends the expressiveness of type system.

2 Likes