CODEWITHSUNDEEP
functional-programmingsml
vesii
vesii

Reputation: 3128

Finding the right type of a function in Standard ML

Usually test which contain question about SML have questions that ask you to find the signature/type of a function.

For example - What is the type of the following function:

fun foo f g x y = f (f x (g x) y) y;

Solution:

val foo = fn : ('a -> 'b -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'b -> 'b -> 'a

I was wondering if there is a good algorithm I could follow in order to solve those kind of questions. Every time I try to solve one of those, I get confused and fail.

Upvotes: 1

Views: 99

Answers (2)

sshine
sshine

Reputation: 16105

There are several ways to derive the type of a function depending on how close to the compiler's algorithm you want to go and how much you want to cut corners with intuition, which can come handy in practice and perhaps in exams, depending on the focus of the exam.

  • An example by Ionuț G. Stan cuts very few corners, and has a quite verbose notation. This mechanical approach is very safe, spells out everything and takes some time.

  • This current example by molbdnilo takes a middle ground and does some equational reasoning, but also relies on some level of intuition. I think this is generally the way you want to be able to do it, since it takes less time and space by hand.

  • An example by me links to various other examples for a diversity in practical approaches.

Upvotes: 0

molbdnilo
molbdnilo

Reputation: 66371

Start with what you know, then figure out a bit here and a bit there until there are no unknowns.

Here is one possibility:

Call the unknown types FOO, F, G, X, and Y, respectively.

Then look for something small and easy and start assigning types.

(g x)

is clearly an application of a function to one argument.
Set X = a and G = a -> b.

Then look at the enclosing expression:

(f x (g x) y)
   |   |
   v   v
   a   b

So far, we know that F = a -> b -> Y -> C, for some C.

Go outwards again:

f (f x (g x) y) y

Since both x and (f x (g x) y) are first arguments to f, they must be the same type a, and the same idea applies to y and (g x), giving them the type b.

So, F = a -> b -> b -> a and, since the outer f is only given two arguments, the type of the right-hand side must be b -> a.

Thus

X = a
Y = b
G = a -> b
F = a -> b -> b -> a
FOO = (a -> b -> b -> a) -> (a -> b) -> a -> b -> (b -> a)

And, since arrows associate to the right, FOO is equivalent to

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

Upvotes: 2

Related Questions