Re: [Caml-list] Generalized Algebraic Datatypes

Re: [Caml-list] Generalized Algebraic Datatypes

[Dario Teixeira]

Hi,

> I am pleased to announce an experimental branch of the O'Caml compiler:
> O'Caml extended with Generalized Algebraic Datatypes. You can find more
> information on this webpage:

I have a couple of questions regarding the syntax you've chosen for GADT
declaration.  For reference, let's consider the first example you've provided:

type _ t =
  | IntLit : int -> int t
  | BoolLit : bool -> bool t
  | Pair : 'a t * 'b t -> ('a * 'b) t
  | App : ('a -> 'b) t * 'a t -> 'b t
  | Abs : ('a -> 'b) -> ('a -> 'b) t 


There's something "Haskellish" about this syntax, in the sense that type
constructors are portrayed as being like functions.  While this does make
sense in Haskell, in Ocaml it feels a bit out of place, because you cannot,
for example, partially apply a type constructor.

Also, note that in all the variant declarations the final token is 't'.  
Are there any circumstances at all where a GADT constructor will not end
by referencing the type being defined?  If there are not, then this syntax
imposes some syntactic salt into the GADT declaration.

I know this is not the sole syntax that was considered for GADTs in Ocaml.
Xavier Leroy's presentation in CUG 2008 shows a different one, which even
though slightly more verbose, does have the advantage of being more "Camlish".
Is there any shortcoming to the 2008 syntax that resulted in it being dropped
in favour of this new one?

Best regards,
Dario Teixeira

Re: [Caml-list] Generalized Algebraic Datatypes

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 1683 bytes --]

Hello,

I didn't know about this alternate syntax; can you please describe it?
cheers
--Jacques

On Fri, Oct 29, 2010 at 10:32 AM, Dario Teixeira <darioteixeira@yahoo.com>wrote:

> Hi,
>
> > I am pleased to announce an experimental branch of the O'Caml compiler:
> > O'Caml extended with Generalized Algebraic Datatypes. You can find more
> > information on this webpage:
>
> I have a couple of questions regarding the syntax you've chosen for GADT
> declaration.  For reference, let's consider the first example you've
> provided:
>
> type _ t =
>  | IntLit : int -> int t
>  | BoolLit : bool -> bool t
>  | Pair : 'a t * 'b t -> ('a * 'b) t
>  | App : ('a -> 'b) t * 'a t -> 'b t
>  | Abs : ('a -> 'b) -> ('a -> 'b) t
>
>
> There's something "Haskellish" about this syntax, in the sense that type
> constructors are portrayed as being like functions.  While this does make
> sense in Haskell, in Ocaml it feels a bit out of place, because you cannot,
> for example, partially apply a type constructor.
>
> Also, note that in all the variant declarations the final token is 't'.
> Are there any circumstances at all where a GADT constructor will not end
> by referencing the type being defined?  If there are not, then this syntax
> imposes some syntactic salt into the GADT declaration.
>
> I know this is not the sole syntax that was considered for GADTs in Ocaml.
> Xavier Leroy's presentation in CUG 2008 shows a different one, which even
> though slightly more verbose, does have the advantage of being more
> "Camlish".
> Is there any shortcoming to the 2008 syntax that resulted in it being
> dropped
> in favour of this new one?
>
> Best regards,
> Dario Teixeira
>
>
>
>
>

[-- Attachment #2: Type: text/html, Size: 2305 bytes --]

Re: Generalized Algebraic Datatypes

[Sylvain Le Gall]

On 29-10-2010, Jacques Le Normand <rathereasy@gmail.com> wrote:
>
> I didn't know about this alternate syntax; can you please describe it?
> cheers
> --Jacques

It is on page 14:
http://gallium.inria.fr/~xleroy/talks/cug2008.pdf

And around 14:22 in the video:
http://video.google.com/videoplay?docid=1704671501085578312&hl=en#

Regards
Sylvain Le Gall

Re: [Caml-list] Generalized Algebraic Datatypes

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 2046 bytes --]

