Tweeted twitter.com/StackCompSci/status/1025803975654887424
2 edited body
source | link

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 int with bool is allowed, then unify bool and int must also be definedallowed, 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.

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 int with bool is allowed, then unify bool and int must also be defined, 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.

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 int with bool is allowed, then unify bool and 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.

1
source | link

Hindley-Milner type inference for language with implicit type casting

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 int with bool is allowed, then unify bool and int must also be defined, 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.