2013/1/4 Tiphaine Turpin <Tiphaine.Turpin@free.fr>

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>

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