Version française
Home     About     Download     Resources     Contact us    
Browse thread
Formal specifications of programming languages
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Christophe Raffalli <christophe.raffalli@u...>
Subject: Re: [Caml-list] Formal specifications of programming languages
Jacques Carette a écrit :
> Jacques Garrigue wrote:
>> (Actually, abstract types in modules can also be seen as existentials,
>> but I don't think this is what you are talking about.)
>>   
> This is a subtle issue that I have yet to understand 'completely'.  
> Can you expand on this "can also be seen as existentials" please?
>
> To me, there seems to be a difference between these, but I have never 
> been able to quite put my finger on it.  It may be because they are 
> not really different, ie both can encode the other.
> This is not just an idle question.  In two separate papers (with 
> co-authors), abstract types in module types (and Functors) are used as 
> what I think of as "constrained existentials", to good effect.  But 
> maybe I really ought to think of those as "for all types that can be 
> used as implementations of this signature" rather than "some 
> _specific_ type that satisfies this signature".  I say 'specific' 
> because while users of the module cannot see the implementation, 
> inside the implementation, the actual representation is rather crucial.
Abstract types are existential types with a projecton operator (like a 
choice operator) and they can have contraints. Unfortunatly, modules are 
not first class and you can not do a list of modules with the same 
signature but distinct implementation for their abstract types. This is 
the lack of first class modules that prevent to encode existential types 
using abstract types.

The best to do is to use universal types in records with "the usual dual 
encoding" as said by J. Garrigues.

Do not forget that an abstract type occurring in the signature of an 
argument to a functor is a universal type because it is "negated" ...

>
> Jacques Carette
>
> _______________________________________________
> 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