[Caml-list] New GADT iteration

[Caml-list] New GADT iteration

[Jacques Garrigue]

Dear Camlers,

Some of you may already be aware that GADTs are available in trunk,
since this summer. Information is available here:
      https://sites.google.com/site/ocamlgadt/

As you can see in the presentation, this first iteration had some
limitations (particularly it was mostly incompatible with objects and
polymorphic variants), which led us to try a new approach.

In this new iteration it is guaranteed that an ambiguous type cannot
escape the scope of a GADT pattern-matching, which leads to
(hopefully) more intuitive type inference, and allows to combine GADTs
with objects and polymorphic variants. The syntax is unchanged.

As this approach depends crucially on the above property of ambiguous
types not escaping, it requires as much testing as possible.
This is why I would like to invite interested people to test it and
report strange behavior.
The new code is in the branch  branches/gadts-devel, or
  http://caml.inria.fr/cgi-bin/viewcvs.cgi/ocaml/branches/gadts-devel/

Sample code is available in the subdirectory testsuite/tests/typing-gadts.
It includes Alain Frisch's example for safe type introspection,
extended with variants.

Please tell me if you find some unsoundness, or you cannot understand
why you get an error.

Jacques Garrigue

Re: [Caml-list] New GADT iteration

[Gabriel Kerneis]

On Fri, Nov 11, 2011 at 04:57:07PM +0900, Jacques Garrigue wrote:
> Some of you may already be aware that GADTs are available in trunk,
> since this summer. Information is available here:
>       https://sites.google.com/site/ocamlgadt/

I think there is a typo on this page: in the function length, the case
| Cons (a,b) -> length b
should be
| Cons (a,b) -> 1 + length b

The repository location is also flawed; instead of
        svn checkout http://caml.inria.fr/caml/svn/ocaml/trunk
it should be
        svn checkout http://caml.inria.fr/svn/ocaml/branches/gadts-devel
(note the spurious "caml" in the current url).

Best regards,
-- 
Gabriel Kerneis

Re: [Caml-list] New GADT iteration

[Jacques Le Normand]

fixed

On Fri, Nov 11, 2011 at 3:24 AM, Gabriel Kerneis <kerneis@pps.jussieu.fr> wrote:
> On Fri, Nov 11, 2011 at 04:57:07PM +0900, Jacques Garrigue wrote:
>> Some of you may already be aware that GADTs are available in trunk,
>> since this summer. Information is available here:
>>       https://sites.google.com/site/ocamlgadt/
>
> I think there is a typo on this page: in the function length, the case
> | Cons (a,b) -> length b
> should be
> | Cons (a,b) -> 1 + length b
>
> The repository location is also flawed; instead of
>        svn checkout http://caml.inria.fr/caml/svn/ocaml/trunk
> it should be
>        svn checkout http://caml.inria.fr/svn/ocaml/branches/gadts-devel
> (note the spurious "caml" in the current url).
>
> Best regards,
> --
> Gabriel Kerneis
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

Re: [Caml-list] New GADT iteration

["Markus W. Weißmann"]

I've added a port "ocaml-devel" to MacPorts that builds the gadt-devel branch (checked out from svn, revision 11273);
so for users of MacPorts you can simply deactivate your current ocaml installation and install ocaml-devel to give it a try.

$> sudo port -f deactivate ocaml
$> sudo port install ocaml-devel 

The ocaml libraries from MacPorts will not accept the development snapshot though.


Best regards

-Markus

On 11 Nov 2011, at 08:57, Jacques Garrigue wrote:

> Dear Camlers,
> 
> Some of you may already be aware that GADTs are available in trunk,
> since this summer. Information is available here:
>      https://sites.google.com/site/ocamlgadt/
> 
> As you can see in the presentation, this first iteration had some
> limitations (particularly it was mostly incompatible with objects and
> polymorphic variants), which led us to try a new approach.
> 
> In this new iteration it is guaranteed that an ambiguous type cannot
> escape the scope of a GADT pattern-matching, which leads to
> (hopefully) more intuitive type inference, and allows to combine GADTs
> with objects and polymorphic variants. The syntax is unchanged.
> 
> As this approach depends crucially on the above property of ambiguous
> types not escaping, it requires as much testing as possible.
> This is why I would like to invite interested people to test it and
> report strange behavior.
> The new code is in the branch  branches/gadts-devel, or
>  http://caml.inria.fr/cgi-bin/viewcvs.cgi/ocaml/branches/gadts-devel/
> 
> Sample code is available in the subdirectory testsuite/tests/typing-gadts.
> It includes Alain Frisch's example for safe type introspection,
> extended with variants.
> 
> Please tell me if you find some unsoundness, or you cannot understand
> why you get an error.
> 
> Jacques Garrigue
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> 

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
Tel. +49 (89) 2 89-1 81 05
Fax +49 (89) 2 89-1 81 07
http://wwwknoll.in.tum.de/

[Caml-list] Re: New GADT iteration

[Jacques Garrigue]

The new branch has now been merged in trunk, all ready for the next version of OCaml.

	http://caml.inria.fr/cgi-bin/viewcvs.cgi/ocaml/trunk

Big thanks to Jeremy Yallop for finding many bugs.
But you still have your chance to find more :-)

Jacques Garrigue

On 2011/11/11, at 16:57, Jacques Garrigue wrote:

> Dear Camlers,
> 
> Some of you may already be aware that GADTs are available in trunk,
> since this summer. Information is available here:
>      https://sites.google.com/site/ocamlgadt/
> 
> As you can see in the presentation, this first iteration had some
> limitations (particularly it was mostly incompatible with objects and
> polymorphic variants), which led us to try a new approach.
> 
> In this new iteration it is guaranteed that an ambiguous type cannot
> escape the scope of a GADT pattern-matching, which leads to
> (hopefully) more intuitive type inference, and allows to combine GADTs
> with objects and polymorphic variants. The syntax is unchanged.
> 
> As this approach depends crucially on the above property of ambiguous
> types not escaping, it requires as much testing as possible.
> This is why I would like to invite interested people to test it and
> report strange behavior.
> The new code is in the branch  branches/gadts-devel, or
>  http://caml.inria.fr/cgi-bin/viewcvs.cgi/ocaml/branches/gadts-devel/
> 
> Sample code is available in the subdirectory testsuite/tests/typing-gadts.
> It includes Alain Frisch's example for safe type introspection,
> extended with variants.
> 
> Please tell me if you find some unsoundness, or you cannot understand
> why you get an error.
> 
> Jacques Garrigue