Re: [Caml-list] GADT constructor syntax

[Lukasz Stafiniak <lukstafi@gmail.com>]

On Sat, Dec 4, 2010 at 10:06 PM, Jacques Le Normand
<rathereasy@gmail.com> wrote:
> in this case, yes, but if you have constraints then it is different. consider:
>
> type 'a term =
>      | Ignore of 'a : int term
>      | Embed of 'a
>   constraint 'a = int
>
> this is different from:
>
> type 'a term =
>     | Ignore of 'a : int term
>     | Embed of 'a : 'a term
>   constraint 'a = int
>
> (in fact, an error is flagged on the second one)
>
> Also, it can save the user some typing.

I don't think that it is very different. Standard-language constraints
are outside of implications, so they apply to each branch. It already
behaves this way in the standard language, basically restricting the
type family to "int term". So I don't see why

> | Embed of 'a : 'a term
>   constraint 'a = int

shouldn't mean that Embed is "basically" Embed of int : int term. My
position is that if a type variable should be treated as local to a
branch, it should be explicitly quantified (using the dot notation,
for example "Ignore of 'a. 'a : int term", without any exceptions to
"existential" variables). And that the patterns

type X =
  | Branch of Y

and

type X =
  | Branch of Y : X

should be equivalent (where X could for example be 'a term).

I would accept concessions to my general outlook on the grounds of
being conservative over standard OCaml programmer intuitions and
conciseness of code... when they apply...