Re: [Caml-list] Re: Generalized Algebraic Datatypes

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2010/10/30, at 8:01, Jacques Le Normand wrote:
> On Fri, Oct 29, 2010 at 5:37 PM, bluestorm <bluestorm.dylc@gmail.com> wrote:
> Note that, as in Jacques's examples, the constructor function was not curryfied. (type t = A of bool * int) would generate a function (A : bool * int -> t). It doesn't help the already tricky confusion between (A of bool * int) and (A of (bool * int))...
> By the way, it is unclear if
>  | App : ('a -> 'b) t -> 'a t -> 'b t
> would be accepted in Jacques proposal. If not, I think going back to a "of ..." syntax would be wiser.
> 
> It is accepted. In fact, that constructor is part of an example on my webpage.
> If there's any doubt, you can always download the source and try it out.

Actually, curryfied constructors are not allowed, so this is not accepted.
(Existential types are allowed, which may have confused the other Jacques)

To go back to the main subjec,t the syntax with an explicit return type was chosen
because it is closer to the way gadts are implemented here than a syntax based
on constraints. Namely the the type of the expression matched get refined
through unification with the return type of the corresponding case.
It also happens to be the usual syntax in Coq and Haskell, so this
should not come as a shock to most people.

If the risk of confusion with constructors-as-functions is deemed problematic,
a syntax like
   App of ('a -> 'b) t * 'a t : 'b t
seems OK too.
Actually this would have the advantage of allowing the scope of existential variables
to be explicit. I.e. one could write
  App of 'a. ('a -> 'b) t * 'a t : 'b t

Jacques Garrigue