具有映射函数的Haskell函数组合

flo*_*poe 4 haskell equality proof function-composition map-function

我经历了理查德·伯德的"哈斯克尔功能的思考"一书,并且存在在那里他证明了滤波方法的属性我无法理解的部分.他证明的是:

filter p . map f = map f . filter (p . f)
Run Code Online (Sandbox Code Playgroud)

在本书的前面,他将过滤器定义为:

filter p = concat . map (test p)
test p x = if p x then [x] else []
Run Code Online (Sandbox Code Playgroud)

这就是他证明第一个等式的方法:

    filter p . map f
= {second definition of filter} -- He's referring to the definition I gave above
    concat . map (test p) . map f
= {functor property of map}
    concat . map (test p . f)
= {since test p . f = map f . test (p . f)}
    concat . map (map f . test (p . f))
= {functor property of map}
    concat . map (map f) . map (test (p . f))
= {naturality of concat}
    map f . concat . map (test (p . f))
= {second definition of filter}
    map f . filter (p . f)
Run Code Online (Sandbox Code Playgroud)

我无法理解的是如何test p . f等于map f . test (p . f).

这是我试图测试它的方式:

test :: (a -> Bool) -> a -> [a]
test p x = if p x then [x] else []

test ((<15) . (3*)) 4 -- test p .f, returns [4]
(map (3*) . test((<15) . (3*))) 4 -- map f . test (p . f), returns [12]
Run Code Online (Sandbox Code Playgroud)

任何人都可以解释我在这里缺少的东西吗?

HTN*_*TNW 6

你测试过了

test (p . f) = map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)

这确实是假的.该物业实际上是

test p . f = map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)

LHS关联的地方

test p . f = (test p) . f
Run Code Online (Sandbox Code Playgroud)

请记住,函数应用程序比任何用户可定义的运算符都更紧密地绑定,就像它一样infixl 10.彼此相邻的两个标识符始终是前缀函数应用程序的一部分.(在as-patterns的情况下除外:f xs@ys zs表示f (xs@ys) zs.)

证明财产:

    test p . f
={definition of (.)}
    \x -> test p (f x)
={definition of test}
    \x -> if p (f x) then [f x] else []
={definition of map, multiple times}
    \x -> if p (f x) then map f [x] else map f []
={float map f out of cases}
    \x -> map f (if p (f x) then [x] else [])
={definition of (.)}
    \x -> map f (if (p . f) x then [x] else [])
={definition of test}
    \x -> map f (test (p . f) x)
={definition of (.)}
    map f . test (p . f)
Run Code Online (Sandbox Code Playgroud)

调整你的例子test (<15) . (*3)意味着"乘以3,确保结果小于15".map (*3) . test ((<15) . (*3))表示"确保输入的三次小于15,如果是,则返回三次输入."