質問

I have started learning Haskell from Introduction to FP using Haskell by Richard Bird, but I am stuck in proving the following:

pair (f, g) . h = pair (f . h, g . h)

The definitions of pair is the following:

pair :: (a -> b, a -> c) -> a -> (b, c)
pair (f, g) x = (f x, g x)

Could someone point me in the right direction? Please keep in mind that I am only at the beginning. Thanks in advance!

役に立ちましたか?

解決 3

Be careful, spoiler! I am going to explain the full proof below, if you want to try it by yourself follow the advice of @nponeccop and try to expand your function calls ;)

Proof

Knowing that:

f . g = \x -> f (g x)

pair :: (a -> b, a -> c) -> a -> (b, c)
pair (f, g) x = (f x, g x)

And that the infix composition operator . has a lower precedence than function application, you can work out the following:

  pair (f, g) . h
= (pair (f, g)) . h            -- explicit precedence
= \x -> (pair (f, g)) (h x)    -- expanding the composition operator
= \x -> (f (h x), g (h x))     -- expanding 'pair'
= \x -> ((f . h) x, (g . h) x) -- using the composition operator
= \x -> pair (f . h, g . h) x  -- back to 'pair'
= pair (f . h, g . h)

Q.E.D if I didn't make a boo boo... Hope this helped!

他のヒント

One way is to expand all definitions. Remember that f . g = \x -> f (g x) and f a b = ... is the same as f a = \b -> ....

So you can try to expand definitions of pair and . in pair (f, g) . h = pair (f . h, g . h)

You can use extensionality, i.e., if two functions give the same result when acting on any x, then they are considered the same (as pure functions - they may have different code and hence different time/space usage).

So in this case, you could take the equality you're trying to prove, act with each side on some x of the appropriate type, and show you obtain the same result in both cases.

ライセンス: CC-BY-SA帰属
所属していません StackOverflow
scroll top