However, by using an existential type like that, you're losing the additional type checking benefits of GADTs. The return type of parse_expr is now any_expr, not 'a expr. You can write e.g. the function extract_int_value : int expr -> int, where OCaml knows you don't need to match the Float case, but you'll never have an int expr to pass to this function, at least not as a result of parsing. Anything handling a parsed any_expr must match the Expr case, which of course can have any expr inside. At this point, it seems like just a cumbersome way to write the traditional expr type.

I went through basically this same thought process while trying to understand how I could apply the new OCaml GADT features, and I concluded that GADTs weren't providing any extra utility in the case where they must be constructed by parsing an input string. That's a shame since parsing and transformation is such a canonical use of OCaml, so I would love to be proven wrong here!

On Fri, Jan 4, 2013 at 9:25 AM, Philippe Veber <philippe.veber@gmail.com> wrote:

This is pretty much what I asked for, thanks Tiphaine!
ph.

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.