Функция, переданная в список привязки монады, может быть идентификатором без ошибки компилятора

При применении функции привязки монады списка к простой функции списка и идентификации:

[[1,2],[3,4]] >>= \x -> x

я получил

[1,2,3,4]

Однако определение класса типа Monad:

class Monad m where
  (>>=) :: m a -> (a -> m b) -> m b

кажется, предполагает, что функция, в моем случае лямбда-функция \x -> x, должна возвращать тип, отличный от переданного. В этом случае я ожидал бы ошибку компилятора, но у меня ее нет. Я запускаю это в ghci.

Почему в этом случае компилятор не выдает ошибку?


person Michal Charemza    schedule 29.11.2014    source источник
comment
Нет, a и m b не обязательно должны быть разными. В вашем случае у вас есть a = [Int] и b = Int и m = [].   -  person n. 1.8e9-where's-my-share m.    schedule 29.11.2014
comment
Две переменные типа могут быть разных типов. Однако они должны быть разными; им разрешено быть равными в любом конкретном вызове.   -  person MathematicalOrchid    schedule 30.11.2014


Ответы (3)


Функция тождества id :: a -> a или явно \x -> x является полиморфной. Это означает, что он может быть специализирован для любого типа, который вы создадите, заменив a каким-либо типом.

В вашем случае (>>= id) компилятор смотрит на тип второго аргумента

(>>=) :: m c -> (c -> m d) -> m d

и тип id и пытается их объединить:

a -> a    -- id
c -> m d  -- the second argument of >>=

это выполняется в самом общем виде, когда мы подставляем a = m d и c = m d. Таким образом, наиболее общий тип id внутри выражения(>>= id) — это

id :: m d -> m d

и тип всего выражения

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

которая является функцией join .

person Petr    schedule 29.11.2014

a, m и b являются переменными типа, и ничто не мешает a быть равным m b в данной ситуации. Это идея полиморфизма: если что-то имеет тип a без дополнительных ограничений на a, то оно также имеет тип Int, и [[Bool]], и c -> [Int] -> d, и (как здесь) m b.

Итак, для этого конкретного вызова a ~ [Int], b ~ Int, m ~ [] и, следовательно, (>>=) имеет тип [[Int]] -> ([Int] -> [Int]) -> [Int].

person Tarmil    schedule 29.11.2014

Внутренний список отображается в выходных данных как внешний список, но список тем не менее является списком.

Другой способ сказать это так:

foreach x in [[1,2],[3,4]]: 
    foreach y in x: 
        emit y

а также

foreach x in [1,2,3,4]: 
    emit x

«одинаковы» в отношении испускаемых элементов.

Я считаю, что презентации шрифтов с выстроенными в ряд субсущностями очень визуально привлекательны:

(>>=) :: m a -> (a -> m b) -> m b
[[1,2],[3,4]] :: [[Int]]    -- actually, (Num a) => [[a]], but never mind that
\x -> x :: a -> a

(>>=) :: m a           -> (  a   -> m b) -> m b       
(>>=)    [[1,2],[3,4]] :: (  a   -> m b) -> m b       m a ~ [[Int]]
(>>=)    [[1,2],[3,4]] :: (  a   -> [b]) -> [b]       m   ~ []
(>>=)    [[1,2],[3,4]] :: ([Int] -> [b]) -> [b]       a   ~ [Int]
(>>=)    [[1,2],[3,4]]    (\ x   ->  x ) :: [b]       [b] ~ [Int]
(>>=)    [[1,2],[3,4]]    (\ x   ->  x ) :: [Int]     b   ~ Int
                                                     -- actually, (Num b) => b

Вот, оказывается, \ x -> x :: (Num b) => [b] -> [b], а не только a -> a.

Видите ли, когда ([Int] -> [b]) сопоставляется с типом (\ x -> x), создавая эквивалентность [Int] ~ [b], [] в [Int] происходит из "внутреннего списка", a в m a; а [] в [b] происходит из "внешнего списка", m в m b; но список есть список, как было сказано выше.

И это то, что позволяет разбить («объединить») два уровня списка в один, «сгладить» список или, в более общем смысле, «объединить» два «уровня» монады в один.


Другой способ увидеть это — расширить монадический код его конкретной версией списка:

[[1,2],[3,4]] >>= \x -> x
=== concatMap id [[1,2],[3,4]]          === concat [ x | x <- [[1,2],[3,4]]]
=== concat [id [1,2], id [3,4]]         === [ y | x <- [[1,2],[3,4]], y <- x]
=== [1,2,3,4]                           === [1,2,3,4]

Все, что имеет значение для f в concatMap f, это то, что это функция, производящая список: f :: a -> [b].

И concatMap id === concat :: [[a]] -> [a] — вполне законная функция. Да, concat равно join для монады списка:

ma >>= f === join (fmap f ma)   -- or, for lists,
         === concat (map f ma)
         === concatMap f ma     -- the definition that we used above
person Will Ness    schedule 29.11.2014