[Caml-list] Re: New GADT iteration

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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