Double vision
rec module X1 : S1 = M1
and moudle X2 : S2 = M2
M1 : struct
type t = int
let x : t = 42
let y = g(x)
t != X.t
Type cyclic definitions
Recursive signature wellformedness
- xavier’s proposal
- problem: with applicative functors
- inside S2: you can have
F(X1)- works only with the full signature ofX1
- inside S2: you can have
abstraction
- hide things
- unify two different implementations
- _applicative functors_ ⇒ more than Derek
initialization of rec modules
also, in terms of applicative functors
-
OCaml: it fails, dynamic tests, safe
-
dynamic checks?
-
the idea: correctly detect field by field dependency, instead of module by module (OCaml does)
-
in terms of cross-submodule-init-dependency, more issues can be there
-
which relates to the problem of mixins (also related to initialization)
F(Y : S ... / { ... requires .. } )
The current
- well-formedness checker
- bug typechecker: first build the skelmton, then
- two styles of applicative functors
- transparent existentials: enable you to create a body, abstract something, then make it a functor