1

Hello I am getting ready for my finals and there is always ml type inference on the exams . i.e. we are asked to write the type of a function like this one :

fun ugh x y z = x z (y z);
val ugh = fn : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c

or 

fun doh x y z = z (x y ) (y + 1);
val doh = fn : (int -> 'a) -> int -> ('a -> int -> 'b) -> 'b

However all the ways I am trying to infer the type I always get it wrong . Although there are examples online there are no examples for functions like that . Is there a way to make up the type following some guidelines ? The guidelines would be best if applied to the first example .

Akismpa
  • 61
  • 7

1 Answers1

1

Yes, there are several examples of type inference by hand on StackOverflow: 1, 2, 3, 4, 5, ...

  1. To infer the type of fun ugh x y z = x z (y z), you could start by saying that

    val ugh : 'a -> 'b -> 'c -> 'd

    since it takes three curried arguments. You can also see that x : 'a is a function of two curried parameters and that y : 'b is a function of one parameter, and that 'd should be expressed entirely in terms of 'a, 'b and 'c.

    So for the type of y, set 'b = 'c -> 'e, since it takes z : 'c as input and returns something of a type that we haven't gotten to yet.

    And for the type of x, set 'a = 'c -> 'e -> 'f, since it takes z : 'c and the output of y as input and returns something of a type that we haven't gotten to yet.

    Replacing those, adding parentheses as needed, you get

    val ugh : ('c -> 'e -> 'f) -> ('c -> 'e) -> 'c -> 'f

    At that point you might want to rename them so you get

    val ugh : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c

    but you don't really have to.

    The only things I had to think about here was the fact that the type of x depends on the type of y, so I wanted to determine that first.

  1. To infer the type of fun doh x y z = z (x y) (y + 1), you could similarly start by saying that

    val doh : 'a -> 'b -> 'c -> 'd

    since it also takes three curried arguments. Most easily you can set 'b = int, and similar to the first example, you can set 'a = int -> 'e and then 'c = 'e -> int -> 'd.

    Replacing those, adding parentheses as needed, you get

    val doh : (int -> 'e) -> int -> ('e -> int -> 'd) -> 'd

    or after a little renaming

    val doh : (int -> 'a) -> int -> ('a -> int -> 'b) -> 'b
sshine
  • 15,635
  • 1
  • 41
  • 66
  • The way you set 'c = int and 'b int -> 'e the type should be : val doh : ('e -> int -> 'd) -> (int -> 'e) -> int -> 'd . What troubles me more is the correct order of those types . Starting from left to right do we put the arguments in order that they appear on the left of the function , meaning that x->y->z->doh ? – Akismpa Sep 05 '17 at 10:20
  • Plus the compiler gives this type for doh : (int -> 'a) -> int -> ('a -> int -> 'b) -> 'b – Akismpa Sep 05 '17 at 10:33
  • 1
    You swapped the positions of the `'a` and `'c` substitutions in that last result. – molbdnilo Sep 05 '17 at 11:18
  • @Akismpa: You could try with the order they appear on the screen. In the first example, though, the function `x` takes the output of function `y` as input, and since I haven't expressed the type of `y` as a function from one type to another yet, I can't readily expand the type of `x` in terms of that. So I put `x` on hold and started inferring `y` instead. You might end up with mutual dependencies or large enough examples that following a type inference algorithm strictly will be a benefit. But as long as you can keep track of the variables in your head, there doesn't seem to be a need to me. – sshine Sep 06 '17 at 11:41