Re: [Caml-list] GADTs and Menhir

[Gerd Stolpmann <info@gerd-stolpmann.de>]

[-- Attachment #1: Type: text/plain, Size: 2880 bytes --]

Am Mittwoch, den 01.04.2015, 09:16 -0300 schrieb Andre Nathan:
> type 'a t =
>   | Int : int -> int t
>   | Bool : bool -> bool t
> 
> type ast =
>   [ `Int of int
>   | `Bool of bool
>   ]
> 
> type any =
>   | Any : 'a t -> any
...
> I'm happy that it works, but the `any` type is a bit of a mistery to me.
> In Jeremy's email it's explained as
> 
> "An existential to hide the type index of a well-typed AST, making it
> possible to write functions that return constructed ASTs whose type is
> not statically known."

A couple of weeks ago I ran into the same problem. It is just a matter
of not being accustomed to how GADTs work, and not having the right
design patterns in your mind.

OCaml users are used to expose any polymorphism and that it is not
directly possible to hide it. So, normally if there is a variable 'a on
the right side of the type definition, it must also appear on the left
side (e.g. type 'a foo = Case1 of 'a | Case2 of ...). This is not
required for GADTs, because the variable is bound by the case it applies
to (i.e. for the Int case you have 'a=int and for the Bool case you have
'a=bool). So it is implicitly known. Because of this, many people prefer
to write

type _ t =                  (* look here, no 'a anymore *)
  | Int : int -> int t
  | Bool : bool -> bool t

and 

type any =
  | Any : _ t -> any

The type parameter still exists because t is still polymorphic, but you
cannot do anything with it unless you match against the cases. Now,
"any" goes a step further, and even discards this parameter. It's a
matter of perspective: if 'a is case-dependent but not dependent to
anything outside t, you can also consider t as monomorphic. In other
words: Knowing all cases binds 'a. 

You need Any if you want to put several t values into a container, e.g.

Does not work: [ Int 34; Bool true ]
Does work:     [ Any(Int 34); Any(Bool true) ]

This nice thing with GADTs is that you can "undo" this change of
perspective by matching against the cases:

let print = ... (* as you defined it *)
let print_any (Any x) = print x
let () =
  List.iter print_any [ Any(Int 34); Any(Bool true) ]

Gerd

> Does anyone have a reference to literature that explains this technique
> (I'm guessing that would be Pierce's book)? The OCaml manual briefly
> shows an example with a `dyn` type, but not much is said about it.
> 
> Thanks,
> Andre
> 
> [1] https://sympa.inria.fr/sympa/arc/caml-list/2013-01/msg00013.html
> 

-- 
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany    gerd@gerd-stolpmann.de
My OCaml site:          http://www.camlcity.org
Contact details:        http://www.camlcity.org/contact.html
Company homepage:       http://www.gerd-stolpmann.de
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]