Что такое магия системы типа Haskell, позволяет определить соединение?

Question

Функция join полезности определяется как:

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

Учитывая, что тип >>= является Monad m => m a -> (a -> m b) -> m b и id является a -> a, как это может быть функция также классифицирован как a -> m b, как это должно быть в приведенном выше определении? Что такое m и b в этом случае?

Answer 1

The a с в типах для >>= и id не обязательно один и те же a с, так что давайте переформулировать типы, как это:

(>>=) :: 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, что означает, что эти два типа эквивалентны. Как правило, если вы заменяете все экземпляры переменной типа другой переменной типа, которая не встречается в оригинале, вы получаете эквивалентный тип.
• Вы можете заменить все вхождения переменной типа конкретным типом. I.e., если у вас есть id :: a -> a, вы можете переписать это на id :: Int -> Int. Последний, однако, не может быть переписан обратно к оригиналу, поэтому в данном случае вы , специализирующийся на типа.
• В более общем смысле, чем второе правило, вы можете заменить все вхождения переменной типа любым типом, конкретным или переменным. Например, если у вас есть f :: a -> m b, вы можете заменить все вхождения a на m b и получить 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)