Re: [Caml-list] [GADT noob question] Building a GADT from an untyped representation

[Tiphaine Turpin <Tiphaine.Turpin@free.fr>]

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

Hi Philippe,

I don't think that you can achieve what you are you are asking exactly,
unless ressorting to an existential type. You can do it using GADT too,
as described in the "existential types" section of

https://sites.google.com/site/ocamlgadt/

For your example, you can write:

type any_expr =
  | Expr : _ expr -> any_expr
;;

let parse_expr x =
  try Expr (Int (int_of_string x))
  with _ ->
    Expr (Float (float_of_string x))
;;

Cheers,

Tiphaine


On 01/04/13 16:05, Philippe Veber wrote:
> Hi Yury,
>
> Thanks for your answer! It is true your fix is accepted by the
> compiler, but this is not what I was looking for: in the end I'd like
> to have an 'a expr such that 'a is the type of the value obtained when
> evaluating the expression. With the polymorphic variants, I cannot
> write an eval function of type 'a eval -> 'a, which is the main
> motivation behind using GADT in that (canonical) case. Sorry for
> ommiting this point!
>
> ph.
>
>
> 2013/1/4 Yury Sulsky <yury.sulsky@gmail.com
> <mailto:yury.sulsky@gmail.com>>
>
>     Hi Philippe,
>
>     I think you can do this by using a polymorphic variant as the type
>     variable:
>
>     type _ expr =
>     | Int : int -> [> `int ] expr
>     | Float : float -> [> `float ] expr
>
>     let parse_expr : string -> [ `int | `float ] expr = fun x -> 
>       try Int (int_of_string x) 
>       with _ -> 
>         Float (float_of_string x)
>     ;;         
>
>     - Yury
>
>
>
>     On Fri, Jan 4, 2013 at 8:32 AM, Philippe Veber
>     <philippe.veber@gmail.com <mailto:philippe.veber@gmail.com>> wrote:
>
>         Dear list,
>
>         Suppose I define a GADT for expressions:
>
>         type _ expr =
>         | Int : int -> int expr
>         | Float : float -> float expr
>
>         Now I want to write a parser, that will build an ['a expr]
>         from a string. Without thinking much, I tried the following:
>
>         let parse_expr : type s. string -> s expr = fun x ->
>           try Int (int_of_string x)
>           with _ ->
>             Float (float_of_string x)
>         ;;
>
>         Which fails with the following error message:
>
>         Error: This expression has type int expr but an expression was
>         expected of type s expr
>
>         That makes sense, since [s] is a locally abstract type. I
>         tried a couple of variants and finally realised that I could
>         not even write the type of [parse_expr]: it should be [string
>         -> 'a expr] for some ['a], but I'm not sure that really means
>         something.
>
>         So to put it simple, how does one construct a GADT value from
>         a string ?
>
>         Cheers,
>           ph.
>
>
>



[-- Attachment #2: Type: text/html, Size: 6723 bytes --]