Assuming I understand this syntax, the following currently valid type
definition would have two interpretations:

type 'a t = IntLit of 'a constraint 'a = int

One interpretation as a standard constrained ADT and one interpretation as a
GADT. We could use another token, other than constraint, for example:

type 'a t = IntLit of 'a : 'a = int

to which I have no objections. As you pointed out, though, the current
syntax is more concise.

cheers,
--Jacques

On Fri, Oct 29, 2010 at 10:32 AM, Dario Teixeira <darioteixeira@yahoo.com>wrote:

> Hi,
>
> > I am pleased to announce an experimental branch of the O'Caml compiler:
> > O'Caml extended with Generalized Algebraic Datatypes. You can find more
> > information on this webpage:
>
> I have a couple of questions regarding the syntax you've chosen for GADT
> declaration.  For reference, let's consider the first example you've
> provided:
>
> type _ t =
>  | IntLit : int -> int t
>  | BoolLit : bool -> bool t
>  | Pair : 'a t * 'b t -> ('a * 'b) t
>  | App : ('a -> 'b) t * 'a t -> 'b t
>  | Abs : ('a -> 'b) -> ('a -> 'b) t
>
>
> There's something "Haskellish" about this syntax, in the sense that type
> constructors are portrayed as being like functions.  While this does make
> sense in Haskell, in Ocaml it feels a bit out of place, because you cannot,
> for example, partially apply a type constructor.
>
> Also, note that in all the variant declarations the final token is 't'.
> Are there any circumstances at all where a GADT constructor will not end
> by referencing the type being defined?  If there are not, then this syntax
> imposes some syntactic salt into the GADT declaration.
>
> I know this is not the sole syntax that was considered for GADTs in Ocaml.
> Xavier Leroy's presentation in CUG 2008 shows a different one, which even
> though slightly more verbose, does have the advantage of being more
> "Camlish".
> Is there any shortcoming to the 2008 syntax that resulted in it being
> dropped
> in favour of this new one?
>
> Best regards,
> Dario Teixeira
>
>
>
>
>

[-- Attachment #2: Type: text/html, Size: 2772 bytes --]

Re: [Caml-list] Generalized Algebraic Datatypes

[Xavier Leroy]

Jacques Le Normand wrote:

> Assuming I understand this syntax, the following currently valid type
> definition would have two interpretations: [...]

Don't take the syntax from my 2008 CUG talk too seriously, it was just
a mock-up for the purpose of the talk.  Besides, it's too early for a
syntax war :-)

This said, Coq could be another source of syntactic inspiration: it
has several equivalent syntaxes for inductive type declarations (a
superset of GADTs), one Haskell-like, others more Caml-like.

- Xavier Leroy

Re: [Caml-list] Generalized Algebraic Datatypes

[Dario Teixeira]

Hi,

> Don't take the syntax from my 2008 CUG talk too seriously, it was just
> a mock-up for the purpose of the talk.  Besides, it's too early for a
> syntax war :-)

Indeed.  There's just something about syntax that tickles the more
primitive parts of the programmer's brain... :-)


> This said, Coq could be another source of syntactic inspiration: it
> has several equivalent syntaxes for inductive type declarations (a
> superset of GADTs), one Haskell-like, others more Caml-like.

I think we can all agree that ultimately the chosen syntax should be
one that is unambiguous and coherent.  Nevertheless, all other factors
being equal, it would be preferable to have a Camlish syntax that feels
"right at home" within the broader language.

My initial reticence to Jacques proposal syntax was based solely on it
having provoked a context-switch in my brain: the declarations only
made intuitive sense when I tried reading them as if they were Haskell.
In contrast, the CUG 2008 syntax made immediate sense, even if it
may require serious massaging before it can be deemed suitable.

But anyway, this syntax talk is all small potatoes.  The important thing
is that Ocaml is getting yet another killer feature...

Cheers,
Dario Teixeira

Re: Generalized Algebraic Datatypes

[Stefan Monnier]

