Re: circular types?

[Tom Hirschowitz <hirschow@mouton.inria.fr>]

Hendrik Tews <tews@tcs.inf.tu-dresden.de> :

> - If I want to program a function typecheck (which recursively
> walks down formulas, expressions, and types) I separate it into
> typecheck_formula, typecheck_expression, etc and put these
> functions into the respective files. Will there be lightweight
> syntax for the forward declaration of typecheck_expression in
> file formula.ml similar to what you used for the types above? 

Yes. You'll have to specify the type of deferred functions in each 
module.
For example,


   ========== file expression.ml
   
   ? type formula
   
   type expression =
     | Abstraction of (string * types) list * expression
     ....
     | Formula of formula

   ? val typecheck_formula : formula -> ...

   let rec typecheck_expression = ...
   
   ===================================
   
   ========== file formula.ml
   
   ? type expression
   
   type formula = 
     | Forall of (string * types) list * formula
     ...
     | Expression of expression
   
   
   ? val typecheck_expression : expression -> ...

   let rec typecheck_formula = ...

   ===================================
   
   ========== file next.ml
   
   module MyTypes = Types + Expression + Formula;;
   
   ...
   
   ===================================
 

should work.


> - Assume another module that uses typecheck_formula, does it have
> to "open" Formula or Next? 

Other modules using those functions have to open Next, 
because before the merging, none of those functions or types 
is really defined.
For instance, the type checker refuses "Formula.typecheck_expression".

> - How about link order? The mixin module is linked after all
> modules it mixes and all modules that use something of file
> formula or expression have to be linked after the mixing module?

I really don't know, haven't worked on it yet.
But one module should be able to be mixed with many others.
Assume you want to test two strategies for type-checking expressions, 
you would use the same Formula module for both. 
Does it fix any link order anyway?

> - (Impatiently) In which ocaml release can I expect the mixing
> modules?

Not yet for sure!
Ocaml v 24.12? 
Xavier?