RE: [Caml-list] Modules and typing

RE: [Caml-list] Modules and typing

[Gregory Morrisett]

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

Actually, Cyclone has two different kinds of abstract types:
One abstracts pointer types (really, types that are compatible
with void*) and another kind that abstracts any type.  The latter
kind can only be used under a pointer.  I think this corresponds more 
closely to what Modula-3 provides with it's notion of "ref"
types.  

There's another option that you didn't mention which is the approach
taken by Ada:  Have a notion of "private" types in interfaces, e.g.

  type t
  [private t = int]

The client is type-checked with t treated abstractly, but the 
compiler can then specialize the client knowing what the implementation
of t is.  Of course, by leaking this information into the interface,
you're effectively losing separate compilation in the sense that
if the implementation of t changes, then its interface must also
change and all clients must then be (potentially) re-compiled.  But
this is a simple option which avoids some of the complexity that
you run into if you try to use abstract kinds to classify types
according to implementation details that a compiler might need
(e.g., size, calling-convention, and alignment constraints.)

-Greg

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

Gregory Morrisett wrote:

>
>There's another option that you didn't mention which is the approach
>taken by Ada:  Have a notion of "private" types in interfaces, e.g.
>
>  type t
>  [private t = int]
>
>The client is type-checked with t treated abstractly, but the 
>compiler can then specialize the client knowing what the implementation
>of t is.  Of course, by leaking this information into the interface,
>you're effectively losing separate compilation in the sense that
>if the implementation of t changes, then its interface must also
>change and all clients must then be (potentially) re-compiled.  
>
Ocaml object system does this. Very confusing it is too,
seeing the private data in the interface .. but it is a good system,
because it is possible to abstract that data away by a further
abstraction. A large class of clients can work solely with the
abstraction .. not all because of the covariance problem ..
and those that can don't need recompilation when the representation
changes.

The biggest pain in this model is that one has to cut and paste
a lot during development... and also the lack of inter-recursion
between classes and type means you have to encode the abstraction
as a parameterised class type and then instantiate it within
the type recursion.

But the beauty of it is that at the cost of one pointer
(to the object) the abstraction allows intermodule
recursion.. the order of class compilation is irrelevant
provided only that the abstractions are introduced first.

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

[Benedikt Grundmann]

> >  + require that abstract types are pointer types, as in 
> > Modula-3 (?) and, more
> >    recently, Cyclone
> 
> Actually, Cyclone has two different kinds of abstract types:
> One abstracts pointer types (really, types that are compatible
> with void*) and another kind that abstracts any type.  The latter
> kind can only be used under a pointer.  I think this corresponds more 
> closely to what Modula-3 provides with it's notion of "ref"
> types.  
> 
> There's another option that you didn't mention which is the approach
> taken by Ada:  Have a notion of "private" types in interfaces, e.g.
> 
>   type t
>   [private t = int]
> 
> The client is type-checked with t treated abstractly, but the 
> compiler can then specialize the client knowing what the implementation
> of t is.  Of course, by leaking this information into the interface,
> you're effectively losing separate compilation in the sense that
> if the implementation of t changes, then its interface must also
> change and all clients must then be (potentially) re-compiled.  But
> this is a simple option which avoids some of the complexity that
> you run into if you try to use abstract kinds to classify types
> according to implementation details that a compiler might need
> (e.g., size, calling-convention, and alignment constraints.)
> 
> -Greg

Another option related to this is to generate a compiler only interface file
(maybe even binary).  Which contains everything the compiler needs to know
about the implementation of an interface.  Everything mentioned above applies
to this solution too, with the added benefit that a reader of the interface
can't make stupid assumptions about the implementation which might not be true
in the next release :-)


Bene

-- 
GMX - Die Kommunikationsplattform im Internet.
http://www.gmx.net

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

[Gurr, David (MED, self)]

Hi, the .cmx files generated by ocamlopt do some of
what you mention.  -D

> -----Original Message-----
> From: Benedikt Grundmann [mailto:bgrundmann@gmx.net]
> Sent: Thursday, May 02, 2002 5:31 AM
> To: Gregory Morrisett
> Cc: Francois.Pottier@inria.fr; skaller@ozemail.com.au;
> caml-list@inria.fr
> Subject: RE: [Caml-list] Modules and typing
> 
> 
> > >  + require that abstract types are pointer types, as in 
> > > Modula-3 (?) and, more
> > >    recently, Cyclone
> > 
> > Actually, Cyclone has two different kinds of abstract types:
> > One abstracts pointer types (really, types that are compatible
> > with void*) and another kind that abstracts any type.  The latter
> > kind can only be used under a pointer.  I think this 
> corresponds more 
> > closely to what Modula-3 provides with it's notion of "ref"
> > types.  
> > 
> > There's another option that you didn't mention which is the approach
> > taken by Ada:  Have a notion of "private" types in interfaces, e.g.
> > 
> >   type t
> >   [private t = int]
> > 
> > The client is type-checked with t treated abstractly, but the 
> > compiler can then specialize the client knowing what the 
> implementation
> > of t is.  Of course, by leaking this information into the interface,
> > you're effectively losing separate compilation in the sense that
> > if the implementation of t changes, then its interface must also
> > change and all clients must then be (potentially) re-compiled.  But
> > this is a simple option which avoids some of the complexity that
> > you run into if you try to use abstract kinds to classify types
> > according to implementation details that a compiler might need
> > (e.g., size, calling-convention, and alignment constraints.)
> > 
> > -Greg
> 
> Another option related to this is to generate a compiler only 
> interface file
> (maybe even binary).  Which contains everything the compiler 
> needs to know
> about the implementation of an interface.  Everything 
> mentioned above applies
> to this solution too, with the added benefit that a reader of 
> the interface
> can't make stupid assumptions about the implementation which 
> might not be true
> in the next release :-)
> 
> 
> Bene
> 
> -- 
> GMX - Die Kommunikationsplattform im Internet.
> http://www.gmx.net
> 
> -------------------
> 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
-------------------
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 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

[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

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

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