Re: [Caml-list] Modules and typing

[Francois Pottier <francois.pottier@inria.fr>]

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