[Haskell-beginners] Haskell type system

[Daniel Fischer]

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.)