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:  20020502 (09:30) 
From:  Andreas Rossberg <rossberg@p...> 
Subject:  Re: [Camllist] Re: Encoding "abstract" signatures 
Hi François, Francois Pottier wrote: > > > 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. > > Oh, I see what you mean. It's a good point. But still I think I can encode > the second functor as > > forall T. () > T > ... > > (where (), the empty structure type, corresponds to Y and T corresponds to X) > which, when applied to an empty structure, yields > > forall T. T > ... > > as expected (provided the ``forall'' quantifier doesn't get in the way of > application, i.e. polymorphic instantiation and abstraction are transparent, > as in ML). OK, consider applying module type T = sig type t type u val x : t * u end Then, in the encoding, application should yield the result type forall t,u. t * u > ... So you cannot simply `reuse' T's quantifier. Also note that in general the quantifier(s) in question might be buried deep inside the RHS of the arrow, even in contravariant position. (Moreover, it is not obvious to me whether we could use implicit type application, because polymorphism is firstclass (a field or argument of functor type would be polymorphic)). > > functor in question would not differ from > > > > functor F (X : sig module type T end) (Y : X.T) = Y > > Indeed it wouldn't. But I fail to see the point; if Y's type is X.T, > there is no difference between Y and (Y : X.T), is there? The two > functors in question have the same type in O'Caml. Ah, yes, you are right, I forgot about that. Actually, I see that as an unfortunate limitation of OCaml's module typing: it has to forget some sharing because it lacks proper singleton types (and thus loses principality). Ideally, the type of the above variant of F should be functor(X : sig module type T end) > functor(Y : X.T) > that Y where I write "that Y" for the singleton type inhabited by Y only (a subtype of X.T). That functor is essentially the polymorphic identity functor, while the other variation was a polymorphic etaexpansion of the abstraction operator. But in fact, what that means is that in OCaml both functors must be represented by a type with an existential quantifier. Otherwise you would not witness any difference between module expressions M and F (struct module type T = ABSTRACT_SIG_OF_M end) (M)  Andreas Rossberg, rossberg@ps.unisb.de "Computer games don't affect kids; I mean if Pac Man affected us as kids, we would all be running around in darkened rooms, munching magic pills, and listening to repetitive electronic music."  Kristian Wilson, Nintendo Inc.  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