Re: [Caml-list] Polymorphic Variants and Number Parameterized Types

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

Hi François,

> > Note that Russo showed [1] that you can actually get rid of dependent
> > typing and interpret ML modules (without nested signatures) as a lambda
> > calculus with higher-order polymorphism (i.e., definitely not
> > simply-typed). The basic idea is to view functors as functions
> > polymorphic over their type arguments.
> 
> This interesting idea was also developed by Mark Jones:

IIRC, he does not consider generative functors, though.

> > In this setting, adding abstract signatures would at least require adding
> > polymorphic kinds, I believe.
> 
> What do you mean? In this encoding, modules are only records, so module types
> are ordinary types, and there is no distinction between ordinary abstract
> types (introduced by explicit polymorphic abstraction) and ``abstract
> signatures''. There is, as far as I can tell, no need for kind polymorphism.

Well, if you have a functor like

	F : functor(X : sig module type S  module Y:S end) -> ...

then it would be polymorphic in an unknown number of types. To capture
this, you had to make the functor polymorphic in the kind carrying the
record of abstract types bound in S (i.e. you would also need record
kinds). Something along the lines of:

	F : forall k. forall S:*. forall ts:k. {Y:S} -> ...

The application

	F (struct module type S = sig type t type u val x : t end 
	          module Y = struct type t = int
	                            type u = bool
	                            val x = 7 end
	   end)

corresponds to something like

	F {t:*,u:*} {x:int} {t=int,u=bool} {Y={x=7}}

I'm being sketchy here, of course, since I haven't thought about it in
real depth. It probably gets even messier when you go higher-order:
consider signatures projected from an applicative functor, for example.
In that case you might even need quantifiers on the kind level to encode
it. Also, the kind k should be restricted to record kinds, so you want
some subkinding discipline (or row polymorphism on the kind level? ;-).

Well, and somewhere in that mess we must have taken the step into the
realms of undecidable subtyping (because if it encodes OCaml modules it
must be undecidable).

Cheers,

	- Andreas
-- 
Andreas Rossberg, rossberg@ps.uni-sb.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 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