ren
ren

Reputation: 23

how to prove the associative law of the compositon operation (.) in Haskell

say ,

    f :: a -> b 
    g :: b -> c 
    h :: c -> d

why the equation

    h.(g.f) = (h.g).f  

is right? how to prove it? and the composition operation is just a basic operation in Haskell, or we can get one by ourselves? if so how to achieve it?

Upvotes: 2

Views: 456

Answers (1)

Aadit M Shah
Aadit M Shah

Reputation: 74204

You can define the composition operator yourself as follows:

(.) :: (b -> c) -> (a -> b) -> a -> c
g . f = \x -> g (f x)

Now, to prove associativity:

lhs = h . (g . f)
    = \x -> h ((g . f) x)         -- substitution
    = \x -> h ((\y -> g (f y)) x) -- substitution
    = \x -> h (g (f x))           -- beta reduction

rhs = (h . g) . f
    = \x -> (h . g) (f x)         -- substitution
    = \x -> (\y -> h (g y)) (f x) -- substitution
    = \x -> h (g (f x))           -- beta reduction

Now, we have lhs = rhs. QED.

Upvotes: 4

Related Questions