什么Haskell类型系统魔术允许连接的定义？

Question

所述join效用函数被定义为:

join :: (Monad m) => m (m a) -> m a
join x = x >>= id

鉴于>>=is Monad m => m a -> (a -> m b) -> m b和idis 的类型,a -> a该函数如何也a -> m b可以在上面的定义中输入？什么是m与b在这种情况下？

Answer 1

a类型中的s >>=和id不一定是相同的as,所以让我们重述这样的类型:

(>>=)    :: Monad m => m a     -> (a -> m b) -> m b
id       ::                        c -> c

因此,我们可以得出这样的结论c 是一样a毕竟,至少当id是第二个参数来>>=......而且这c是一样的m b.所以a是一样的m b.换一种说法:

(>>= id) :: Monad m => m (m b) ->               m b

Answer 2

dave4420点击它,但我认为以下言论可能仍然有用.

有一些规则可用于将类型有效地"重写"为与原始类型兼容的另一种类型.这些规则涉及用其他类型替换所有出现的类型变量:

• 如果你有id :: a -> a,你可以替换a使用c,并得到id :: c -> c.后一种类型也可以重写为原始id :: a -> a类型,这意味着这两种类型是等价的.作为一般规则,如果将类型变量的所有实例替换为原始中不存在的另一个类型变量,则会得到等效类型.
• 您可以使用具体类型替换所有出现的类型变量.即,如果你有id :: a -> a,你可以改写它id :: Int -> Int.然而,后者不能重写回原版,所以在这种情况下,你是专门的类型.
• 比第二个规则更常见的是,您可以替换任何类型,具体或变量的所有类型变量.例如,如果有f :: a -> m b,则可以替换所有出现的awith m b和get f :: m b -> m b.由于这个也无法撤消,它也是一个专业化.

最后一个例子展示了如何id用作第二个参数>>=.所以你的问题的答案是我们可以重写和派生类型如下:

1. (>>=)    :: m a -> (a -> m b) -> m b        (premise)
2. id       :: a -> a                          (premise)
3. (>>=)    :: m (m b) -> (m b -> m b) -> m b  (replace a with m b in #1)
4. id       :: m b -> m b                      (replace a with m b in #2)
   .
   .
   .
n. (>>= id) :: m (m b) -> m b                  (indirectly from #3 and #4)