В чем разница между Fix, Mu и Nu в пакете рекурсии Ed Kmett

В пакете Ed Kmett recursion-scheme есть три объявления:

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

data Nu f where 
  Nu :: (a -> f a) -> a -> Nu f

В чем разница между этими тремя типами данных?

Ответ 1

Mu представляет собой рекурсивный тип как его сгиб, а Nu представляет его как его разворачивание. В Haskell они изоморфны и представляют собой разные способы представления одного и того же типа. Если вы делаете вид, что у Haskell нет произвольной рекурсии, различие между этими типами становится более интересным: Mu f является наименьшей (начальной) фиксированной точкой f, а Nu f является ее наибольшей (конечной) фиксированной точкой.

Фиксированная точка f является типом T изоморфизмом между T и f T, т.е. парой обратных функций in :: f T -> T, out :: T -> f T. Тип Fix просто использует встроенную рекурсию Haskell, чтобы объявить изоморфизм напрямую. Но вы можете реализовать in/out для Mu и Nu.

Для конкретного примера притворитесь, что вы не можете записать рекурсивные значения. Жители Mu Maybe, т.е. Значения :: forall r. (Maybe r -> r) -> r, являются естественными, {0, 1, 2,...}; обитатели Nu Maybe, т.е. значения :: exists x. (x, x -> Maybe x), являются контурами {0, 1, 2,..., ∞}. Подумайте о возможных значениях этих типов, чтобы узнать, почему Nu Maybe имеет дополнительный житель.

Если вы хотите получить некоторую интуицию для этих типов, это может быть забавным упражнением для реализации следующего без рекурсии (примерно в возрастающем порядке сложности):

zeroMu :: Mu Maybe, succMu :: Mu Maybe -> Mu Maybe
zeroNu :: Nu Maybe, succNu :: Nu Maybe -> Nu Maybe, inftyNu :: Nu Maybe
muTofix :: Mu f -> Fix f, fixToNu :: Fix f -> Nu f
inMu :: f (Mu f) -> Mu f, outMu :: Mu f -> f (Mu f)
inNu :: f (Nu f) -> Nu f, outNu :: Nu f -> f (Nu f)

Вы также можете попытаться реализовать их, но они требуют рекурсии:

nuToFix :: Nu f -> Fix f, fixToMu :: Fix f -> Mu f

Mu f является наименьшей фиксированной точкой, а Nu f является наибольшей, поэтому запись функции :: Mu f -> Nu f очень проста, но написать функцию :: Nu f -> Mu f сложно; это как плавание против тока.

(В какой-то момент я хотел написать более подробное объяснение этих типов, но это может быть слишком долго для этого формата.)