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.