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

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

[Krishnaswami, Neel]

Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> Neel Krishnaswami wrote:
> 
> > There's no recursion in the module system because that would break
> > the termination guarantee. If you think of modules as records, and
> > functors as lambda abstractions, you can see that the module system
> > defines a simply-typed lambda calculus. As you've noticed with C++, 
> > adding recursion to it would mean you can write nonterminating module
> > expressions. (All this is wonderfully clearly explained in 
> > the paper, "A modular  module system".)
> 
> I'm not sure about "simply-typed". Did the situation change since
> that of http://caml.inria.fr/archives/199907/msg00027.html ?

Wow! I didn't even know that was possible. I thought that typechecking
record subtyping was decidable...?

--
Neel Krishnaswami
neelk@cswcasa.com
-------------------
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

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

[Andreas Rossberg]

"Krishnaswami, Neel" wrote:
> 
> Pascal Cuoq [mailto:pascal.cuoq@inria.fr] wrote:
> > Neel Krishnaswami wrote:
> >
> > > There's no recursion in the module system because that would break
> > > the termination guarantee. If you think of modules as records, and
> > > functors as lambda abstractions, you can see that the module system
> > > defines a simply-typed lambda calculus. As you've noticed with C++,
> > > adding recursion to it would mean you can write nonterminating module
> > > expressions. (All this is wonderfully clearly explained in
> > > the paper, "A modular  module system".)
> >
> > I'm not sure about "simply-typed". Did the situation change since
> > that of http://caml.inria.fr/archives/199907/msg00027.html ?
> 
> Wow! I didn't even know that was possible. I thought that typechecking
> record subtyping was decidable...?

Well, module types are (a limited form of) dependent types. What
concretely triggers undecidability of subtyping in OCaml is the presence
of abstract module types, at least in combination with the
contravariance of higher-order functors.

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. In this setting, adding abstract
signatures would at least require adding polymorphic kinds, I believe.

[1]

@inproceedings{Russo:NonDependentTypes,
  author	= "Claudio Russo",
  title		= "Non-Dependent Types for {Standard} {ML} Modules",
  booktitle	= "International Conference on Principles and
                   Practice of Declarative Programming",
  address	= "Paris, France",
  year		= 1999,
  month		= sep,
}

-- 
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

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

[Francois Pottier]

Hi,

> 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:

  @InProceedings{jones-96,
    author       = "Mark P. Jones",
    title        = "Using Parameterized Signatures to Express Modular
		   Structure",
    booktitle    = "Proceedings of the 23rd {ACM} Symposium on Principles
		   of Programming Languages",
    publisher    = "ACM Press",
    month        = jan,
    year         = "1996",
    address      = "St. Petersburg Beach, Florida",
    note         = "\url{http://www.cse.ogi.edu/~mpj/pubs/paramsig.html}",
  }

as well as (in a couple of much more technical papers) by Zhong Shao.

> 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.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

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

[Andreas Rossberg]

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

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

[Francois Pottier]

Hi Andreas,

On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote:
> 
> 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.

Perhaps our views differ. What I gathered from Jones' and Russo's
papers was that modules do not contain types. So, the module type
S cannot be a component of X; rather, the type of the functor F
will be universally quantified over S. This leads me to something
like:

  F : forall S. functor (X : S) -> ...

