Version française
Home     About     Download     Resources     Contact us    
Browse thread
GADT constructor syntax
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Lukasz Stafiniak <lukstafi@g...>
Subject: Re: [Caml-list] GADT constructor syntax
On Sun, Dec 5, 2010 at 9:10 AM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
>
> 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).

To clarify again: modulo variable capture! That is, the pattern

> type X =
>  | Branch of 'a. Y : X

will be different (unless 'a is not used in Y nor X).