Re: gadt constructor

Le 2016-07-04 18:10, Gabriel Scherer [email protected] 
[ocaml_beginners] a écrit :
> It is incorrect to use a polymorphic type here. The function (let
> empty () = []) has the polymorphic type (type a . unit -> a list),
> because it can build a list of *any* type: you can use its result as
> an (int list), a (float list), any list you want.
> 
> Giving your function builder the type (type a . values -> a data)
> would mean that, for example, the return value (builder (`Num 3)) can
> be used at *any* type of the form ('a data), such as (int data) and
> (string data). This is wrong and would break type soundness.
> 
> Instead you must say that your function returns a value of type ('a
> data) for *some* type 'a, but not any of them. This requires the use
> of so-called "existential types", which can themselves be expressed
> through GADTs (or modules). For example, you can do the following:
> 
> type some_data = Data : 'a data -> some_data
> 
> (* Build the gadt *)
> let builder : values -> some_data = begin function
>    | `Num n -> Data (Num n)
>    | _ -> Data (Str "")
> end
> 
> This is discussed here for example:
>   http://engineering.issuu.com/2015/09/17/gadt-practicalities.html

This makes sense. Thanks a lot for your explanation.