Type in functional programming (OCaml)

Question

I am learning functional programming and I am not understanding the types in OCaml, and I have not found anything real helpful.

I have this code:

let rec map2 f l1 l2 =
          match (l1,l2) with
          ([], _) -> []
        | (_, []) -> []
        | (x::l1s,y::l2s) -> (f x y) :: map2 f l1s l2s;;


let pick n m =
      if n > m then (fun b x -> if b then x+1 else x*2)
      else (fun b x -> if b then x+2 else x*4);;

map2 (pick 7 9) [true;false] [3;4;5;6];;

What I find difficult to understand the steps to know the type of this kind of functions (map2, pick).

I know a little bit how signature works, the right associative property and that the symbol " ' " refers to a generic type.

solution:

pick: 'a -> 'a -> bool -> int -> int = <fun>
map2: ('a->'b->'c) -> 'a list -> 'b list -> 'c list

I don't understand why bool -> int and why in map bool isn't in the function parameter.

Any reference to books, link, is welcomed

Answer 1

If you look at pick then you see that it takes 2 argument and then returns a function. What it returns is (same for the other fun):

(fun b x -> if b then x+1 else x*2)

The "if" construct is of the form if <bool> then <'a> else <'a>. So b must be bool while x can still be 'a. Going deeper there is x+1. So x must be int and the result is int too.

So the above function is bool -> int -> int and hat is shown in the type of pick.

As for map2: The map2 function can work with any function of the form 'a -> 'b -> 'c as first argument. In your example you pass bool -> int -> int but this does not limit map2 to that type. Your code could continue with

let pick_f n m =
      if n > m then (fun b x -> if b then x +. 1. else x *. 2.)
      else (fun b x -> if b then x +. 2. else x *. 4.);;

map2 (pick_f 7 9) [true;false] [3.;4.;5.;6.];;

pick_f: 'a -> 'a -> bool -> float -> float = <fun>

The same map2 function is used but here with bool -> float -> float as type of the first argument. The map2 function is polymorphic (what you called generic) and can work with many types.

Answer 2

pick: 'a -> 'a -> bool -> int -> int = <fun>
map2: ('a->'b->'c) -> 'a list -> 'b list -> 'c list

What you see here is a process in functional programming called currying. To make sense of this, let's consider a simpler example. Let's say you have a function f that takes 2 arguments X and Y, and output Z. How we usually write this is

f(X, Y) = Z

Let's see this in a different way - we have a function f, and if we give it X, and then Y, it will gives us Z. What would happen if we only give f 1 argument, X? Let's test it out!

let plus a b = a + b;;

This code defines a function plus, which takes 2 arguments a and b and returns their sum. If you type plus 1 1;; into utop, it will give you 2. Now, the output when you type

plus 1;;

is

- : int -> int = <fun>

This means plus(1) actually produces a FUNCTION that takes an int and output an int! Wait a minute, initially we have a function that produces integer, and suddenly the same function is producing ... FUNCTION? What's going on?

The key idea here is to think of a function as a process that consumes the arguments one by one. In the spirit of this, the function plus above is like a process that consumes 2 arguments: if you give it just 1 argument, it would stall and wait for the 2nd argument. And this stalled process is exactly similar to a process that consumes 1 argument: give it the remaining ingredient and it would start grinding to give you the expected output.

To see how this perspective can help you make sense of the obscure way in which function signature is written in your example, let's look at the function pick:

let pick n m =
  if n > m then (fun b x -> if b then x+1 else x*2)
  else (fun b x -> if b then x+2 else x*4);;

pick takes in 2 arguments, n and m, and output a function f that takes in 2 arguments b and x. The definition of f depends on a comparison. If n > m, then it outputs a function fun b x whose definition is if b then x+1 else x*2. Else, it outputs a function fun b x whose definition is if b then x+2 else x*4.

If we were to write a rough signature for pick based on the above understanding, it would be something like:

pick: (n, m) -> (function f that takes in b and x, and output some number)

In light of our understanding of currying, pick is like a process that consumes n, and then m. So the signature can be written in this way too:

pick: n -> m -> (function f that takes in b and x, and output some number)

Oh hey, this function f can also be thought of as a process that consumes b and then x, so we can also write:

pick: n -> m -> (b -> x -> some number)

which looks strikingly similar to:

pick: 'a -> 'a -> bool -> int -> int = <fun>

Now, as of how the heck does OCaml know that b is supposed to be bool, and x and some number is supposed to be int, OCaml has a featured called type inference. Basically speaking, the compiler looks at the operations you perform on the variables and try to make a guess of their types. E.g. I see if b in the code, so probably b should be a bool.

In summary, that obscure way in which the function signature is written is called currying, and how OCaml knows b is a bool is through a feature called type inference in OCaml. This should makes it easier for searching.