Sml Church numeral type inference

Question

I have this expression in SML and need to find the most general type of it. When run through the compiler I get what it shows below. How would I go about finding what the most general type would be of not only this function but other functions like church numerals function "two".

val one = fn f => (fn x => f x)

Why is the type of this:

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

Answer 1

I don't really understand your question, so I am just guessing ...

If I define the first church numeral functions in the REPL:

val c0 = fn f => fn x => x
val c1 = fn f => fn x => f x
val c2 = fn f => fn x => f (f x)
val c3 = fn f => fn x => f (f (f x))
val c4 = fn f => fn x => f (f (f (f x)))

... and then look at their types:

val c0 = fn : 'a -> 'b -> 'b
val c1 = fn : ('a -> 'b) -> 'a -> 'b
val c2 = fn : ('a -> 'a) -> 'a -> 'a
val c3 = fn : ('a -> 'a) -> 'a -> 'a
val c4 = fn : ('a -> 'a) -> 'a -> 'a 

... after the 2nd function the type ('a ->'a) -> 'a -> 'a emerges. Is this the general type you are looking for?

The type of the first two functions differs only because the type inference algorithm chooses the most general type. And for the first function 'a -> 'b -> 'b is a more general type as ('a -> 'a) -> 'a -> 'a. But you can always give the compiler a hint using a type annotation:

val c0 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => x
val c1 : ('a -> 'a) -> 'a -> 'a = fn f => fn x => f x

... and all your functions should have the same type now.

Answer 2

What you do is, you apply a process called Hindley–Milner type inference.

The general principle involves three steps:

1. First, we assign undetermined types (written 'Z, 'Y, 'X, etc.) to variables and expressions.

   • If the expression uses a variable that we've already assigned a type to, then we use that. For example, if three has already been bound with type int, then in val nine = three * three, we know that the three has type int.
   • If the expression uses a variable that we've already assigned a nontrivial type scheme to (i.e., it's polymorphic), then we use that scheme, but replace each type variable with an undetermined type. For example, if first has already been bound with type 'a * 'b -> 'a, then in val firstOfFirst = fn quartet => first (first quartet), we assign one first the type 'Z * 'Y -> 'Z and the other one the type 'X * 'W -> 'W.
   • If the expression uses a newly-bound variable (scoped by fn or rec), then all occurrences of that variable have to have exact the same type — no polymorphism is allowed at this point. For example, in fn f => (f 1, f "one") (which ends up giving a type error), we initially assign all occurrences of f the single type 'Z. (The type error results because we later need to refine that to both int -> 'Y and string -> 'Y, and these are contradictory. This is because Standard ML doesn't support first-class polymorphism.)

   In your example, val one = fn f => (fn x => f x), we can assign f the type 'Z, and x the type 'Y.

2. Next, we perform type unification, where we identify different parts of the types of different sub-expressions that have to match. For example, if we know that f has type 'Z -> real and that i has type int, then if we see f i, we can "unify" the 'Z with the int and conclude that f has type int -> real.

   • There are many, many details of type unification, but I think they're all pretty much what you would assume, so I won't go into them.

   In your example, since f is applied to x, we can unify 'Z with 'Y -> ..., and end up assigning f the type 'Y -> 'X. So the expression as a whole has type ('Y -> 'X) -> 'Y -> 'X.

3. Lastly, we perform type generalization. Once we've performed all unifications that can be performed — once we've deduced everything we can about the types — we can safely replace the undetermined types with bound type variables. In your case, that lets us assign one the type-scheme ∀ αβ . (α → β) → α → β (meaning "for any and all types α and β, one has the type (α → β) → α → β"). In Standard ML notation, we don't include the explicit "∀ αβ" part; we just write ('a -> 'b) -> 'a -> 'b.