English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Re: [Caml-list] Polymorphic Variants and Number Parameterized Typ es
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2002-04-30 (15:18)
From: Francois Pottier <francois.pottier@i...>
Subject: [Caml-list] Re: Encoding "abstract" signatures


On Tue, Apr 30, 2002 at 12:34:26PM +0200, Andreas Rossberg wrote:
> How do you express
>     functor F (X : sig module type T end) (Y : X.T) = (Y : X.T)
> without parameterizing over the set of existentially quantified variables
> somehow? I had in mind something like (again assuming non-applicative
> functors, because they are much simpler):
>     LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts).
>         pack Y as exists ts:k.S(ts)

You make the functor F polymorphic in the number of type components
defined by the signature S. As far as I understand, this is made
necessary by the desire to hide these types in the functor's result
(i.e. the pack operation).

It seems to me that it is simpler to suppress the pack operation,
i.e. to return Y instead of (pack Y as ...). Then, instead of
quantifying separately over S and ts, you only need to quantify
over S(ts), that is, T, as follows:

  val F : forall T. T -> T

I must say I don't know exactly what is lost with this simplification;
is there a loss of abstraction? The answer isn't obvious to me. But it
seems to offer a simple understanding of the above O'Caml specification.

François Pottier
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners