CODEWITHSUNDEEP
typessmlsmlnj
James
James

Reputation: 1289

How does the compiler determine types in sml

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?

Upvotes: 3

Views: 365

Answers (1)

sshine
sshine

Reputation: 16105

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.

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 : t1
  • f : t1 → bool
  • if ... : t1

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

  • b : t1

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

  • f (raise Break) : bool
  • t1 = 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

Upvotes: 5

Related Questions