В чем разница между Fix, Mu и Nu в пакете схемы рекурсии Эда Кметта

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

Неподвижная точка f является типом T изоморфизмом между T и f T, то есть парой обратных функций in :: f T -> T, out :: T -> f T. Тип Fix просто использует встроенную в Haskell рекурсию типов для прямого объявления изоморфизма. Но вы можете реализовать вход/выход как для 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 сложно; это как плыть против течения.

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