I refer to the C++ example given above. Because of the hidden module type (hidden outside the module), functions can't be applied to the module from the outside. They can only be injected and need to be converted (instantiated ) by the module itself. An instantiated function then makes a change from A->B to M[A->B] . The conversion step postponed, we want to use the function like this:
* M[A](A->B) => M[B] So,With the help of A->B, we can modify/update/extend the module. What type has M[A]? We obtain: * M[A] :: M[(A->B)->B] ...Presumed that the instantiation of A->B succeeds. How does it look like with the template calc in the C++ program? We have: calc :: (all T) T[_,v] -> T[v,v] (all T) is the universally bound T, so there is no free T in calc and (all T) is a scope delimiter. Therefore, an instantiated T will not affect the global type environment. v is a value with a value type V that depends on T, e.g. v :: T.V . For simplification, we treat values and terms as singletons here, the stand for themselves, so v :: v or N :: N . Now, if we bind T to MS (MS is available in the module) * calc :: ((all T; T=MS) T[_,v] -> T[v,v]) * calc :: ((all T; T=MS) MS[_,v] -> MS[v,v]) With v:: MS.V abbrev. v :: V : * calc :: MS[(_,V) -> (V,V)] success.... now we can apply the instantiated calc to the module with calc(this). Furthermore, MS contains a member a :: N. calc works exactly the same way here, but with a different instantiation: * calc :: ((all T; T=N) N[_,v] -> N[v,v]) We just modeled abstraction and implemented the existential quantifier at the same time. * Mitchell, Plotkin (1988) : "Abstract types have existential type" (it is regarded as a seminal paper) Now , we could add many functions the same way. The typing doesn't change if we implement functions directly without using a template. Abstraction means hidden quantifiers - even if we don't see them. We could go further than that. How are modules related to each other? Do they allow for subtyping, instantiation subtyping, composition etc. ? These derivations become possible, if we resort to higher order unification. First order unification (like Hindley-Milner) might work too, but not in general.
