Как gpostpro «убегает от монады»?

Question

Я пытаюсь понять, как это очень абстрактно-рекурсивная функция из пакета Haskell recursion-schemes работает (или, на самом деле, что он делает!) - от this file:

class Functor (Base t) => Corecursive t where 

    [...] 

    -- | A generalized postpromorphism 
    gpostpro 
    :: (Recursive t, Monad m) 
    => (forall b. m (Base t b) -> Base t (m b)) -- distributive law 
    -> (forall c. Base t c -> Base t c)   -- natural transformation 
    -> (a -> Base t (m a))      -- a (Base t)-m-coalgebra 
    -> a          -- seed 
    -> t 
    gpostpro k e g = a . return where a = embed . fmap (ana (e . project) . a . join) . k . liftM g 

В частности, то, что я хочу, чтобы понять: как он применяет функцию g, которая упоминает конструктор типа монады m, но затем возвращает значение типа t, которое не упоминает или не зависит от m? Я думал, что победить из произвольных монадов невозможно в Хаскелле!

Сначала я загрузил исходный файл в Intero, чтобы попытаться использовать его функцию типа в точке, но эта попытка failed.

Затем я загрузил его в GHCi, используя cabal repl, и попытался следовать за типами через скомпонованные функции по одному, используя GHCi, чтобы помочь с типом вывода, комментируя различные биты определения. Однако, когда я добрался до fmap, я не смог понять, что закомментировать, потому что, если я раскомментировал рекурсивный вызов a, но прокомментировал другие вещи, я подумал, что он, вероятно, даже не будет компилироваться, потому что частично закомментированный определениеa не будет иметь подходящий тип.

Answer 1

Мне удалось получить ghci, чтобы рассказать мне, какие типы подвыражений были окружены ими в ( ... :: _).

Оказывается, хитрость заключается в том, то «дистрибутивный закон» k позволяет впихнуть монады внутри временного Base типа, а затем метод embed позволяет обойтись без временного Base типа и вернуться к t. Если действительно конкретный тип t не упоминает IO, тогда было бы невозможно написать такой k (безопасно) для монады IO, например. Таким образом, здесь нет никакой магии, т. Е. Не использовать эту функцию для выхода из монадов, которые в противном случае были бы незаменимыми, например, IO.