[TYPES] Issues regarding typeclasses and modular languages like ML

[Brian Hulley]

Dear Derek,

Thanks for taking the time to write such a detailed reply, and especially for the explanation of partial application in terms of full instantiation to unification variables followed (modulo value restriction) by re-generalization, which shows that MTC is indeed much more applicable (no pun intended) than I had thought. (This was also pointed out to me off-list by another kind person.)

I'm still not sure about the treatment of coherence, since it seems that the purpose of the using declarations in section 3.1 is to prevent ambiguity arising via type inference, whereas I'd have thought that even with fully annotated types for all structure components, coherence would still be a problem, i.e. that there are very deep reasons why Haskell requires only one instance per type, but I have not been able to think up an example to demonstrate this at the moment. This is one area where it is possible that the lack of first class polymorphism in ML (due to the value restriction due in turn to the unsound generalization rule of HM TI) may just possibly be masking an issue by ruling out the interesting cases by construction.

Regarding the Pi notation, clearly my understanding of GHCi's treatment of the types of (f) and (g) in:

  let f x y = show y
  let g = f 'c'

was wrong, but if one were to consider a language where the type of (f) is represented internally by:

  Pi (t : *) . Pi (x : t) . Pi (a : * | Show a) . Pi (y : a) . String

then the binding to (g) would have the type:

  Pi (a : * | Show a) . Pi (y : a) . String

The important thing here is that there is no full instantiation followed by re-generalization - the binding to (g) simply supplies the first 2 args of (f). There is therefore no need (afaict) in such a language for a value restriction or separation of effects via monads (this becomes an orthogonal issue) since there is no generalization rule to introduce unsoundness.

In contrast, the MTC type system seems to require the HM concept of full instantiation followed (if possible) by re-generalization in order to allow an MTC polymorphic type to be formulated as a functor application yielding a structure with a monomorphic value component. In order to integrate something like MTC into my language I would have to find a different technical formulation like the Pi notation above, to avoid having to have a generalization rule.

In any case there's lots of stuff to be thinking about ;-)

Thanks again,

Brian.