> type _ t =
>   | IntLit : int -> int t
>   | BoolLit : bool -> bool t
>   | Pair : 'a t * 'b t -> ('a * 'b) t
>   | App : ('a -> 'b) t * 'a t -> 'b t
>   | Abs : ('a -> 'b) -> ('a -> 'b) t 

> There's something "Haskellish" about this syntax, in the sense that type
> constructors are portrayed as being like functions.

Indeed IIRC OCaml does not accept "App" as an expression (you have to
provide arguments to the construct).  Maybe this is a good opportunity
to lift this restriction.

> While this does make sense in Haskell, in Ocaml it feels a bit out of
> place, because you cannot, for example, partially apply
> a type constructor.

The types above don't allow partial applications either.  They use the
OCaml/SML style of constructors were partial application is not possible
because the various arguments are not provided in a curried way.


        Stefan

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

[bluestorm]

[-- Attachment #1: Type: text/plain, Size: 1343 bytes --]

On Fri, Oct 29, 2010 at 11:10 PM, Stefan Monnier <monnier@iro.umontreal.ca>
 wrote:

> > type _ t =
> >   | IntLit : int -> int t
> >   | BoolLit : bool -> bool t
> >   | Pair : 'a t * 'b t -> ('a * 'b) t
> >   | App : ('a -> 'b) t * 'a t -> 'b t
> >   | Abs : ('a -> 'b) -> ('a -> 'b) t
>
> > There's something "Haskellish" about this syntax, in the sense that type
> > constructors are portrayed as being like functions.
>
> Indeed IIRC OCaml does not accept "App" as an expression (you have to
> provide arguments to the construct).  Maybe this is a good opportunity
> to lift this restriction.


It was actually the case in Caml Light : each datatype constructor
implicitly declared a constructor function with the same name. I don't
exactly know why this feature was dropped in Objective Caml, but I think I
remember (from a previous discussion) that people weren't sure it was worth
the additional complexity.

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.

[-- Attachment #2: Type: text/html, Size: 2044 bytes --]

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

[Wojciech Daniel Meyer]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

> Indeed IIRC OCaml does not accept "App" as an expression (you have to
> provide arguments to the construct).  Maybe this is a good opportunity
> to lift this restriction.
>

I wish to see first class data constructors in OCaml someday.

>
> The types above don't allow partial applications either.  They use the
> OCaml/SML style of constructors were partial application is not possible
> because the various arguments are not provided in a curried way.

Probably it will never happen to un-curry the arguments for the data
constructors in OCaml. It is too massive change, but passing the
constructor as a standalone argument should be fairly possible, 

Wojciech

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

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 1956 bytes --]

On Fri, Oct 29, 2010 at 5:37 PM, bluestorm <bluestorm.dylc@gmail.com> wrote:

> On Fri, Oct 29, 2010 at 11:10 PM, Stefan Monnier <monnier@iro.umontreal.ca
> > wrote:
>
>> > type _ t =
>> >   | IntLit : int -> int t
>> >   | BoolLit : bool -> bool t
>> >   | Pair : 'a t * 'b t -> ('a * 'b) t
>> >   | App : ('a -> 'b) t * 'a t -> 'b t
>> >   | Abs : ('a -> 'b) -> ('a -> 'b) t
>>
>> > There's something "Haskellish" about this syntax, in the sense that type
>> > constructors are portrayed as being like functions.
>>
>> Indeed IIRC OCaml does not accept "App" as an expression (you have to
>> provide arguments to the construct).  Maybe this is a good opportunity
>> to lift this restriction.
>
>
>  It was actually the case in Caml Light : each datatype constructor
> implicitly declared a constructor function with the same name. I don't
> exactly know why this feature was dropped in Objective Caml, but I think I
> remember (from a previous discussion) that people weren't sure it was worth
> the additional complexity.
>
> 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.
cheers,
Jacques

>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

[-- Attachment #2: Type: text/html, Size: 3404 bytes --]

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

[Jacques Garrigue]

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

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

[Jacques Carette]

On 30/10/2010 1:14 AM, Jacques Garrigue wrote:
> On 2010/10/30, at 8:01, Jacques Le Normand 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).
> Actually, curryfied constructors are not allowed, so this is not accepted.
> (Existential types are allowed, which may have confused the other Jacques)

I was not confused at all.

Jacques Carette

PS: ;-)

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

