Existentially quantified type parameter, recursive function and type error

Question

Consider the following piece of OCaml code:

type mytype = My : 'a list * 'a -> mytype

let rec foo : int -> mytype =
    fun n -> if n < 0 then My([], 2)
        else let My(xs, y) = foo (n - 1)
        in My(3::xs, y)

The OCaml interpreter gives me an error on the last line of foo, saying:

This expression has type a#1 list but an expression was expected of type int list

Type a#1 is not compatible with type int

I could make that code work by adding a type parameter to mytype so it would be

type _ mytype = My : 'a list * 'a -> 'a mytype
let rec foo : int -> 'a mytype =
...

But let's say I really don't want to change the definition of mytype. Could I then write foo, assuming I want to preserve that function's (intuitively understood by the non-working code) behaviour?

Also, could someone explain what is the root of the problem, i.e. why the initial code doesn't type-check?

PatJ PatJ · Accepted Answer · 2015-04-14T22:17:09

When a pattern matching is done on a mytype value, there is no way to know what type is inside. The thing is, the typing system acts quite simply and doesn't try to know where the mytype is from even if it comes from a recursive call (the typing system just doesn't work that way).

The thing is, you know in that case that the 'a is indeed int, but you need to give a proof of that to the compiler.

In that specific case, you don't need to. You just need to use the GADT only at the end of your function:

let foo n =
 let rec aux n =
  if n < 0 then ([], 2)
  else let (xs, y) = aux (n - 1)
   in (3::xs, y)
 in
 let (xs,y) = aux n in My (xs,y)

It is worth noting that with that type definition, there is no way for you to use the fact that you know there are integers values in your mytype, so it will be pretty unusable. GADTs should be used only in specific cases and you should precisely know why and how you'll be using them.

EDIT:

A type can be seen as a logical formula attached to every value. In most cases, it is pretty simple and you don't have to worry about it, mostly because type variables ('a 'b and so forth) are universally quantified and always visible to the exterior of the type.

type 'a mylist = Cons of 'a * 'a list | Nil
(* should be read as:
    for all 'a,
    'a mylist is either
      * a cons containing the same 'a and 'a list
      * nil *)

type mylist = Cons : 'a * mylist -> mylist | Nil : mylist
(* should be read as:
    mylist is either
     * for some 'a, a 'a and another list
     * nil *)

In the GADT above, you can see that nothing states that every element in the list is of the same type. In fact, if you get a mylist, you have no way of knowing what element is inside.

So, you need to prove it. A good way of doing so is to store inside the gadt a proof of type:

type _ proof =
 | Int : int proof
 | Float : float proof
 | Tuple : 'a proof * 'b proof -> ('a * 'b) proof
 (* You can add other constructors depending on
    the types you want to store *)

type mytype = My : 'a proof * 'a list * 'a -> mytype

Now with this, when opening a mytype, you can match on the proof to prove the value of 'a. The compiler will know it's the same because it would refuse to create a mytype without a proof corresponding to the right type.

As you can see, GADTs are not simple, and you often need to do several drafts before going to implementation. Most of the time, you can avoid using them (and if you're not sure of how they work, don't use them at all).

Existentially quantified type parameter, recursive function and type error

1 Answers