signatures/types in functional programming (OCaml)

Question

I started learning functional programming (OCaml), but I don't understand one important topic about fp: signatures (I'm not sure if it's a proper name). When I type something and compile with ocaml, I get for example:

# let inc x = x + 1 ;;
val inc : int -> int = <fun>

This is trivial, but I don't know, why this:

let something f g a b = f a (g a b)

gives an output:

val something : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun>

I suppose, that this topic is absolutely basics of fp for many of you, but I ask for help here, because I haven't found anything on the Internet about signatures in OCaml (there are some articles about signatures in Haskell, but not explanations).

If this topic somehow will survive, I post here several functions, which signatures made me confused:

# let nie f a b = f b a ;; (* flip *)
val nie : (’a -> ’b -> ’c) -> ’b -> ’a -> ’c = <fun>

# let i f g a b = f (g a b) b ;;
val i : (’a -> ’b -> ’c) -> (’d -> ’b -> ’a) -> ’d -> ’b -> ’c = <fun>


# let s x y z = x z (y z) ;;
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>

# let callCC f k = f (fun c d -> k c) k ;;
val callCC : ((’a -> ’b -> ’c) -> (’a -> ’c) -> ’d) -> (’a -> ’c) -> ’d = <fun>

Thank you for help and explanation.

Answer 1

There are a couple of concepts you need to understand to make sense of this type signature and I don't know which ones you already do, so I tried my best to explain every important concept:

Currying

As you know, if you have the type foo -> bar, this describes a function taking an argument of type foo and returning a result of type bar. Since -> is right associative, the type foo -> bar -> baz is the same as foo -> (bar -> baz) and thus describes a function taking an argument of type foo and returning a value of type bar -> baz, which means the return value is a function taking a value of type bar and returning a value of type baz.

Such a function can be called like my_function my_foo my_bar, which because function application is left-associative, is the same as (my_function my_foo) my_bar, i.e. it applies my_function to the argument my_foo and then applies the function that is returned as a result to the argument my_bar.

Because it can be called like this, a function of type foo -> bar -> baz is often called "a function taking two arguments" and I will do so in the rest of this answer.

Type variables

If you define a function like let f x = x, it will have the type 'a -> 'a. But 'a isn't actually a type defined anywhere in the OCaml standard library, so what is it?

Any type that starts with a ' is a so-called type variable. A type variable can stand for any possible type. So in the example above f can be called with an int or a string or a list or anything at all - it doesn't matter.

Furthermore if the same type variable appears in a type signature more than once, it will stand for the same type. So in the example above that means, that the return type of f is the same as the argument type. So if f is called with an int, it returns an int. If it is called with a string, it returns a string and so on.

So a function of type 'a -> 'b -> 'a could take two arguments of any types (which might not be the same type for the first and second argument) and returns a value of the same type as the first argument, while a function of type 'a -> 'a -> 'a would take two arguments of the same type.

One note about type inference: Unless you explicitly give a function a type signature, OCaml will always infer the most general type possible for you. So unless a function uses any operations that only work with a given type (like + for example), the inferred type will contain type variables.

Now to explain the type...

val something : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>

This type signature tells you that something is a function taking four arguments.

The type of the first argument is 'a -> 'b -> 'c. I.e. a function taking two arguments of arbitrary and possibly different types and returning a value of an arbitrary type.

The type of the second argument is 'a -> 'd -> 'b. This is again a function with two arguments. The important thing to note here is that the first argument of the function must have the same type as the first argument of the first function and the return value of the function must have the same type as the second argument of the first function.

The type of the third argument is 'a, which is also the type of the first arguments of both functions.

Lastly, the type of the fourth argument is 'd, which is the type of the second argument of the second function.

The return value will be of type 'c, i.e. the return type of the first function.

Answer 2

If you're really interested in the subject (and have access to a university library), read Wadler's excellent (if somewhat dated) "Introduction to functional programming". It explains type signatures and type inference in a very nice and readable way.

Two further hints: Note that the -> arrow is right-associative, so you can bracket things from the right which sometimes helps to understand things, ie a -> b -> c is the same as a -> (b -> c). This is connected to the second hint: Higher order functions. You can do things like

let add x y = x + y
let inc = add 1

so in FP, thinking of 'add' as a function that has to take two numerical parameters and returns a numerical value is not generally the right thing to do: It can also be a function that takes one numerical argument and returns a function with type num -> num.

Understanding this will help you understand type signatures, but you can do it without. Here, quick and easy:

# let s x y z = x z (y z) ;;
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun>

Look at the right hand side. y is given one argument, so it is of type a -> b where a is the type of z. x is given two arguments, the first one of which is z, so the type of the first argument has to be a as well. The type of (y z) , the second argument, is b, and hence the type of x is (a -> b -> c). This allows you to deduce the type of s immediately.