Re: [Caml-list] GADTs and Menhir

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

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