ML Types for function, a litle tips?

Question

I prepare for GATE Exam. one of the oldest question is unfamiliar with us. some experts please clarify this for us.

Which of the following can be a type for following ML function ?

my f(g, nil)=nil | f(g,x::xs)=(fn a  ⇒ g(a,x))::f(g, xs);

1) (int *book → real) * bool list → (int → real) list
2) (bool *int → int) * real list → (bool → int) list
3) (int *int → real) * real list → (real → bool) list
4) (bool *real → int) * int list → (int → int) list

The Answer Sheets say (1) Is corrects. comments or short description for better understanding?

Answer 1

One of the first things you should do is rewrite the function definition yourself. This will force you to actually parse and understand it.

fun f (g, nil)     = nil
  | f (g, x :: xs) = (fn a => g (a, x)) :: f (g, xs);

So, f is a function, even the question says that, it must have type ... -> ...:

val f : ... -> ...

What does it receive? Let's take a look at the first pattern of the function:

fun f (g, nil)     = nil

It's something of the form (a, b), which is a 2-tuple. The function's argument must be a tuple then:

val f : (... * ...) -> ...

Just by looking at the definition, we can't figure out what type g must have, but it uses nil for the second element of the tuple and nil is the empty list. That means the second component of the tuple must be a list of something:

val f : (... * ... list) -> ...

What else can we deduce? The return value is nil as well, which means that the function returns a list of something, unclear what that something is yet.

val f : (... * ... list) -> ... list

Ok, let's jump to the second pattern of the function definition now:

| f (g, x :: xs) = (fn a => g (a, x)) :: f (g, xs);

We don't find anything more about the type of the argument, we just got confirmation that the second element of the tuple must indeed be a list, because it uses the :: constructor.

Let's take a look at the body:

(fn a => g (a, x)) :: f (g, xs)

It looks like it's building a list, so it must return a list, which is in accordance with the return type we've sketched so far, i.e., ... list. Let's try to figure out the type of elements.

It seems to add a function object as the head of the list built by recursively calling the function f, which we're currently investigating. So the elements of the list we're returning must be functions:

val f : (... * ... list) -> (... -> ...) list

What does that function do, though? It calls g with a 2-tuple argument. Now we can fill in some information about the first element of the 2-tuple f receives. It must be a function that receives a 2-tuple as well:

val f : (((... * ...) -> ...) * ... list) -> (... -> ...) list

Can we say anything about the a parameter received by the function literal added to the return list? Not really, just that it's passed to g. Can we tell anything about the type of x? Not really, just that it's passed to g. Moreover, is there any constraint between a and x? Doesn't look like it. So far, we can only tell that g's type must be looking something like this:

('a * 'b) -> 'c'

Where 'a, 'b and 'c are polymorphic types, i.e., any concrete type can satisfy them. You can view them as wholes. We can now fill in more of the type for the f function:

val f : ((('a * 'b) -> 'c) * ... list) -> (... -> ...) list

We can do more actually, we've already assign a type to the x variable, but that comes from the second argument of the 2-tuple received by f, so let's fill in that too:

val f : ((('a * 'b) -> 'c) * 'b list) -> (... -> ...) list

And we can even fill in the element type of the returned list, because we've already assigned types for that, too.

val f : ((('a * 'b) -> 'c) * 'b list) -> ('a -> 'c) list

We can remove some extra parenthesis from the type we came up with without changing the meaning, because of the type operator precedence rules:

val f : ('a * 'b -> 'c) * 'b list -> ('a -> 'c) list

Now, our function's type is complete. However, this type can't be found in the list of possible answers, so we'll have to see if any of them can be used instead of what we've determined. Why? Because our function type uses type variables, which can be filled in by concrete types. Let's take them one by one:

Choice 1

val f : ('a  * 'b   -> 'c)   * 'b list   -> ('a  -> 'c) list
val f : (int * bool -> real) * bool list -> (int -> real) list

It looks like 'a could be int, 'b could be a bool (it's book in what you've pasted, but I'm assuming it was a typo) and 'c could be a real. All the replacements match these correspondences, so we declare that, yes, the first choice can be a possible type for the given function, even though not the most general. Let's take the second choice:

Choice 2

val f : ('a   * 'b  -> 'c)  * 'b list   -> ('a   -> 'c) list
val f : (bool * int -> int) * real list -> (bool -> int) list

The type-variable to concrete -type correspondence table could be this:

• 'a -> bool
• 'b -> int
• 'c -> int
• 'b -> real

We can stop here because we can see that 'b was assigned to different types, so this function signature can't be assigned to the implementation we've been given.

Choice 3 and 4

They are similar to choice 2, but I'll let them as an exercise to the reader :)