where the distinction between X and Y is eliminated, because it
becomes superfluous. In fact, the `functor' syntax and the name
X are just sugar, since a functor is a function. So I would really
write

  F : forall S. 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 would simply apply

  F { x : int } { x = 7 }

or, perhaps (if abstraction is desired)

  F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t })

So, in this example, we seem to need neither higher kinds nor
kind polymorphism. But perhaps my encoding doesn't have the
features you'd wish?

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

[Caml-list] Modules and typing

[John Max Skaller]

.. I ask a dumb question, and some very interesting stuff
I don't understand is exchanged

So here's another one :-)

Previously, I saw a reference to a paper, but I've lost it, and it may
be relevant to me. In Ocaml, a type in a module

   type t = int (* for example *)

can be hidden by binding a type in a signature

  type t

to it. That works, it seems to me, because all types have the same
size (usually a pointer) so the abstract type has enough information
for the code generator to do the right thing.

If one is using expanded types, the basic type system is inadequate,
somehow the concrete type has to be 'attached' to the abstract one,
so that the type checker uses the abstract one, and the code
generator the concrete one, and manipulations in between preserve
the link. In the Felix type system, I have such a type combinator,
and functions to extract the two parts...

Unfortunately, I don't have a proper calculus for dealing with
these type pairs. I seem to recall someone mentioned a paper
in which types were considered as functors (??) for just this purpose,
and some calculus developed. Does anyone recall the mention
of the paper or happen to have a URL for it?

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

[Caml-list] Encoding "abstract" signatures

[Andreas Rossberg]

Francois Pottier <francois.pottier@inria.fr> wrote:
>
> On Mon, Apr 29, 2002 at 06:48:11PM +0200, Andreas Rossberg wrote:
> >
> > 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.
>
> Perhaps our views differ. What I gathered from Jones' and Russo's
> papers was that modules do not contain types.

Yes. But Russo describes how you can encode ML module types in such a
setting (Jones was not interested in that, AFAIR). As long as you don't have
nested signatures you can recover the full expressiveness of functors
(including generativity) by just using universal and existential
quantification.

(For other readers: the module type

    functor(X : sig type t val x : t end) -> sig type u val y : u end

can be encoded as

    forall t. {x:t} -> exists u. {y:u}

Well, with OCaml's applicative functors you had to lift the existential
quantifier, but you get the idea.)

What I was saying is that this encoding does not easily extend to the full
OCaml module system, because abstract signatures pose a problem: the number
of quantifiers you have to generate in the encoding is not fixed. I
reckonned some more complex kind system and kind polymorphism might enable
you to recover their expressiveness. But I am not at all sure (see below).

> So, the module type
> S cannot be a component of X; rather, the type of the functor F
> will be universally quantified over S. This leads me to something
> like:
>
>   F : forall S. functor (X : S) -> ...
>
> where the distinction between X and Y is eliminated, because it
> becomes superfluous. In fact, the `functor' syntax and the name
> X are just sugar, since a functor is a function. So I would really
> write
>
>   F : forall S. 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 would simply apply
>
>   F { x : int } { x = 7 }
>
> or, perhaps (if abstraction is desired)
>
>   F (exists t,u.{ x : t }) (pack { x = 7 } as exists t,u.{ x : t })
>
> So, in this example, we seem to need neither higher kinds nor
> kind polymorphism. But perhaps my encoding doesn't have the
> features you'd wish?

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)

(Oops, I got the kind of S wrong in my previous posting).

But as I said I did not think about it much, so I have no idea whether this
really scales. In particular, when you nest signatures you might hit the
same problem of an unfixed number of quantifiers, but for kinds. In fact, I
am pretty certain it does not fly, because nested signatures essentially
give you Type:Type, i.e. you'd most likely need an infinite hierarchy of
universes...

    - Andreas
-------------------
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

Re: [Caml-list] Modules and typing

[Francois Pottier]

Hi,

On Tue, Apr 30, 2002 at 08:04:49PM +1000, John Max Skaller wrote:

> That works, it seems to me, because all types have the same
> size (usually a pointer) so the abstract type has enough information
> for the code generator to do the right thing.

This is correct. This problem arises not only with abstract types, but more
generally, in any programming language that has polymorphism. The most common
solutions to the data representation issue are

 + adopt a uniform representation (e.g. everything-is-a-pointer), as in O'Caml

 + require that abstract types are pointer types, as in Modula-3 (?) and, more
   recently, Cyclone

 + pass type information around at runtime, as in the TIL/ML compiler

 + adopt two representations, a uniform (boxed) one and a specialized (unboxed)
   ones, and insert coercions in your code to switch between the two, as in one
   of Xavier Leroy's papers

 + adopt specialized representations only, duplicating polymorphic functions
   if they have to be used at several types whose representations differ

As far as I can tell, you are interested in exploring the last option.
Then, you essentially need to annotate type variables (and abstract types)
with a kind, that is, with enough information to determine its concrete
representation. A kind could be, for instance, a size (e.g. 1 or 2 words)
and a register type (integer or floating-point). Then, code that depends
on a type variable (or on an abstract type) can be compiled, provided its
kind is known. In the case of abstract types, the kind would probably need
to be mentioned in a module's interface.

In the case of polymorphic functions, it is possible to perform kind
specialization automatically, that is, a function such as

  let f x = x

