我已经从 Richard Bird 的使用 Haskell 的 Introduction to FP 开始学习 Haskell,但我坚持证明以下几点:
pair (f, g) . h = pair (f . h, g . h)
对的定义如下:
pair :: (a -> b, a -> c) -> a -> (b, c)
pair (f, g) x = (f x, g x)
有人能指出我正确的方向吗?请记住,我只是在开始。提前致谢!
我已经从 Richard Bird 的使用 Haskell 的 Introduction to FP 开始学习 Haskell,但我坚持证明以下几点:
pair (f, g) . h = pair (f . h, g . h)
对的定义如下:
pair :: (a -> b, a -> c) -> a -> (b, c)
pair (f, g) x = (f x, g x)
有人能指出我正确的方向吗?请记住,我只是在开始。提前致谢!
一种方法是扩展所有定义。记住f . g = \x -> f (g x)
和f a b = ...
是一样的f a = \b -> ...
。
所以你可以尝试扩展pair
和.
的定义pair (f, g) . h = pair (f . h, g . h)
您可以使用extensionality,即,如果两个函数在作用于任何x时给出相同的结果,那么它们被认为是相同的(作为纯函数 - 它们可能具有不同的代码,因此可能具有不同的时间/空间使用)。
因此,在这种情况下,您可以采用您要证明的等式,在适当类型的某个x上对每一边采取行动,并表明您在两种情况下都获得了相同的结果。
小心,剧透!我将在下面解释完整的证明,如果您想自己尝试,请遵循@nponeccop 的建议并尝试扩展您的函数调用;)
知道:
f . g = \x -> f (g x)
pair :: (a -> b, a -> c) -> a -> (b, c)
pair (f, g) x = (f x, g x)
并且中缀组合运算符.
的优先级低于函数应用程序,您可以计算出以下内容:
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)
QED 如果我没有发出嘘声......希望这会有所帮助!