[Dario Teixeira]

Hi,

> > While this does make sense in Haskell, in Ocaml it feels a bit
> > out of place, because you cannot, for example, partially apply
> > a type constructor.
> 
> The types above don't allow partial applications either.  They use the
> OCaml/SML style of constructors were partial application is not possible
> because the various arguments are not provided in a curried way.

That was precisely my point (I think you may have misunderstood what I said).
In Ocaml, whenever you see a curried type declaration you can safely assume
that the constructors may be partially applied.  The GADT syntax under
discussion breaks this assumption; hence my reticence.

Cheers,
Dario Teixeira

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

[Dario Teixeira]

Hi,

> 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

I find this new syntax preferable too.  As I just mentioned in my reply to
Stefan Monnier, my main criticism to the currently implemented GADT syntax
is that type constructors are declared in a curried way, despite the fact
that they cannot actually be partially applied.  This breaks an assumption
that is otherwise consistent throughout the language, and I think we can
all agree that adding caveats and exceptions to a language specification
is something that should be avoided as much as possible (and is often the
symptom of a bad specification).

Best regards,
Dario Teixeira

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

[Wojciech Daniel Meyer]

bluestorm <bluestorm.dylc@gmail.com> writes:

> It was actually the case in Caml Light : each datatype constructor
> implicitly declared a constructor function with the same name. I
> don't exactly know why this feature was dropped in Objective Caml,
> but I think I remember (from a previous discussion) that people
> weren't sure it was worth the additional complexity.

Would that be not possible now with Camlp4 extension?

Wojciech

Re: Generalized Algebraic Datatypes

[Sylvain Le Gall]

On 31-10-2010, Wojciech Daniel Meyer <wojciech.meyer@googlemail.com> wrote:
> bluestorm <bluestorm.dylc@gmail.com> writes:
>
>> It was actually the case in Caml Light : each datatype constructor
>> implicitly declared a constructor function with the same name. I
>> don't exactly know why this feature was dropped in Objective Caml,
>> but I think I remember (from a previous discussion) that people
>> weren't sure it was worth the additional complexity.
>
> Would that be not possible now with Camlp4 extension?
>

I am pretty sure, it is possible to implement them with camlp4. Just a
matter of time -- and motivation.

The only limitation I can see, is that the generated constructors won't
be capitalized. E.g.:

type t = MyConstr | YourConstr of int 

=>

type t = MyConstr | YourConstr of int

let myConstr = MyConstr
let yourConstr i = YouConstr i

Regards,
Sylvain Le Gall

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

[Lukasz Stafiniak]

On Sun, Oct 31, 2010 at 3:35 PM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
> On 31-10-2010, Wojciech Daniel Meyer <wojciech.meyer@googlemail.com> wrote:
>> bluestorm <bluestorm.dylc@gmail.com> writes:
>>
>>> It was actually the case in Caml Light : each datatype constructor
>>> implicitly declared a constructor function with the same name. I
>>> don't exactly know why this feature was dropped in Objective Caml,
>>> but I think I remember (from a previous discussion) that people
>>> weren't sure it was worth the additional complexity.
>>
>> Would that be not possible now with Camlp4 extension?
>>
>
> I am pretty sure, it is possible to implement them with camlp4. Just a
> matter of time -- and motivation.
>
> The only limitation I can see, is that the generated constructors won't
> be capitalized. E.g.:
>
> type t = MyConstr | YourConstr of int
>
> =>
>
> type t = MyConstr | YourConstr of int
>
> let myConstr = MyConstr
> let yourConstr i = YouConstr i
>

Why do you say so? HOL Light uses capitalized identifiers for values,
for example. It's probably possible to do whatever one reasonably
wants.

