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
What you do is, you apply a process called Hindley–Milner type inference.
The general principle involves three steps:
First, we assign undetermined types (written 'Z, 'Y, 'X, etc.) to variables and expressions.
three has already been bound with type int, then in val nine = three * three, we know that the three has type int.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.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.
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.
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.
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.
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.
