Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Understanding the type of this Haskell function

Tags:

haskell

I'm new to Haskell and I have a question about the following code:

a x (b:bs) = a (b x) bs
a x b = x []

What is the general type of these patterns?

With :info a I get: ([t1] -> t) -> [([t1] -> t) -> [t1] -> t] -> t

However, I cannot understand why. Does a have just two "inputs" or not?

like image 800
user1299292 Avatar asked Mar 09 '23 23:03

user1299292


2 Answers

I just have two "Inputs" or not?

Yes, you have two parameters (technically one because of the way currying works).

With :info a I get: ([t1] -> t) -> [([t1] -> t) -> [t1] -> t] -> t

This means the first parameter has type [t1] -> t (so it's a function that takes a list of t1s and produces a t), the second parameter has type [([t1] -> t) -> [t1] -> t] (a list of functions that take a function of type [t1] -> t and a list of t1s and produce a t) and the result has type t.

But I cannot understand why.

Let's look at the code:

a x (b:bs) =

The first parameter is just a variable pattern, so its type is anything. The second one is a list pattern, so it must be a list.

So if we use numbered question marks to denote types we don't know yet, we so far know the following:

x :: ?1
b :: ?2
bs :: [?2]
a :: ?1 -> [?2] -> ?3

Now let's look at the body:

a (b x) bs

b is applied to x, so b must be a function that takes the type of x as its parameter. The result of b x is used as the first argument to a, so the result type of b must also match the type of x. Thus ?2 must be ?1 -> ?1 and we get:

x :: ?1
b :: ?1 -> ?1
bs :: [?1 -> ?1]
a :: ?1 -> [?1 -> ?1] -> ?3

Now let's take a look at the second body (b and bs are now no longer in scope, technically there's a new b, but it's not used, so we'll ignore it):

x []

Here x is applied to an empty list. So it must also be a function and its parameter type is some sort of list. Since the result of x [] is also the result of the a, x's result type must be ?3. So we get ?1 = [?4] -> ?3 and thus:

a :: ([?4] -> ?3) -> [([?4] -> ?3) -> ([?4] -> ?3)] -> ?3

Since -> is right-associative, we can get rid of the parentheses at the end there and get:

a :: ([?4] -> ?3) -> [([?4] -> ?3) -> [?4] -> ?3] -> ?3

And now, since that's all the type information we have, all the question marks that are left are actual type variables, so we can replace them with arbitrary type variable names. If we choose ?3 = t and ?4 = t1, we get the exact output of info (but of course we could name them anything else and the type would still be equivalent).

like image 89
sepp2k Avatar answered Mar 18 '23 23:03

sepp2k


If you only look at the first half of the definition we get a nice type:

a :: t -> [t -> t] -> t1
a x (b:bs) = a (b x) bs

We take a value and apply a bunch of functions from the list to it. We don't know yet what happens after we run out of functions because we haven't looked at the second part yet.

Lets try to imagine another ending first:

a :: t -> [t -> t] -> t
a x [] = x

When we are done we return our final value. Note that this solved our uncertain return type. Since we just do reversed function application over a list we could just fold with reversed function application over the list and get the same function:

a :: t -> [t -> t] -> t
a = foldl (flip ($))

But that isn't how our function ends in reality. It ends with

a x [] = x []

Here is what we just learned: x is a function that takes an list of somethings and returns something. What these somethings are we can't say so lets call them t1 and t2. We know x's type is t so we can just replace all occurrences of t in our first function with [t1] -> t2:

a :: ([t1] -> t2) -> [([t1] -> t2) -> ([t1] -> t2)] -> t2

And that is how that type signature happened! We also know that it is equivalent to:

a x ls = foldl (flip ($)) x ls $ []

which still is a weird function.

like image 38
Taren Avatar answered Mar 19 '23 00:03

Taren