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

Could you give a little more clarification as to what exactly it is you're asking?

I have a slight idea, and if my idea is right then this answer should suffice as my answer. I believe you're talking about this from the perspective of someone who's creating a language, in which case you can look at a language like ActionScript 3 for an example. In AS3 you can typecast two different ways: 1) NewType(object), or 2) object as NewType.

From an implementation standpoint I imaging every class should define it's own ways of converting to whichever types it can convert to (an Array can't really convert to an integer...or can it?). For example, if you try Integer(myArrayObject), and myArrayObject does not define a way of converting to and Integer, you can either throw an exception or let it be and simply pass in the original object, uncasted.

My entire answer could be totally off though :-D Let me know if this isn't what you're looking for

Answer 2

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.

Answer 3

My experience is that sugaring every term intuitively seems unattractive, but is worth pursuing.

An interest in persistent storage has led me by a circuitous route to consider the problems of mixing expression and atomic values. To support this, I decided to separate them completely in the type system; thus Int, Char etc. are the type constructors only for integer and character values. Expression types are formed with the polymorphic type constructor Exp; e.g. Exp Int refers to a value which reduces in one step to Int.

The relevance of this to your question arises when we consider evaluation. At an underlying level, there are primitives which require atomic values: COND, addInt etc. Some people refer to this as forcing an expression, I prefer to see it simply as a cast between values of different types.

The challenge is to see if this can be done without requiring explicit reduction directives. One solution is exactly as you suggest: i.e. to treat coercion as a form of overloading.

Say we have an input script: foo x

Then, after sugaring, this becomes: (coerce foo) (coerce x)

Where, informally:

coerce :: a -> b
coerce x = REDUCE (cast x) if a and b are incompatible
x                          otherwise

Thus coerce is either identity or an application of cast where b is the return type for a given context.

cast can now be treated as a type class method, e.g.

class Cast a, b where {cast :: a -> b };
-- ¬:: is an operator, literally meaning: don’t cast
--(!) is the reduction operator. Perform one stage of reduction.

-- Reduce on demand
instance Cast Exp c, c where { inline cast = ¬::(!)(\x::(Exp c) -> ¬::(!)x) };

The ¬:: annotations are used to suppress the coerce syntactic sugaring.

The intention is that other instances of Cast can be introduced to extend the range of conversions, although I haven't explored this. As you say, overlapping instances seem necessary.