Am Sonntag 27 September 2009 12:22:50 schrieb informationen:
Hi,
i am trying to understand the Haskell type system. I thought i understood it quite well until i encountered the three following exercises. As you can see, i have the answers already. But i don't understand, why they are correct.
Could anybody tell me a good place where i could learn how to answers these kind of questions correctly or could give me some explanations, why these answers are correct?
Any help is highly appreciated.
Kind regards
Chris
Two functions f and g with the following signatures are given: f :: a -> a g :: b -> c -> b
If you have a function of type fun :: x -> y then for all values v of type x, fun x has type y.
A) Give the type of the following expressions:
1) g [False] True ::
g :: b -> c -> b [False] :: [Bool] ~> (we must unify b and [Bool]) g [False] :: c -> [Bool] True :: Bool -- but that doesn't matter, could be any type ~> g [False] True :: [Bool]
2) g [] True ::
g :: b -> c -> b [] :: [a] ~> (unify b and [a]) g [] :: c -> [a] ~> g [] True :: [a]
3) g (f True) ::
g :: b -> c -> b f :: a -> a True :: Bool ~> (unify a and Bool) f True :: Bool ~> (unify b and the type of (f True)) g (f True) :: c -> Bool
4) g f ::
g :: b -> c -> b f :: a -> a ~> (unify b and (a -> a)) g f :: c -> (a -> a)
Answers:
1 [Boolean] 2) [a] 3) c -> Bool 4) c -> (a -> a)
B) Which of the following statements is correct?
1) g f 1 is type correct
By the above, g f :: c -> (a -> a) , hence (unify c and the type of 1 (forall n. Num n => n)) to get g f 1 :: (a -> a) which is valid, so (g f 1) is type correct
2) g (f 1) is type correct
f 1 has the same type as 1, (forall n. Num n => n), that must be unified with b, since the latter is a type variable, there's no problem, giving g (f 1) :: forall n. Num n => c -> n
3) g . (f 1) is type correct
For (g . (f 1)) to be type correct, (f 1) must be a function (i.e. have type (x -> y) for some x, y). As said above, (f 1) has type (forall n. Num n => n). We must now (try to) unify that with (x -> y). n is a type variable, so the art of unifying disregarding contexts is fine, replace n by (x -> y). No go for the context, the appropriate substitutions there lead to the context forall x, y. Num (x -> y) => (x -> y) If you have such a Num instance around, then g . (f 1) is well typed. But usually you haven't (and you shouldn't), so then it's not well typed because you can't unify (forall n. Num n => n) with (x -> y).
4) g . f 1 is type correct
Due to the precedences of function application and composition (.), this is exactly the same as 3).
5) (g . f) 1 is type correct
(.) :: (y -> z) -> (x -> y) -> (x -> z) g :: b -> (c -> b) f :: a -> a Thus in (g . f) we have b -> (c -> b) === (y -> z), hence y === b, z === c -> b and a -> a === (x -> y), hence x === a, y === a By y === b and y === a, we find a === b, so g . f :: x -> z === a -> (c -> a) === a -> c -> a a can be trivially unified with the type of 1 (forall n. Num n => n), so (g . f) 1 :: forall n. Num n => c -> n is type correct.
6) none of the expressions is correct
Answers: 1,2 and 5 are correct.
C) A function h is given as: h p x = p (f x). Which of the following statements is correct.
h p x = p (f x) h takes two arguments, so h :: t1 -> t2 -> t3 with as yet unknown types t1, t2, t3. From the right hand side, we see that p takes one argument and it returns a value of the same type as h, so p :: t4 -> t3 On the other hand, p is the first argument of h, so p :: t1, hence t1 === t4 -> t3 p's argument is (f x), where x is the second argument of h, so x :: t2 f :: a -> a, unifying a with t2 is just renaming, so (f x) :: t2 On the other hand, (f x) is the argument of p, so (f x) :: t4, hence t4 === t2 Together, h :: (t2 -> t3) -> t2 -> t3 rename to h :: (a -> b) -> a -> b
1) h :: a -> b -> a -> b
If h had that type, we'd have a === (t2 -> t3) b === t2 a -> b === t3, so (t2 -> t3) -> t2 === t3 [( a ) -> b a -> b] which leads to an infinite type t3 === (t2 -> t3) -> t2 === (t2 -> ((t2 -> t3) -> t2)) -> t2 === (t2 -> ((t2 -> ((t2 -> t3) -> t2)) -> t2)) -> t2 === (t2 -> ((t2 -> ((t2 -> ((t2 -> t3) -> t2)) -> t2)) -> t2)) -> t2 which is not allowed.
2) h :: (a -> a) -> a -> a
h has a more general type, so h can have this type, too (any function expecting an argument of that type will accept h)
3) h :: (a -> b) -> a -> b
Yup.
4) h is equivalent to h' with h' p = p . f
h p x = p (f x) (h' p) x = (p . f) x = p (f x) Aye.
5) h is equivalent to h' with h' p = p f
Nay. With h' p = p f, we find h' :: s1 -> s2 p :: s1 and from the right hand side, p :: (a -> a) -> b so s2 === b and s1 === ((a -> a) -> b), giving h' :: ((a -> a) -> b) -> b which is not the type of h.
5) h is equivalent to h' with h' p x = p f x
Answers: (I am not sure, if i remember correctly, but 3) and 4) should be correct.)