Как gpostpro "сбежать из монады"?

Question

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

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, чтобы попытаться использовать его функцию "тип в точке", но эта попытка не удалась.

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

Answer 1

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

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