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

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

[Dario Teixeira]

Hi,

> If I misunderstood you, then I still misunderstand you: the App
> constructor you quoted took only 1 "argument" (a pair), so you can't
> "partially apply it", and that's from the type declaration.
> IOW the type declaration you quoted is *not* curried.

Now I get what you mean, and there's definitely been a misunderstanding.
First, I wasn't referring to constructor App in particular, nor confusing
a tuple argument with a curried form.  I may be abusing the term, but
I used "partial application" in the most general sense, ie, including
an application with zero arguments (in other words, a first-class value).

Suppose I had the following type declaration:

  val f: int -> int -> int -> int

I could do a partial application with 2 arguments:

  let f2 = f 1 2

A partial application with 1 argument:

  let f1 = f 1

And generalising, a "partial application" with 0 arguments, which
is simply referring to f itself:

  let f0 = 0

Now, going back to the GADTs example, a declaration such as the one
below hints that the constructors may be used as first-class values
(a zero-arg "partial application"), when in fact they cannot.  That
is why I find this syntax to be inconsistent with the rest of the
language.

type _ t =
  | IntLit : int -> int t
  | BoolLit : bool -> bool t


Best regards,
Dario Teixeira

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] 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: [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: [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

[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

[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

[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 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

[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

[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 --]