[Caml-list] GADTs and Menhir

[Caml-list] GADTs and Menhir

[Andre Nathan]

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

Hello

I'm trying to learn a bit about GADTs, but I can't figure out how to
make them work with Menhir.

I have defined the following GADT:

(* foo.ml *)

type 'a t =
  | Int : int -> int t
  | Bool : bool -> bool t

With this definition I can write an "eval" function as

let eval (type t) (foo : t Foo.t) : t =
  match foo with
  | Foo.Int i -> i
  | Foo.Bool b -> b

Now considering the simple parser and lexer below,

(* parser.mly *)

%{ open Foo %}

%token <int> INTEGER
%token <bool> BOOL
%token EOF

%start <'a Foo.t> start
%%

start:
  | value; EOF { $1 }
  ;
value:
  | i = INTEGER  { Int i }
  | b = BOOL     { Bool b }
  ;

(* lexer.mll *)

{ open Parser }

let digit = ['0'-'9']
let boolean = "true" | "false"

rule token = parse
  | [' ' '\t']             { token lexbuf }
  | '\n'                   { Lexing.new_line lexbuf; token lexbuf }
  | digit+ as i            { INTEGER (int_of_string i) }
  | boolean as b           { BOOL (bool_of_string b) }
  | eof                    { EOF }

when I try to compile this I get the error below:

File "parser.mly", line 15, characters 43-52:
Error: This expression has type int Foo.t
       but an expression was expected of type bool Foo.t
       Type int is not compatible with type bool

This is the

  | b = BOOL     { Bool b }

line. I believe the error comes from not having the locally-abstract
type annotations in the code generated by Menhir.

Is there any way around this?

Thanks in advance,
Andre


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

Re: [Caml-list] GADTs and Menhir

[Francois Pottier]

On Tue, Mar 31, 2015 at 03:16:32PM -0300, Andre Nathan wrote:
> value:
>   | i = INTEGER  { Int i }
>   | b = BOOL     { Bool b }

The problem lies here. What is the OCaml type of the symbol "value"? The OCaml
compiler complains that in one branch it seems to be int Foo.t, but in the
other branch it seems to be bool Foo.t. (The problem does not have anything to
do with Menhir, really.)

Usually, it is not advisable to try to perform parsing and type-checking in
one single phase. So, my advice would be to:

  1- perform parsing in the usual way,
     constructing ASTs in a normal algebraic data type "ast"
     (not a GADT);

  2- perform type-checking (or type inference).
     If you insist on using GADTs, you will probably need
     a GADT of terms (your type 'a Foo.t) and
     a GADT of type representations ('a ty)
     and the type-checking function will have type
     ast -> 'a ty -> 'a Foo.t option
     which means that, given an untyped term and
     a representation of an expected type, it
     either fails or succeeds and produces a typed term.

There are examples of this kind of thing online, e.g.
http://www.cs.ox.ac.uk/projects/gip/school/tc.hs
by Stephanie Weirich.

Hope this helps,

-- 
François Pottier
Francois.Pottier@inria.fr
http://gallium.inria.fr/~fpottier/

Re: [Caml-list] GADTs and Menhir

[Andre Nathan]

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

On 03/31/2015 04:45 PM, Francois Pottier wrote:
> The problem lies here. What is the OCaml type of the symbol "value"?

I see now.

>   2- perform type-checking (or type inference).
>      If you insist on using GADTs, you will probably need
>      a GADT of terms (your type 'a Foo.t) and
>      a GADT of type representations ('a ty)
>      and the type-checking function will have type
>      ast -> 'a ty -> 'a Foo.t option
>      which means that, given an untyped term and
>      a representation of an expected type, it
>      either fails or succeeds and produces a typed term.

Can you give me an example of what this "GADT of type representations"
would look like? I couldn't understand the Haskell example...

Thanks,
Andre


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

Re: [Caml-list] GADTs and Menhir

[Andre Nathan]

[-- 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 --]

Re: [Caml-list] GADTs and Menhir

[Jeremy Yallop]

On 1 April 2015 at 13:16, Andre Nathan <andre@digirati.com.br> wrote:
> 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.

There's a more detailed explanation of the technique in the lecture
notes on the following page:

   http://www.cl.cam.ac.uk/teaching/1415/L28/materials.html

The section you want is

    8.4.2 Pattern: building GADT values

on p83 of the notes from 9 February, but it might also be helpful to
look through some of the earlier notes for background.

Jeremy.

Re: [Caml-list] GADTs and Menhir

[Andre Nathan]

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

On 04/01/2015 09:27 AM, Jeremy Yallop wrote:
> There's a more detailed explanation of the technique in the lecture
> notes on the following page:
> 
>    http://www.cl.cam.ac.uk/teaching/1415/L28/materials.html
> 
> The section you want is
> 
>     8.4.2 Pattern: building GADT values
> 
> on p83 of the notes from 9 February, but it might also be helpful to
> look through some of the earlier notes for background.

Thank you!



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

Re: [Caml-list] GADTs and Menhir

[Gerd Stolpmann]

[-- 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 --]

Re: [Caml-list] GADTs and Menhir

[Andre Nathan]

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

Hi Gerd

On 04/01/2015 10:16 AM, Gerd Stolpmann wrote:
> 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:

But is there any way to, say, write some sort of lookup function for
values in such containers?

Eg. given an eval function, this doesn't work:

let rec find k l =
  match l with
  | [] -> raise Not_found
  | (k', v)::rest ->
      if k = k' then v
      else find k rest

let foo () =
  let dict = ["int", Any (Int 1); "bool", Any (Bool true)] in
  let Any x = find "int" dict in
  eval x
  ^^^^^^
Error: This expression has type a#0 but an expression was expected of
type a#0
       The type constructor a#0 would escape its scope

I don't understand why `eval` can be written but it's result cannot be
returned from another function.

I tried introducing a type variable but it still doesn't work

let foo (type a) () : a =
  let dict = ["x", Any (Int 1); "y", Any (Bool true)] in
  let Any (x : a t) = find "x" dict in
  eval x
          ^^^^^^^^^
Error: This pattern matches values of type a t
       but a pattern was expected which matches values of type a#0 t
       Type a is not compatible with type a#0

Thanks,
Andre


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