I've only implemented the HM algorithm on a small academic language with a few primitive types and functions. In that case, the unification algorithm would return a type error if two different primitive types were given. For example, if statements unify their condition with primitive type
bool, producing the following results:
if (true) ... // type safe if ("5") // type error, cannot unify string and bool
I've now been tasked to implement a type inference algorithm on a language that allows type casting on primitive types. For example, one cast is
int -> bool such that
if(5) ... is now a valid expression.
The problem is, I can't figure out how to adapt the unify algorithm. Specifically, I'm stuck on dealing with the one directional nature of type casts, e.g.
int -> bool is defined, but
bool -> int is not. The unify algorithm has no notion of direction. Unifying type
a and type
b is the same as unifying type
b and type
a. So in the case of the if statement, if I say that unify
bool is allowed, then unify
int must also be allowed, and suddenly the statement
true + false is type safe.
I've searched for details of existing type systems that do this, but unfortunately I've only found resources that either show a basic HM inference algorithm similar to the first one I implemented, or are completely off topic.