Annotating by an existential type

Learning
,
1

When using GADTs I often find myself needing to give a type annotation that’s impossible to give because it involves existential types that I don’t have a name for. For instance, consider the following code:

type bar = private Dummy_bar
type baz = private Dummy_baz
type _ foo = Bar : int -> bar foo | Baz : string -> baz foo
type afoo = A : 'a foo -> afoo
let update_afoo : afoo -> afoo = fun x ->
  let (A y) = x in
  let z = match y with Bar i -> Bar (i+1) | Baz s -> Baz (s ^ "1") in
  A z

This produces the error on Baz (s ^ "1") that

This expression has type $a foo but an expression was expected of type
  bar foo
Type $a is not compatible with type bar
Hint: $a is an existential type bound by the constructor A.

Evidently the problem is that OCaml has inferred from the type of the result Bar (i+1) of the first branch that the result type of the match should be the specific bar foo, whereas I really wanted the type of the match to be the more general $a foo where $a is the type of y. If I had a name for $a then I could annotate the match so that it would work, but I don’t.

The only real solution I’ve found to this sort of problem is to define a helper function with an explicitly polymorphic type:

et update_afoo : afoo -> afoo = fun x ->
let (A y) = x in
  let makez : type a. a foo -> a foo = fun y ->
    match y with Bar i -> Bar (i+1) | Baz s -> Baz (s ^ "1") in
  A (makez y)

But this is kind of annoying, especially having to write out the whole type of the helper function, which in applications can be quite long as it needs to be given as arguments all the other variables in scope whose type should be refined in the match bodies. Is there a better way to deal with it?

2

You can bind the existentials in a GADT constructor as follows:

let update_afoo : afoo -> afoo = fun x ->
  let A (type a) (y : a foo) = x in
  let z : a foo = match y with Bar i -> Bar (i+1) | Baz s -> Baz (s ^ "1") in
  A z

See OCaml - Generalized algebraic datatypes.

Cheers,
Nicolas

7 Likes
3

Fabulous, thank you!

4

Can I do this if the arguments of the constructor are wrapped in an inline record? Using the example from the manual:

type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)

I tried the obvious

type _ closure = Closure : {f : ('a -> 'b); x : 'a} -> 'b closure
let eval = fun (Closure (type a) ({f; x} : {f : (a -> _); x : _})) -> f (x : a)

but I got “Syntax error: type expected”.

5

I don’t think it is possible, as there is no syntax denoting the type of an inline record (as you discovered).

Cheers,
Nicolas

6

Oh. That’s… disappointing. Is there any chance of that situation being improved? I had always thought that inline-record constructors were strictly better (aside from being more verbose) because they enforce documentation of the names/meanings of all the constructor arguments, so it’s surprising and disappointing if there’s something we can do with ordinary constructors that we can’t do with inline-record constructors.

7

Oh, duh, I can just factor out the record type:

type ('a, 'b) closure_args = {f : ('a -> 'b); x : 'a}
type _ closure = Closure : ('a, 'b) closure_args -> 'b closure
let eval = fun (Closure (type a) ({f; x} : (a, _) closure_args)) -> f (x : a)