Re: [Caml-list] Generalized Algebraic Datatypes
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 darioteixe...@yahoo.comwrote:
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
___
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
Re: [Caml-list] Generalized Algebraic Datatypes
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 darioteixe...@yahoo.comwrote:
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
___
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
Re: [Caml-list] Generalized Algebraic Datatypes
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 ___ 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
Re: [Caml-list] Generalized Algebraic Datatypes
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 ___ 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
Re: [Caml-list] Generalized Algebraic Datatypes
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 ___ 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
Re: [Caml-list] Generalized Algebraic Datatypes
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 ___ 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
Re: [Caml-list] Generalized Algebraic Datatypes
On Mon, Oct 25, 2010 at 6:44 PM, bluestorm bluestorm.d...@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