Re: Generalized Algebraic Datatypes

[Sylvain Le Gall]

On 31-10-2010, Lukasz Stafiniak <lukstafi@gmail.com> wrote:
> On Sun, Oct 31, 2010 at 3:35 PM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
>> On 31-10-2010, Wojciech Daniel Meyer <wojciech.meyer@googlemail.com> wrote:
>>> bluestorm <bluestorm.dylc@gmail.com> writes:
>>>
>>>> It was actually the case in Caml Light : each datatype constructor
>>>> implicitly declared a constructor function with the same name. I
>>>> don't exactly know why this feature was dropped in Objective Caml,
>>>> but I think I remember (from a previous discussion) that people
>>>> weren't sure it was worth the additional complexity.
>>>
>>> Would that be not possible now with Camlp4 extension?
>>>
>>
>> I am pretty sure, it is possible to implement them with camlp4. Just a
>> matter of time -- and motivation.
>>
>> The only limitation I can see, is that the generated constructors won't
>> be capitalized. E.g.:
>>
>> type t = MyConstr | YourConstr of int
>>
>> =>
>>
>> type t = MyConstr | YourConstr of int
>>
>> let myConstr = MyConstr
>> let yourConstr i = YouConstr i
>>
>
> Why do you say so? HOL Light uses capitalized identifiers for values,
> for example. It's probably possible to do whatever one reasonably
> wants.
>

Function names and values are "low id" in OCaml (first letter must be
uncapitalized). If you try to define "let MyConstr = 0" in an OCaml
toplevel, you will get a syntax error... 

The code generated by camlp4 must be syntactically correct.

But maybe you are talking about a deeper integration?

E.g. whenever you encounter the constructor "YourConstr" in expr, you
transform it into "fun i -> YourConstr i". This should work but since
camlp4 is limited to a single module, you won't be able to use this
outside the module, because you won't have access to the definition of
YouConstr and won't be able to determine his arity...

But if you have an idea about how to solve this, just tell us.

Regards,
Sylvain Le Gall

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

[Lukasz Stafiniak]

On Sun, Oct 31, 2010 at 4:08 PM, Sylvain Le Gall <sylvain@le-gall.net> wrote:
>
> Function names and values are "low id" in OCaml (first letter must be
> uncapitalized). If you try to define "let MyConstr = 0" in an OCaml
> toplevel, you will get a syntax error...

In unmodified toplevel, but the whole point is to use camlp4 (or camlp5).

> The code generated by camlp4 must be syntactically correct.

No, camlp4 generates syntax trees (i.e. they don't have syntax other
than abstract syntax). (But if there are any asserts in OCaml source
that an AST element called a lower case identifier is actually lower
case, that could be a problem.)

> But maybe you are talking about a deeper integration?

One possibility would be to translate any "Constr" into a value in
contexts where it cannot be parsed as applied to a value, and as
constructor where it is applied to a value... It wouldn't be directly
partially applicable, but it would serve most purposes since it would
work as a function when passed to higher order functions as fold (and
also could be easily rebound).

Re: [Caml-list] Generalized Algebraic Datatypes

[Florian Hars]

Am 25.10.2010 10:39, schrieb Jacques Le Normand:
> I am pleased to announce an experimental branch of the O'Caml compiler:
> O'Caml extended with Generalized Algebraic Datatypes.

Of course, some would claim than 3.12 is already almost there:
http://okmij.org/ftp/ML/first-class-modules/#naive-GADTs
(not that I usually understand what Oleg does...)

- Florian

Re: [Caml-list] Generalized Algebraic Datatypes

[Jacques Le Normand]