can be first given a kind- and type-polymorphic specification:

  val f: forall k. forall 'a : k. 'a -> 'a

then specialized for several kinds k1, k2, etc.

  val f1 : forall 'a : k1 -> 'a
  val f2 : forall 'a : k2 -> 'a

Each of these functions can then be compiled, since the kind of 'a
determines the calling conventions for the function (e.g. which
register the parameter x is found in).

I am aware that I am not directly answering your question, but I hope
these ideas help. It seems that it's easier to reason in terms of kinds
than in terms of (abstract type, concrete type) pairs -- indeed, the
whole point of abstraction is that the concrete type is usually not
known, unless you're doing whole-program compilation.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

[Caml-list] Re: Encoding "abstract" signatures

[Francois Pottier]

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 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
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Modules and typing

[John Max Skaller]

Francois Pottier wrote

>
>This is correct. This problem arises not only with abstract types, but more
>generally, in any programming language that has polymorphism. The most common
>solutions to the data representation issue are
>
> + adopt a uniform representation (e.g. everything-is-a-pointer), as in O'Caml
>
> + require that abstract types are pointer types, as in Modula-3 (?) and, more
>   recently, Cyclone
>
> + pass type information around at runtime, as in the TIL/ML compiler
>
> + adopt two representations, a uniform (boxed) one and a specialized (unboxed)
>   ones, and insert coercions in your code to switch between the two, as in one
>   of Xavier Leroy's papers
>
> + adopt specialized representations only, duplicating polymorphic functions
>   if they have to be used at several types whose representations differ
>
>As far as I can tell, you are interested in exploring the last option.
>
Yes. More precisely, in finding a hybrid system which permits
superior performance without losing too much generality.
I support pointers, so it should be possible
for a single specialisation of a polymorphic function
to be use where all the type variable are under a pointer.

I currently expand products, but sum types use tagged pointers.
And as you might guess from previous postings .. I have a problem
with type recursion where the term under the fixpoint binder
is a product (since that may lead to an infinitely large data structure).
The equi-recursive (tree) model doesn't work here.

>
>Then, you essentially need to annotate type variables (and abstract types)
>with a kind, that is, with enough information to determine its concrete
>representation. A kind could be, for instance, a size (e.g. 1 or 2 words)
>and a register type (integer or floating-point). 
>
The actual model is: the kind is another type. Primitive types are
annotated with the C++ type that represents them, the programmer writes:

    type int = "long";

to say that the Felix type "int" is represented by the C++ type "long".
Other kinds (in your terminology) are determined by binding
modules with signatures like:

    interface X { type t; }
    module Y { type t = int; }
    Z = Y : X;

where the "kind" of the abstract type X.t is bound to Y.t = int, and the 
type
system carries the annotation so that the type of Z.t is (Y.t, int).
I have two functions:

    lift (x,y) |-> x
    drop (x,y) |-> y

The difficulty is I need a calculus. For example:

    (x,y) -> (a,b)  reduces to  (x->a, y->b)

In other words, I need to know how to carry the kind annotations around
during reductions on the types: this is simplified, since the annotations
themselves are types .. (at least, I hope that simplifies it).

>Then, code that depends
>on a type variable (or on an abstract type) can be compiled, provided its
>kind is known. In the case of abstract types, the kind would probably need
>to be mentioned in a module's interface.
>
In the current model, as illustrated above, modules don't have interfaces
per se: instead, you have to bind an interface to a module, and *that*
creates the type/kind pair.

>
>I am aware that I am not directly answering your question,
>
heh .. a complete answer would require you to write the
code for me  .. I'm looking for a way to manage the problem ..

> but I hope
>these ideas help. It seems that it's easier to reason in terms of kinds
>than in terms of (abstract type, concrete type) pairs -- indeed, the
>whole point of abstraction is that the concrete type is usually not
>known, unless you're doing whole-program compilation.
>
Yes. Because I use types for kinds, I think I have been confusing
them: that representation is useful, since the same calculus can be
used for both, but it confuses reasoning, and your model provides
a way to decouple them.

My situation is even more confused because Iintroduced
modules after the basic system was already running, and so there
are terms for both plain and annotated types, and the code
handles all the combinations separately .. I should remove
plain type terms, and annotate them all.. but I don't want
to break working code, so I need to be sure the operations
on annotated types are right first ... which I'm not, because
I don't yet have a coherent theory. Anyhow thanks!

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850




