<p>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 <a href="http://people.cs.uu.nl/bastiaan/phdthesis/index.html" rel="noreferrer">Top Quality Type Error Messages</a> by Bastiaan Heeren, but I'd assume that the general idea is probably the same in all Hindley-Milner-esque approaches.</p>

<p>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 <em>e</em>, to coerce(<em>e</em>), but sugaring it to coerce(coerce(coerce(... coerce(<em>e</em>) ...))) 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.</p>

[{'answer_id': 69770, 'author': 'willurd', 'author_id': 1943957, 'author_profile': 'https://Stackoverflow.com/users/1943957', 'pm_score': 0, 'selected': False, 'text': "<p>Could you give a little more clarification as to what exactly it is you're asking?</p>\n\n<p>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) <em>NewType(object)</em>, or 2) <em>object as NewType</em>.</p>\n\n<p>From an implementation standpoint I imaging every class should define it's own ways of converting to whichever types it <em>can</em> convert to (an Array can't really convert to an integer...or can it?). For example, if you try <em>Integer(myArrayObject)</em>, 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.</p>\n\n<p>My entire answer could be totally off though :-D Let me know if this isn't what you're looking for</p>\n"}, {'answer_id': 69787, 'author': 'Jason Dagit', 'author_id': 5113, 'author_profile': 'https://Stackoverflow.com/users/5113', 'pm_score': 2, 'selected': False, 'text': '<p>I hope you get some good answers to this.</p>\n\n<p>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.</p>\n\n<p>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, <a href="http://repetae.net/computer/jhc/" rel="nofollow noreferrer">jhc</a> 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.</p>\n\n<p>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: <a href="http://research.microsoft.com/~simonpj/" rel="nofollow noreferrer">Scroll down to "Papers about types"</a>  His papers are haskell specific but the type theoretic stuff should be meaningful and useful to you.</p>\n\n<p>I think this paper about rank-n polymorphism and the type checking issues should spark some interesting thoughts for you: <a href="http://research.microsoft.com/~simonpj/papers/higher-rank/" rel="nofollow noreferrer">http://research.microsoft.com/~simonpj/papers/higher-rank/</a></p>\n\n<p>I wish I could provide a better answer!  Good luck.</p>\n'}, {'answer_id': 2048127, 'author': 'mayfly', 'author_id': 223690, 'author_profile': 'https://Stackoverflow.com/users/223690', 'pm_score': 1, 'selected': False, 'text': "<p>My experience is that sugaring every term intuitively seems unattractive, but is worth pursuing.</p>\n\n<p>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.</p>\n\n<p>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.</p>\n\n<p>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.</p>\n\n<p>Say we have an input script: <code>foo x</code></p>\n\n<p>Then, after sugaring, this becomes: <code>(coerce foo) (coerce x)</code> </p>\n\n<p>Where, informally:</p>\n\n<pre><code>coerce :: a -&gt; b\ncoerce x = REDUCE (cast x) if a and b are incompatible\nx                          otherwise\n</code></pre>\n\n<p>Thus <em>coerce</em> is either identity or an application of <em>cast</em> where <em>b</em> is the return type for a given context.</p>\n\n<p><em>cast</em> can now be treated as a type class method, e.g.</p>\n\n<pre><code>class Cast a, b where {cast :: a -&gt; b };\n-- ¬:: is an operator, literally meaning: don’t cast\n--(!) is the reduction operator. Perform one stage of reduction.\n\n-- Reduce on demand\ninstance Cast Exp c, c where { inline cast = ¬::(!)(\\x::(Exp c) -&gt; ¬::(!)x) };\n</code></pre>\n\n<p>The <code>¬::</code> annotations are used to suppress the coerce syntactic sugaring.</p>\n\n<p>The intention is that other instances of <code>Cast</code> can be introduced to extend the range of conversions, although I haven't explored this.  As you say, overlapping instances seem necessary.</p>\n"}]
['https://Stackoverflow.com/questions/69711', 'https://Stackoverflow.com', 'https://Stackoverflow.com/users/11173/']