How to infer coercions?

Question

I would like to know how to infer coercions (a.k.a. implicit conversions) during type inference. I am using the type inference scheme described in Top Quality Type Error Messages by Bastiaan Heeren, but I'd assume that the general idea is probably the same in all Hindley-Milner-esque approaches.

It seems like coercion could be treated as a form of overloading, but the overloading approach described in this paper doesn't consider (at least not in a way I could follow) overloading based on requirements that the context places on return type, which is a must for coercions. I'm also concerned that such an approach might make it difficult to give priority to the identity coercion, and also to respect the transitive closure of coercibility. I can see sugaring each coercible expression, say e, to coerce(e), but sugaring it to coerce(coerce(coerce(... coerce(e) ...))) for some depth equal to the maximum nesting of coercions seems silly, and also limits the coercibility relation to something with a finite transitive closure whose depth is independent of the context, which seems (needlessly?) restrictive.

Answer 1

I hope you get some good answers to this.

I haven't yet read the paper you link to but it sounds interesting. Have you looked at all how ad-hoc polymorphism (basically overloading) works in Haskell? Haskell's type system is H-M plus some other goodies. One of those goodies is type classes. Type classes provide overloading, or as Haskeller's call it, ad-hoc polymorphism.

In GHC, the most widely used Haskell compiler, the type classes are implemented by passing dictionaries at run-time. The dictionary lets the run-time system do a lookup from type to implementation. Supposedly, jhc can use super-optimization to pick the right implementation at compile time but I'm skeptical it handles the fully polymorphic cases that Haskell can allow and I know of no formal proofs or papers asserting the correctness.

It sounds like your type inference will run into the same problems as other rank-n polymorphic approaches. You may well want to read some of the papers here for additional background: Scroll down to "Papers about types" His papers are haskell specific but the type theoretic stuff should be meaningful and useful to you.

I think this paper about rank-n polymorphism and the type checking issues should spark some interesting thoughts for you: http://research.microsoft.com/~simonpj/papers/higher-rank/

I wish I could provide a better answer! Good luck.