How does the compiler determine types in sml

Question

I've been given the following code and I've been asked to determine the type.

exception Break;
fn f => fn a => fn b =>
    (f(raise Break)
       handle Break => if (f a) then a else raise Break)
          handle Break => if not(f a) then a else b;

I know that this function takes in f, a and b and outputs a in all instances so it must be equivelant to:

fn f => fn a => fn b => a

which has the type:

'a -> 'b -> 'c -> 'b

because 'if( f a)' we can derive that 'a must be a function that takes in type 'b and outputs a boolean otherwise it wouldn't work.

('b->bool) -> 'b -> 'c -> 'b

re done so 'a is the beginning:

('a->bool) -> 'a -> 'b -> 'a

is what I get from this for my final answer. However when I type it out in the command prompt I get the following type:

(bool->bool) -> bool -> bool -> bool

what am I missing? At what point does 'a and 'b (from my final type evaluation) specialize to bool?

score 5 · Accepted Answer · edited May 23 '17 at 11:58

How does the compiler determine types in sml

Standard ML uses Damas-Hindley-Milner type inference, but there are several algorithms for resolving the most general type, notably Algorithm W. The type-inference rules are explained in e.g.

A Generalized Let-Polymorphic Type Inference Algorithm [PS], which actually mainly presents an alternative Algorithm G that is more efficient, but the introduction is very easy to read and gives a full example of inferring the type of a small expression.
So you still don't understand Hindley-Milner?, which introduces just enough type theory to explain the StackOverflow question "What part of Milner-Hindley do you not understand?".

At what point does 'a and 'b specialize to bool?

The exact point at which 'a and 'b specialize to bool depends on the algorithm used. I will jump ahead and skip some steps where expressions are given types and those types are unified.

When it says if (f a) then a else raise Break, then

a : t₁
f : t₁ → bool
if ... : t₁

And similarly, when it says if not (f a) then a else b, we additionally have that

b : t₁

Lastly, f (raise Break) handle Break => if ... then a else ... gives us that

f (raise Break) : bool
t₁ = bool, since f (raise Break) and if ... then a else ... must have the same type.

The part you were missing was probably to realize that for x handle ... => y, x and y must have the same type. Otherwise you would have an expression that changes type depending on whether an exception is thrown. That is not possible when types are resolved during compilation and exceptions are thrown at run-time. A practical example where this is relevant is negative tests, where the type on the left side of handle ... is forced to be that of the right side:

val factorial_robust_test = (factorial -1; false)
                            handle Domain => true
                                 | Overflow => false
                                 | _ => false

How does the compiler determine types in sml

1 Answers1

Linked