Re: [Caml-list] Formal specifications of programming languages

[Jacques Carette <carette@mcmaster.ca>]

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.

Jacques Carette