Re: [Camllist] Polymorphic Variants and Number Parameterized Typ es
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20020430 (15:18) 
From:  Francois Pottier <francois.pottier@i...> 
Subject:  [Camllist] Re: Encoding "abstract" signatures 
Andreas, 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 nonapplicative > 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 Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners