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.