Почему Haskell предполагает, что возвращаемый тип монады - это тот же тип, который передается в качестве аргумента?

Question

Почему этот код компилируется?

--sequence_mine :: Monad m => [m a] -> m [a]
sequence_mine [] = return []
sequence_mine (elt:l) = do
  e <- elt
  sl <- sequence l
  return (e:sl)

Примечание. Я намеренно закомментировал здесь объявление типа.Но код все еще компилируется и, кажется, работает, как и ожидалось, даже без объявления типа - и это меня удивляет.

Насколько я понимаю, в этой строке должна возникнуть неоднозначность:

return (e:sl)

Причина в том, что Хаскелл не должен знать, какой тип монады мы возвращаем.Почему это должен быть тот тип, который мы принимаем?

Чтобы уточнить больше.Насколько я понимаю, если я не ставлю явным образом объявление типа, аналогичное тому, которое я закомментировал, Хаскелл должен сделать вывод, что эта функция имеет типизацию:

sequence_mine :: (Monad m1, Monad m2) => [m1 a] -> m2 [a]

Если только я явно не объединю m1 иm2 называя их обоих m, у Хаскелла нет причин полагать, что они оба относятся к одному и тому же типу!Я бы предположил.

Но это не так.Что мне здесь не хватает?

Answer 1

Хорошо, давайте посмотрим, к чему ведет блок do:

sequence_mine (elt:l) = elt >>= \e -> (sequence l) >>= \sl -> return (e:sl)

Напомним, что оператор "bind" >>= имеет сигнатуру типа (Monad m) => m a -> (a -> m b) -> m b. Обратите внимание, что монада m здесь, хотя и произвольна, должна быть одинаковой как для аргументов, так и для типа результата.

Таким образом, если elt имеет тип m a, легко увидеть, что return (e:sl) - тип вывода всего выражения - должен иметь тип m [a] для той же монады m.

Другими словами, каждый блок do работает только в контексте фиксированной монады.