[Haskell-cafe] Help with Bird problem 1.4.1

[Daniel Fischer]

On Tuesday 18 May 2010 21:49:50, R J wrote:
> Newbie trying to get through Bird.  Could someone provide a clean
> solution, with proof (so I can see how these proofs are laid out), to
> this: Given:
> f :: Integer -> Integer
> g :: Integer -> (Integer -> Integer)
> h :: ...
> h x y =  f (g x y)
> Questions:
> a.  Fill in the type assignment for "h".

h takes two arguments[1], feeds them to g and applies f to the result.
So the type of h must be

h :: a -> b -> c (or, equivalently, h :: a -> (b -> c)).

The overall result is the result of f, hence the final result type of h 
must be the result type of f, in other words, c = Integer.
The arguments of h are passed to g, hence the types of h's arguments must 
be the types of g's arguments, in other words, a = b = Integer, so

h :: Integer -> Integer -> Integer

If you don't get irritated by the parentheses in g's type (or if you're 
used to how functions work), it's very straightforward. 

> b.  Which of the following is true:   
> (i)   h = f . g

The type of (.) is

(.) :: (b -> c) -> (a -> b) -> (a -> c)

Hence, if (f . g) is a well typed expression, f's type must be (b -> c) and 
g's type must be (a -> b).
Now, f :: Integer -> Integer, giving b = Integer and c = Integer.
Further, g :: Integer -> (Integer -> Integer), giving a = Integer and 
b = (Integer -> Integer).
We have conflicting resolutions of b, thus the expression (f . g) isn't 
well typed, in particular, (i) is false.

> (ii)  h x = f . (g x)

Firstly, if x :: Integer, then (f . (g x)) is a well typed expression. For, 
(g x) :: Integer -> Integer, so now unifying the type of (g x) with the 
(a -> b) from (.)'s type gives a = Integer and b = Integer.
Thus f and (g x) resolve b to the same type and we have

f . (g x) :: Integer -> Integer

Now, the definition of (.) is
(u . v) y = u (v y).
Substituting u = f and v = (g x), we find
(f . (g x)) y = f ((g x) y).
Since function application is left-associative, we can also write ((g x) y) 
as (g x y) and find that indeed both sides of the equation give the same 
values for each argument y, so they are the same. (ii) is true.

> (iii) h x y = f . (g x y)

Now, g x y :: Integer. Integer can't be unified with (a -> b), so (g x y) 
is not a suitable argument for (.) and
f . (g x y) is not a well typed expression, in particular, (iii) is false.




[1] Actually, every function takes exactly one argument. Some functions, 
however, return functions, which then take another argument and return 
possibly another function, which then takes another argument, ...

But, if

fun :: a -> (b -> (c -> d))

, it would be too cumbersome to say "fun is a function which takes an 'a' 
as argument and returns a function which takes a 'b' as argument and 
returns a function which takes a 'c' as argument and returns a 'd'", so 
most of the time we abbreviate that to "fun is a function taking three 
arguments, an 'a', a 'b' and a 'c' and returns a 'd'".
And, unless there are reasons not to, usually the parentheses in the 
function type are omitted, like the parentheses in the function 
application.
Properly parenthesised, the definition of h above would be

h x y = f ((g x) y).
But since function application associates to the left and the function type 
(->) associates to the right, the parentheses aren't necessary.