[Caml-list] Modules and typing

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

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