Implementing map for a size-indexed vector using GADTs

Learning
#1

I defined the vector GADT as the following:

module Vector = struct
  type ('a, 'size) t  =
    | []  : ('a, z) t
    | (::) : 'a * ('a, 'size) t ->  
        ('a, 'size s) t
end

I tried implementing map like the following:

  let rec map (type size num_elem_to_add) ~(f:'a -> 'b)  (vector: ('a, size) t) : ('b, size) t =

    match vector with
    | x::xs -> f x :: map ~f vector
    | [] -> []

However, I am getting the compiling error:

This expression has type 'a but an expression was expected of type  ('b, $0) t
The type constructor $0 would escape its scope

How would I be able to fix this?

#2 
let rec map : type size. f:('a -> 'b) -> ('a, size) t -> ('b, size) t = fun ~f vector ->
    match vector with
    | x::xs -> f x :: (map ~f xs)
    | [] -> []
#3

Why does that work? It seems very similar to what I did.

#4

The short version is that you need an explicit universal annotation when defining a recursive function over GADTs.
And the syntax

let rec map: type size.
  f:('a -> 'b) -> ('a, size) t -> ('b, size) t = ...

makes the type size both locally abstract and universally quantified.

More precisely, those explicit universal quantification annotations are needed when defining recursive functions which are used inside their own body with different types.

This happens with your map function since it is defined as working on ('a,n) t and then called inside its definition on a value of type ('a, n-1) t.

1 Like