I am trying to get my head around GADTs and have been working through the examples in Real World Ocaml.
As a learning exercise I thought I would try for a “simpler” example so decided to build a simple minded fixed length vector. The code for which is below.
Having got versions of head and tail working I was feeling good. But then I tried to build a function that would convert a list to a vector of the correct length. Something like:
let rec makevec (type a n) (x: a list) : (a, n) vec =
match x with
| [] -> Nil
| y::ys -> C(y, makevec ys)
But not matter what I try I cannot get this function to compile. I suspect I am running into the problem described in Real World Ocaml in the section entitled “GADTs, Locally Abstract Types and Polymorphic Recursion” but dont understand how to “fix it”.
What am I doing wrong or not understanding.
Guidance or help gratefully accepted ??
(*Natural numbers*)
type zero = Z
type 'n succ = S of 'n
(* A gadt that defines a fixed length vector - its length is part of the type definition *)
type ('a, 'n) vec =
| Nil :('a, zero) vec
| C: 'a * ('a, 'n)vec -> ('a, 'n succ)vec
(* Poor definition of head as it permits an empty vector*)
let rec vec_head_poor (type a n)(v: (a, n)vec): a =
match v with
| Nil -> invalid_arg ("cannot take hd of Nil")
| C(x, _) -> x
(* | _ -> invalid_arg("") *)
(*Better defn of head as it excludes the possibility of the empty list as a parameter*)
let rec vec_head (type a n)(v: (a, n succ)vec): a =
match v with
(* | Nil -> invalid_arg ("cannot take hd of Nil") *)
| C(x, _) -> x
(* | _ -> invalid_arg("") *)
(*Now we need a function that joins together two vectors only if they are of the same length*)
let rec vec_tail (type a n) (v: (a, n succ )vec): (a, n) vec =
match v with
| C(_, vv) -> vv
The issue is that your function makevec has a type that is dependent on the runtime value of x, which isn’t consistent with the type you’re trying to give it:
val makevec: 'a 'n. 'a list -> ('a,'n) vec
I.e forall types 'a, 'n, produce a function 'a list -> ('a, 'n) vec
However in reality, the quantification over 'n doesn’t hold in general - for any particular list, the function will only be able to return exactly one type for 'n.
You can get around this and write your makevec function by hiding the 'n parameter using an existential type:
type zero = Z
type 'n succ = S of 'n
(* A gadt that defines a fixed length vector - its length is part of the type definition *)
type ('a, 'n) vec =
| Nil :('a, zero) vec
| C: 'a * ('a, 'n) vec -> ('a, 'n succ) vec
type 'a wrapped_vec = Wrap : ('a, 'n) vec -> 'a wrapped_vec
let rec makevec (x: 'a list) : 'a wrapped_vec =
match x with
| [] -> Wrap Nil
| y::ys ->
let Wrap vec = makevec ys in
Wrap (C(y, vec))
Because the type of the result returned by your original makevec ('a, 'n) vec depends on the length of it’s input xs: 'a list which is a property that is not tracked by the type system (i.e both [] : 'a list and [x;y] : 'a list have the same types despite having different lengths) it is not possible to assign your implementation of makevec a valid type in OCaml (because w.r.t the type system, makevec [] and makevec [x;y] should have the same type).
In order to capture the semantics of your original definition we can “wrap” the output of your makevec function to hide the runtime dependent type behind an existential type, hence:
type 'a wrapped_vec = Wrap : ('a, 'n) vec -> 'a wrapped_vec
and giving makevec the type:
val makevec: 'a list -> 'a wrapped_vec
Notice now that makevec doesn’t directly return a ('a,'n) vec but returns a wrapped 'a wrapped_vec which hides the runtime dependent type.
Now, finally w.r.t the statement you had a query about. That statement is equivalent to:
match makevec ys with
| Wrap vec -> Wrap (C(y, vec))
The reason for it is that because we modified makevec to return a wrapped vec ('a wrapped_vec) rather than a ('a, 'n) vec, we first unwrap the result of the recursive call to retrieve the inner ('a, 'n) vec so that we can construct the cons case.
Thanks for your explanation of the let statement.
I certainly did not see it being equivalent to:
match makevec ys with
| Wrap vec -> Wrap (C(y, vec))
I have 2 more dumb questions for you:
which type is the existential - I think of an existential type as as an interface or super type which can hold a lot of more specialized types by throwing away some of the specialized structure. So I would conclude that Wrap is the existential type.
Can I unwrap a Wrap - or is that simply the original problem back again
I’m not 100% sure about the precise terminology, but I believe that the existential type is the argument to Wrap:
type 'a wrapped_vec = Wrap : ('a, 'n) vec -> 'a wrapped_vec
(* ^^^^^^^^^ *)
The reason it is an existential type is because when you have a value of type 'a wrapped_vec, you know that there exists a value of type ('a, 'n) vec for some choice of 'n, but you don’t have access to the exact type (because there’s nothing in the type 'a wrapped_vec that will tell you what 'n should be).
For the same reason, there’s no way to unwrap a wrapped type to obtain a ('a, 'n) vec at the top level, because there’s no way for OCaml to know statically at compile time what 'n should be. You can unwrap the Wrap temporarily as I did in the makevec function, but the type can not escape it’s scope.
So I see that the challenge of building ('a, 'n)vec from a list actually boils down to constructing the correct natural number type ('n in my language with the right number of succ applications) from an actual natural number value which is the length of the list.