Re: [Caml-list] GADTs and Menhir

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

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