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:   (:) 
From:  Andreas Rossberg <AndreasRossberg@w...> 
Subject:  Re: [Camllist] Re: Encoding "abstract" signatures 
François, Francois Pottier <francois.pottier@inria.fr> 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). This is just one reason. More generally, it's the need for a coherent encoding in the higherorder setting we face. If we say that type functor(X : sig type t val x : t end) > ... maps to something like forall t. t > ... then consequently functor(Y : sig module type T end) > ... > functor(X : Y.T) > ... must map to some type that yields the above as the result of some sequence of applications. We need to be polymorphic in the form of the quantification to achieve that. So even by ignoring type abstraction you cannot avoid the problem. But if you replace "type" by "module type" in the above argument signature you see why there actually cannot be an encoding with the desired properties: the encoding of the latter type also had to contain quantifiers for all potential *kind arguments* induced by applying an argument with nested signatures. There is no fixed point for the level of abstractions we had to do, unless we allowed for dependent types at some level. > 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. Well, besides the aforementioned problems, you don't represent type abstraction at all (which, I would argue, is a central feature)  the functor in question would not differ from functor F (X : sig module type T end) (Y : X.T) = Y Or was your question about abstraction in some other sense?  Andreas  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