[Caml-list] questions on type representations

[Caml-list] questions on type representations

[skaller]

I have some questions on typing:
one is Ocaml specific and the others seek generic
design advice.

First I exhibit my encoding of types in Felix:

(** value typing *)
type 't b0typecode_t' = 
  [
  | `BTYP_name of bid_t         
  | `BTYP_inst of bid_t * 't list 
  | `BTYP_tuple of 't list         
  | `BTYP_sum of 't list            
  | `BTYP_function of 't * 't
  | `BTYP_pointer  of 't 
  | `BTYP_void                       
  | `BTYP_binding of 't * 't 
  | `BTYP_fix of int      
  | `BTYP_var of bid_t     
  ]

(** meta typing *)
type 't b1typecode_t' =
  [
  | `BTYP_apply of 't * 't 
  | `BTYP_typefun of (int * 't) list * 't * 't
  | `BTYP_type
  | `BTYP_type_tuple of 't list
  ]

(** general typing *)
type 't btypecode_t' =
  [
  | 't b0typecode_t'
  | 't b1typecode_t'
  ]

type b0typecode_t = 't b0typecode_t' as 't
type btypecode_t = 't btypecode_t' as 't

--------------------------------------------
Some notes. a bid_t is a unique identifier,
actually an alias for 'int'. It is used to
refer to generative types.

`BTYP_inst (index, [t1, t2, .. tn])

refers to an instance of a generative type which has been
indexed by types, for example vector[int]: the current instantiation
is like a C++ template -- done entirely at compile time.

`BTYP_fix depth

is my inverted fixpoint binder. It specifies the 
point of recursion, with an implicit fixpoint binder
'depth' levels up in the structure. (well, -depth actually :(

Finally: Felix doesn't have type inference, only
synthetic deduction: function argument types must
always be given, although return types may be omitted.
This is because Felix supports overloading.

QUESTION 1. (polymorphic variant issue)
----------------------------------------

For this system, the Ocaml typing using a parameter
works fine to obtain covariant typing for plain types
and types extended with meta types.

Unfortunately, i need the equivalent mechanism in 
other places, for example I have statements, and 
statements extended by macro statemants. The problem
is that there are about 6 other types involved:
patterns and expressions being two of them.

This makes the above trick with fixpoints to obtain
covariance very ugly. Is there another way?
Could there be some syntactic sugar OR language
extension to alleviate this problem?

[I actually tried to apply the technique to statements
and i got so totally lost I gave up. The transformation
is purely mechanical, but the result is totally unreadable.]


QUESTION 2 (design issue)
-------------------------

There are actually 2 types of type variable in use
in Felix, but they are not distinguished in the type
encoding shown above. They are:

(a) unknown types of variables and function returns
(b) instantiable type variables

Variables of type (a) must be calculated by the compiler.
They're unknowns, not variables. Variables of type (b)
must be instantiated by the user. [explicitly or by 
unification of an argument with a generic function
signature]

In addition, I plan 2 other kinds of variables:

(c) dynamic variables under pointers. which can't be dereferenced
(d) fully dynamic variables

Variables under pointers which can't be dereferenced
are equivalent to Ocaml boxed types. The C++ representation
will be void*. This allows run time polymorphism of the kind
for which the following algorithm admits a single encoding:

	fun [T1, T2] swap (a : &T1, b : &T2) = { return (b,a); }

Fully dynamic variables remove the 'under a pointer' restriction.
They will work by passing Run Time Type Information [RTTI]
in the form of a descriptor which allows an object to be
copied (assigned, etc ..).

Thus I have 4 distinct kinds of type variables,
but only one encoding. Should I use distinct encodings?

There is a clear downside, namely routines such as unification
become considerably more complex with 4 kinds of type variable.
On the other hand the lack of distinction makes it harder to
detect errors and implement the representation.

QUESTION 3 . (design issue)
--------------------------

I have unified the ordinary type encoding
with both lambda expressions and meta typing 
(kinding). Should I? Or is it better to make one or
both of these distinct types?

Note: `BTYP_type is the kind of an ordinary type,
so that, `BTYP_type -> `BTYP_type is the kind
of a type function. encoded `BTYP_typefun _ ..

I can't kind that at the moment: Should `BTYP_type 
should have a level argument: 

	`BTYP_type of int

or is it better (possible?) to avoid a heirarchy
of kinding levels?

Another question is: is there an advantage
to lazy evaluation of type lambdas?
[I currently use eager evaluation]

QUESTION 4 (design issue)
-------------------------

Felix has Modules and Interfaces,
and also Functors (a module parameterised
by an Interface). Both modules and interfaces
are currently generative, however function
instances are not: like C++, you can use
an anonymous functor application, the system
tracks all the instantiations.

[Note to anyone examining the actual code: 
I got it wrong. I track the module and interface,
instead of the module and functor.

the typing:

	`BTYP_binding (upper,lower)

is used for a module:interface coercion
so that the type checking is done with
component 'upper', but the code generator
uses the representation type 'lower'.
Unlike Ocaml, I can't discard the representation
because not all type in Felix have a uniform
representation (no boxing ..)]

I think I actually need:

	`BTYP_binding (binding_index, interface_index)

where binding_index specifies the interface -> module
mapping. (eg 'type t -> int')

In Ocaml, on the other hand, modules and functors
are generative, but interfaces (signatures) are not.
Ocaml requires a functor application to be named
to make the functor/argument binding generative.

I think it is possible to track functor/argument
pairs, bypassing this restriction. Why doesn't
Ocaml do that? [Separate compilation problem?]

--------------------------------
Any comments appreciated on any of this.
Also any pointers to papers or actual code
that may be useful (especially for the kinding
and lamba calculations)



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