Re: [Caml-list] Modules and typing

[John Max Skaller <skaller@ozemail.com.au>]

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