1

我正在尝试手动导出类型fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

F 。是的

y :: t1 -- First occurrence
f :: t2 -- First occurrence

(.) (b1 -> c1) -> (a1 -> b1) -> a1 -> c1 -- (.) definition

t1 ~ a1 -> b1 -- y unified with (a1 -> b1)
t2 ~ b1 -> c1 -- y unified with (b1 -> c1)

y :: a1 -> b1
f :: b1 -> c1
---
f . y :: a1 -> c1 -- Cancellation rule

\f -> 让操作 xy = x 。F 。是的

(.) (b2 -> c2) -> (a2 -> b2) -> a2 -> c2 -- (.) definition

x :: t3 -- First occurrence

t3 ~ b2 -> c2 -- x unified with (b2 -> c2)
a1 -> c1 ~ a2 -> b2 -- f . y unified with (a2 -> b2)

a1 ~ a2
c1 ~ b2

y :: a2 -> b1 -- Substituing a1 by a2
f :: b1 -> b2 -- Substituing c1 by b2
x :: b2 -> c2 -- Substituing t3 by b2 -> c2
---
x . f . y :: a2 -> c2 -- Cancellation rule
(\f -> let ope x y :: x . f . y) 
          :: (b2 -> c2) -> (a2 -> b1) -> (b1 -> b2) -> a2 -> c2 -- Adding f

foldr1 操作 xss

foldr1 :: (a -> a -> a) -> [a] -> a -- foldr1 definition

xss ~ t4 -- First occurrence

那么a ~ (b2 -> c2), a ~ (a2 -> b1), a ~ (b1 -> b2) and t4 ~ [a]这似乎是一个错误。

有什么帮助吗？

谢谢，
塞巴斯蒂安。

4

2 回答 2

1

从函数开始

fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

我将其重写为

fun xss f = foldr1 ope xss
    where ope x y = x . f . y

所以我们开始foldr1：

foldr1 :: (a -> a -> a) -> [a] -> a

所以我们可以分解

foldrl1
    ope    -- (a -> a -> a)
    xss    -- [a]

因此ope :: a -> a -> a，了解这一点非常有用，因为它简化了 和 的类型，x完全y限制为a，或者换一种方式，它们都具有相同的类型。由于它们都是函数（如 所要求的那样.），而不是长时间统一它们的类型，我只想说x, y :: b -> c

ope x y =    x     .    f     .    y
--        (b -> c) . (s -> t) . (b -> c)

f除了指定它必须是一个函数之外，我现在将 's 的类型保留为未知数。既然我们知道x并且y具有相同的类型，我们现在可以说y的输出类型与f的输入类型相同，所以s ~ c，并且f的输出类型必须与x的输入类型相同，所以t ~ b，所以我们得到

ope x y =    x     .    f     .    y
--        (b -> c) . (c -> b) . (b -> c)

所以现在我们可以填写fun的签名。我们已经知道 的类型xss，它是a ~ b -> c，并且由于foldr1的​​输出类型也是a，我们得到

 fun :: [b -> c] -> (c -> b) -> (b -> c)

确实，这是GHCi给我们的类型

于 2014-05-09T16:55:51.480 回答
1

这是推导。

fun xss = \f -> let ope x y = x . f . y in foldr1 ope xss

fun xss f = foldr1 ope xss
   where
      ope x y = x . f . y                                      y :: a -> b
              =     y   >>>   f   >>>   x                      f :: b -> c
                  a -> b    b -> c    c -> d                   x :: c -> d
              ::  a  ------------------->  d

ope          x         y    ::  a->d
ope    ::  (c->d) -> (a->b) -> (a->d)

foldr1 :: (  a1   ->   a1   ->   a1  ) -> [ a1 ] ->   a1       c ~ a, d ~ b
          ((a->b) -> (a->b) -> (a->b)) -> [a->b] -> (a->b)     a1 ~ a->b
foldr1                ope                  xss   :: (a->b)

fun      xss       f    ::  a->b
fun :: [a->b] -> (b->a) -> (a->b)

函数组合是关联的：f . (g . h)=~= (f . g) . h。这就是为什么表达f . g . h形式良好。

就像(.) :: (b->c) -> (a->b) -> (a->c)创建一个由两个函数组成的链一样，该f . g . h表达式创建一个由三个函数组成的链，每个函数都将其前任的输出作为输入。

有时使用(.)的表亲更容易>>>，它只是颠倒了参数的顺序：

f . g === g >>> f

它定义在Control.Category.

于 2014-05-09T17:06:53.000 回答