Re: [Caml-list] ambitious proposal: polymorphic arithmetics

["Jacques Carette" <carette@mcmaster.ca>]

Richard Jones <rich@annexia.org> wrote:

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

GADTs have non-uniform input *and* output types.  But the non-uniformity still has enough regularity to it that this 
does not give full sub-typing or dependent types (both of which are much harder).  They are a really beautiful 
extension of algebraic types in the 'dependent types' direction without introducing anything harder than what is 
already present in the type system.  The chapter by Pottier and Re'my in ATTAPL pretty much admits that in writing ;-) 
 So maybe the Ocaml developers have been working hard on this for ocaml 3.09, they just didn't want to tip their hats 
quite yet... 

Certainly GADTs are sufficient for statically typing an embedded language *and* [the important part] its 'cannot go 
wrong' interpreter that follows purely from the operational semantics.  The leap from that to controlled, non ad hoc 
polymorphic + seems quite small.

So if the types on which you are working are tagged, then GADTs could well help.  Of course, for performance and 
historical reasons, int are not tagged in Ocaml, so that is a definite problem.  But perhaps the 'untagging' of 
integers is done late enough in the compilation process (I don't know!) that it is not a real problem.

Jacques