Re: gadt constructor

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

On Mon, Jul 4, 2016 at 11:34 AM, Sébastien Dailly
[email protected] [ocaml_beginners] <
[email protected]> wrote:

> Hello everybody,
>
> I'm trying to convert a structure data into gadt, and do not know how to
> build them :
>
> Here is a little example :
>
> (* The gadt I want to build *)
> type _ data =
>    | Num : int -> int data
>    | Str : string -> string data
>
> type values = [
>      | `Num of int
>      | `Other
> ]
>
> (* Build the gadt *)
> let builder : type a. values -> a data = begin function
>    | `Num n -> Num n
>    | _ -> Str ""
> end
>
> But this gives me an error :
>
> Error: This expression has type int data
>         but an expression was expected of type a data
>         Type int is not compatible with type a
>
> Do you know how I can tell the compiler that the type is polymorphic ?
>
> Thanks a lot
>
>
> ------------------------------------
> Posted by: =?UTF-8?Q?S=C3=A9bastien_Dailly?= <[email protected]>
> ------------------------------------
>
> Archives up to December 31, 2011 are also downloadable at
> http://www.connettivo.net/cntprojects/ocaml_beginners
> The archives of the very official ocaml list (the seniors' one) can be
> found at http://caml.inria.fr
> Attachments are banned and you're asked to be polite, avoid flames etc.
> ------------------------------------
>
> Yahoo Groups Links
>
>
>
>