From: Christophe Raffalli <christophe.raffalli@univ-savoie.fr>
To: Jacques Carette <carette@mcmaster.ca>
Cc: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>,
caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Formal specifications of programming languages
Date: Mon, 18 Feb 2008 22:52:21 +0100 [thread overview]
Message-ID: <47B9FE15.4090900@univ-savoie.fr> (raw)
In-Reply-To: <47B9B5D9.5010303@mcmaster.ca>
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
prev parent reply other threads:[~2008-02-18 21:48 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-02-13 18:22 Andrej Bauer
2008-02-13 18:27 ` [Caml-list] " Christopher L Conway
2008-02-13 19:45 ` Andrej Bauer
2008-02-14 9:00 ` Jacques Garrigue
2008-02-14 9:08 ` Xavier Leroy
2008-02-15 14:30 ` Christopher L Conway
2008-02-18 10:05 ` Jacques Garrigue
2008-02-18 16:44 ` Jacques Carette
2008-02-18 21:52 ` Christophe Raffalli [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=47B9FE15.4090900@univ-savoie.fr \
--to=christophe.raffalli@univ-savoie.fr \
--cc=caml-list@yquem.inria.fr \
--cc=carette@mcmaster.ca \
--cc=garrigue@math.nagoya-u.ac.jp \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).