Re: ambitious proposal: polymorphic arithmetics

[Ethan Aubin <ethan.aubin@pobox.com>]

Gadts can do for all sorts of cool things. For example, an approach to
simulate type classes with gadts see
http://www.cs.bu.edu/~hwxi/GRecTypecon/PAPER/main.pdf, to create a
statically typed printf see
http://www.cs.bu.edu/~hwxi/academic/papers/popl03.pdf

Hongwei Xi and Tim Sheard's papers have tons of interesting examples
in their publications. I hope some ideas from their languages, ATS and
Omega respectively, trickle down to Ocaml.

> On Wed, Apr 06, 2005 at 08:43:01PM +0400, Dmitry Lomov wrote:
>> Richard Jones wrote:
>> >The problem, I'm guessing, is that you add polymorphic +, -, and so
>> >on.  But that's really just a hack in the language.  Sooner or later
>> >people are going to ask why it's not possible to write a polymorphic
>> >'print' function, _without_ hacking the language some more.  At that
>> >point you need a theory, and you need something like G'Caml, or type
>> >classes, or GADTS.
>> 
>> Pardon my ignorance, but how are GADTs are going to help in this regard?
>> I thought GADTs are basically data types with constructors that have
>> non-uniform "return type".

> Pardon _my_ ignorance.  I read something about using GADTs to simulate
> class types in the paper, and assumed that they are equivalent, but
> I'm probably wrong.

Also, sorry for any duplicate post.