[-- Attachment #1: Type: text/plain, Size: 7973 bytes --]

On Mon, Oct 25, 2010 at 6:44 PM, bluestorm <bluestorm.dylc@gmail.com> wrote:

> It's very interesting.
>
> First, I'm curious of the "historical" aspects of this work : where does it
> come from ? Apparently there is work from you and Jacques Garrigue, but it's
> hard to tell. Is it new, or a long-running experiment ?
>
>
The history: the algorithm was developed, in part, for my PhD research. I've
been working on it with Jacques Garrigue for the last two months.


> In your "intuition" section (btw. there is a typo here, it should be (type
> s) (x : s t)), you seem to present GADT as directly related to the new (type
> s) construct. It's a bit surprising because it's difficult to know the
> difference between this and classic type variables. I suppose it is because
> only (type s) guarantee that the variable remains polymorphic, and you use
> that to ensure that branch-local unifications don't "escape" to the outer
> level ? Could you be a bit more explicit on this ?
>
>
I don't know what you mean by "remains polymorphic". However, (type s) and
polymorphism are quite distinct concepts. Consider the following examples:

# let rec f (type s) (x : s) : s = f x;;
Error: This expression has type s but an expression was expected of type s
       The type constructor s would escape its scope

# fun (type s) ( f : s -> s) ( x : s) -> f x;;
- : ('_a -> '_a) -> '_a -> '_a = <fun>


The reason I chose to use newtypes, ie (type s), is that I needed a type
variable which did not change (I believe the Haskell people call it rigid),
so I decided to use type constructors. Another option, previously
implemented, was to use polymorphic variables, ie:

let rec foo : 'a. 'a t -> t =
    function
        | IntLit x -> x


However, this has several disadvantages, the biggest of which is that  the
variable 'a cannot be referenced inside the expression since its scope is
the type in which it was introduced.




> It's also a bit difficult to know what's the big deal about "exhaustiveness
> checks". As I understand it, you remark that with GADTs some case cannot
> happen due to typing reasons, but the exhaustive check doesn't know about
> it. Could you be a bit more explicit about what the exhaustiveness checker
> does :
> - is it exactly the same behavior as before, ignoring GADT specificities ?
> (ie. you haven't changed anything)
> - if not, what have you changed and how can we try to predict its reaction
> to a given code ?
> - what can we do when it doesn't detect an impossible case ? I suppose we
> can't a pattern clause for it, as the type checker would reject it.
>
>
This problem is not new in O'Caml. For example:

# type t = { x : 'a . 'a list } ;;
type t = { x : 'a. 'a list; }
# let _ = function { x = [] } -> 5;;
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
{x=_::_}

however, try creating a value of type ('a. 'a list) satisfying the pattern _
:: _

What I've done is written a second pass to the exhaustiveness checker. The
first pass does the same thing as before, but ignores GADTs completely. The
second pass exhaustively checks every possible generalized constructor
combination.

For example, in the code

type 'a t = Foo : int t | Bar : bool t | Baz : float t

let f : type s. s t * s t * s t -> s =
    function
         Foo, Foo, Foo
      | ....

My code will check all 9 possible patterns and will output any which were
missed. The pattern returned by my algorithm is a valid pattern.


> I'm not sure I understand the example of the "Variance" section.
> Why is the cast in that direction ? It seems to me that even if we could
> force t to be covariant, this cast (to a less general type) shouldn't work :
>
>   # type +'a t = T of 'a;;
>   # let a = T (object method a = 1 end);;
>   # (a :> < m : int; n : bool > t);;
>   Error: Type < a : int > t is not a subtype of < m : int; n : bool > t
>
>
I apologize, that should be:

type -'a t = C : < m : int > -> < m : int > t

or, as a constraint:

type -'a t = C of 'a constraint 'a = < m : int >


> Again, you "Objects and variants" and "Propagation" subsections are a bit
> vague. Could you give example of code exhibiting possible problems ?
>
>
Propagation:

Currently, this code doesn't compile:

    let rec baz : type s . s t -> s =
      fun (type z) ->
function
    IntLit x -> x : s
  | BoolLit y -> y : s

so you need to add the annotation:

    let rec baz : type s . s t -> s =
      fun (type z) ->
((function
    IntLit x -> x
  | BoolLit y -> y) : s t -> s)

objects (and polymorphic variants):

the following will not compile:

    let rec eval : type s . s t -> s =
      function
| IntLit x -> ignore (object method m : s = failwith "foo" end : < m : int;
..>) ; x

polymorphic variants in patterns:

the following will not compile:

    let rec eval : type s . [`A] * s t -> unit =
      function
| `A, IntLit _ -> ()
| `A, BoolLit _ -> ()


> Finally, a few syntax trolls, in decreasing order of constructivity :
>
> - is it a good idea to reproduce the "implicit quantification" of ordinary
> types ? It seems it could be particularly dangerous here.
>   for example, changing
>     type _ t = Id : 'a -> 'a t
>   to
>     type 'a t = Id : 'a -> 'a t | Foo of 'a
>   introduce, if I'm not mistaken, a semantic-changing variable captures.
>   (I thought other dark corners of the type declarations already had this
> behavior, but right now I can't remember which ones)
>

type 'a t = Id : 'a -> 'a t | Foo of 'a

is the same as

type 'b t = Id : 'a -> 'a t | Foo of 'b

In other words, the type variables in generalized constructor definitions
are distinct from the type parameters.


>
> - if I understand it correctly, (type a . a t -> a) is yet another syntax
> for type quantification. Why ? I thought (type a) was used to force
> generalization, but ('a . ...)-style annotation already force polymorphism
> (or don't they ?). Is it a semantic difference with ('a . 'a t -> 'a), other
> than its interaction with gadts ? Can we use (type a . a t -> a) in all
> places where we used ('a . 'a t -> 'a) before ?
>

(type s) does not force generalization (see above); this is why this new
syntax is needed. You can use (type a . a t -> a) anywhere you used ('a. 'a
t -> 'a) could before, assuming that you don't have any types a that you
don't want hidden. This syntax extension is purely syntactic sugar.


>
> - is there a rationale for choosing Coq-style variant syntax instead of
> just adding a blurb to the existing syntax, such as
>     | IntLit of int : int t
>   or
>     | IntList of int return int t
>   ?
>
>
The only rationale is that I want to make it clear that the type variables
found inside generalized constructor definitions are distinct from the type
parameters. In your second example, return is not a keyword in O'Caml. I
could very well have chosen your first example. If there is a consensus on
some alternate syntax, I have no qualms about changing it.

Thank you for the feedback. I will add some of these things to my webpage.

Sincerely,

Jacques Le Normand


> Thanks.
>

> On Mon, Oct 25, 2010 at 10:39 AM, Jacques Le Normand <rathereasy@gmail.com
> > wrote:
>
>> Dear Caml list,
>>
>> I am pleased to announce an experimental branch of the O'Caml compiler:
>> O'Caml extended with Generalized Algebraic Datatypes. You can find more
>> information on this webpage:
>>
>> https://sites.google.com/site/ocamlgadt/
>>
>>
>> And you can grab the latest release here:
>>
>> svn checkout https://yquem.inria.fr/caml/svn/ocaml/branches/gadts
>>
>>
>>
>>
>> Any feedback would be very much appreciated.
>>
>> Sincerely,
>>
>> Jacques Le Normand
>>
>>
>> _______________________________________________
>> Caml-list mailing list. Subscription management:
>> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>> Archives: http://caml.inria.fr
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>>
>>

[-- Attachment #2: Type: text/html, Size: 14482 bytes --]

Re: [Caml-list] Generalized Algebraic Datatypes

[Dario Teixeira]

Hi,

> I am pleased to announce an experimental branch of the O'Caml compiler:
> O'Caml extended with Generalized Algebraic Datatypes. You can find more
> information on this webpage:

More in depth feedback will come after proper digestion; for now let me
just say these are great news!  And I'm sure there are other Ocaml users
out there who will be glad to finally get rid of some of the Obj.magic
blemishes in their code...

Best regards,
Dario Teixeira

Re: [Caml-list] Generalized Algebraic Datatypes

[bluestorm]

[-- Attachment #1: Type: text/plain, Size: 3908 bytes --]

It's very interesting.

First, I'm curious of the "historical" aspects of this work : where does it
come from ? Apparently there is work from you and Jacques Garrigue, but it's
hard to tell. Is it new, or a long-running experiment ?

In your "intuition" section (btw. there is a typo here, it should be (type
s) (x : s t)), you seem to present GADT as directly related to the new (type
s) construct. It's a bit surprising because it's difficult to know the
difference between this and classic type variables. I suppose it is because
only (type s) guarantee that the variable remains polymorphic, and you use
that to ensure that branch-local unifications don't "escape" to the outer
level ? Could you be a bit more explicit on this ?

It's also a bit difficult to know what's the big deal about "exhaustiveness
checks". As I understand it, you remark that with GADTs some case cannot
happen due to typing reasons, but the exhaustive check doesn't know about
it. Could you be a bit more explicit about what the exhaustiveness checker
does :
- is it exactly the same behavior as before, ignoring GADT specificities ?
(ie. you haven't changed anything)
- if not, what have you changed and how can we try to predict its reaction
to a given code ?
- what can we do when it doesn't detect an impossible case ? I suppose we
can't a pattern clause for it, as the type checker would reject it.

I'm not sure I understand the example of the "Variance" section.
Why is the cast in that direction ? It seems to me that even if we could
force t to be covariant, this cast (to a less general type) shouldn't work :

  # type +'a t = T of 'a;;
  # let a = T (object method a = 1 end);;
  # (a :> < m : int; n : bool > t);;
  Error: Type < a : int > t is not a subtype of < m : int; n : bool > t

Again, you "Objects and variants" and "Propagation" subsections are a bit
vague. Could you give example of code exhibiting possible problems ?

Finally, a few syntax trolls, in decreasing order of constructivity :

- is it a good idea to reproduce the "implicit quantification" of ordinary
types ? It seems it could be particularly dangerous here.
  for example, changing
    type _ t = Id : 'a -> 'a t
  to
    type 'a t = Id : 'a -> 'a t | Foo of 'a
  introduce, if I'm not mistaken, a semantic-changing variable captures.
  (I thought other dark corners of the type declarations already had this
behavior, but right now I can't remember which ones)

- if I understand it correctly, (type a . a t -> a) is yet another syntax
for type quantification. Why ? I thought (type a) was used to force
generalization, but ('a . ...)-style annotation already force polymorphism
(or don't they ?). Is it a semantic difference with ('a . 'a t -> 'a), other
than its interaction with gadts ? Can we use (type a . a t -> a) in all
places where we used ('a . 'a t -> 'a) before ?

- is there a rationale for choosing Coq-style variant syntax instead of just
adding a blurb to the existing syntax, such as
    | IntLit of int : int t
  or
    | IntList of int return int t
  ?


Thanks.

On Mon, Oct 25, 2010 at 10:39 AM, Jacques Le Normand <rathereasy@gmail.com>
 wrote:

> Dear Caml list,
>
> I am pleased to announce an experimental branch of the O'Caml compiler:
> O'Caml extended with Generalized Algebraic Datatypes. You can find more
> information on this webpage:
>
> https://sites.google.com/site/ocamlgadt/
>
>
> And you can grab the latest release here:
>
> svn checkout https://yquem.inria.fr/caml/svn/ocaml/branches/gadts
>
>
>
> Any feedback would be very much appreciated.
>
> Sincerely,
>
> Jacques Le Normand
>
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

[-- Attachment #2: Type: text/html, Size: 6095 bytes --]

Re: [Caml-list] Generalized algebraic datatypes

[Gabriel Kerneis]

On Mon, Apr 28, 2008 at 01:35:06AM -0400, Jacques Le Normand wrote:
> Does ocaml support Generalized Algebraic datatypes? 

No.

> If not, are there any caml based compilers that support it?

Some pieces of software (e.g. Ocsigen), which need GADT, use (very
carefuly crafted) "black magic" (Obj.magic) to get things compiled. 
You could probably do this in your "toy compiler", put you will loose 
the benefit of Ocaml's type-checking.

Regards,
-- 
Gabriel Kerneis