haskell - 什么 Haskell 类型系统魔法允许定义连接？

Question

join效用函数定义为：

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

鉴于>>=isMonad m => m a -> (a -> m b) -> m b和idis的类型a -> a，该函数如何也a -> m b像上面定义中的那样被键入？在这种情况下m是什么？b

Answer 1

和a类型中的s不一定是相同的 s，所以让我们重述一下类型：>>=ida

(>>=)    :: 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，您可以替换所有出现的awithm 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)