-------------------
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

Re: [Caml-list] Modules and typing

[Noel Welsh]

--- John Max Skaller <skaller@ozemail.com.au> wrote:
> Francois Pottier wrote
> 
> > + adopt specialized representations only,
> duplicating polymorphic functions
> >   if they have to be used at several types whose
> representations differ
> >
> >As far as I can tell, you are interested in
> exploring the last option.
> >
> Yes.

I believe MLTon does this, at the cost of no separate
compilation.

Noel

__________________________________________________
Do You Yahoo!?
Yahoo! Health - your guide to health and wellness
http://health.yahoo.com
-------------------
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

Re: [Caml-list] Re: Encoding "abstract" signatures

[Andreas Rossberg]

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 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).

This is just one reason. More generally, it's the need for a coherent
encoding in the higher-order 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 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

Re: [Caml-list] Modules and typing

[Francois Pottier]

Hello,

Noel Welsh wrote:

> > adopt specialized representations only,
> > duplicating polymorphic functions
> > if they have to be used at several types whose
> > representations differ
> 
> I believe MLTon does this, at the cost of no separate
> compilation.

MLton does a bit more than that, really. It specializes *all* polymorphic
code, so that, after the transformation, the program can be typed in a
monomorphic type discipline. My suggestion, on the other hand, was to
duplicate polymorphic code only on a ``per-kind'' basis; for instance, if
all product types are of kind POINTER and (unboxed) integers are of kind
INT, then a polymorphic function (say, the identity) that is used at types
(say) int * int, float * float and int would only be compiled twice. I
believe this would severely limit the ``code size explosion'' problem
that is sometimes feared when doing monomorphization.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Re: Encoding "abstract" signatures

[Francois Pottier]

On Wed, May 01, 2002 at 03:19:29PM +0200, Andreas Rossberg wrote:
> 
> This is just one reason. More generally, it's the need for a coherent
> encoding in the higher-order 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).

> 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

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.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Re: Encoding "abstract" signatures

[Andreas Rossberg]

Hi François,

Francois Pottier wrote:
> 
> > This is just one reason. More generally, it's the need for a coherent
> > encoding in the higher-order 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 first-class (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 eta-expansion 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.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

Re: [Caml-list] Re: Encoding "abstract" signatures

[Francois Pottier]

Andreas,

> So you cannot simply `reuse' T's quantifier.

You're right -- it seems difficult to obtain a compositional encoding of
O'Caml's module system. We would need, in the target system, one universal
quantification over a type of record kind to be somehow equivalent to a series
of universal quantifications over types of base kind. I guess that's what you
were saying from the very start, but it took me a while to see the problem.
It would be interesting to devise a type system that has this property. Didier
Rémy noticed the need for such a feature back in 1994 when writing `Dynamic
typing in polymorphic languages' (see section 4.2 of the SRC tech report). I
don't think he has a polished solution, though.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
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

Re: [Caml-list] Re: Encoding "abstract" signatures

[Andreas Rossberg]

François,

> It would be interesting to devise a type system that has this property. Didier
> Rémy noticed the need for such a feature back in 1994 when writing `Dynamic
> typing in polymorphic languages' (see section 4.2 of the SRC tech report).

Ah, indeed, he is discussing something quite similar. Interesting.

But I strongly suspect that even a system like that wouldn't be enough
to encode OCaml's modules. Consider that higher-order type again:

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

The idea was representing this as

    Forall k. forall T:(k->*). forall ts:k. T(ts) -> ...  (*)

But that is still not good enough, because we might apply

    T = sig module type U module type V end

The result had to be something like

    Forall k1. Forall k2. forall U:(k1->*). forall V:(k2->*). ...

so (*) is not an appropriate encoding -- application may also result in
an indefinite number of kind quantifiers. We might try to tackle that by
introducing another universe of "hyperkinds" and repeat the same trick.
But unfortunately, that just pushes the problem to yet another level --
no finite number of additional universes will help, because what OCaml
provides with nested abstract signatures is essentially Type:Type.

So I conjecture that it is impossible to faithfully encode OCaml's
modules into a non-dependent system (which comes to no surprise taking
into account that it is known to be undecidable).

-- 
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