Re: [Caml-list] GADTs and Menhir

[Andre Nathan <andre@digirati.com.br>]

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

On 03/31/2015 05:41 PM, Andre Nathan wrote:
> Can you give me an example of what this "GADT of type representations"
> would look like? I couldn't understand the Haskell example...

I found a reference to an email from Jeremy Yallop to the list from 2013
[1], and managed to get it working with the following solution:

(* foo.ml *)
open Printf

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

let typed = function
  | `Int i -> Any (Int i)
  | `Bool b -> Any (Bool b)

let print : type a. a t -> unit = function
  | Int i -> printf "%d\n" i
  | Bool b -> printf "%b\n" b

The parser now returns a `Foo.ast`:

value:
  | i = INTEGER { `Int i }
  | b = BOOL    { `Bool b }
  ;

and with that I can print the parsed value with

  let ast = Parser.start Lexer.token lexbuf in
  let Foo.Any t = Foo.typed ast in
  Foo.print t

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."

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


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 490 bytes --]