Sml type confusion

Question

I have this function:

fun x (u,v,w) = (u::[v])::w;

Which gets a return type of

fn: 'a * 'a * 'a list list -> 'a list list

Could anyone explain to me how this type is generated from the function? Thank you!

Edit: Also, how would I call this function?

Answer 1

:: takes two arguments -- one on the left and one on the right. If its left argument is of type t, then its right argument must be of type t list.

Thus, :: has type ('a * 'a list) -> 'a list, as the t is arbitrary, and is therefore represented by an 'a.

When you have the code (u::[v]), therefore, you are telling SML that u : t and 'v : t for some type t. This expression is then a t list, and so to use it as the left argument to ::, the right argument, w, must have type t list list.

This then gives that the type of (u::[v])::w is t list list for some t.

In summary:
u : t
v : t
w : t list
(u::[v])::w : t list list,

all for some type t.

Thus, the type of x is ('a * 'a * 'a list) -> 'a list list, as t is arbitrary.

To call this function, you could do something like x(1,2,[3,4]), which would give the list [[1,2],[3,4]].