haskell - ¿Cuál es la diferencia entre Fix, Mu y Nu en el paquete de esquema de recursión de Ed Kmett?

fixed-point recursion-schemes

Question

En el paquete de recursion-scheme de recursion-scheme Ed Kmett, hay tres declaraciones:

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

¿Cuál es la diferencia entre esos tres tipos de datos?

Answer 1

Mu representa un tipo recursivo como su pliegue, y Nu representa como su despliegue. En Haskell, estos son isomorfos, y son formas diferentes de representar el mismo tipo. Si pretende que Haskell no tiene una recursión arbitraria, la distinción entre estos tipos se vuelve más interesante: Mu f es el punto fijo (inicial) mínimo de f , y Nu f es su punto fijo (terminal) más grande.

Un punto fijo de f es un tipo T un isomorfismo entre T y f T , es decir, un par de funciones inversas in :: f T -> T , out :: T -> f T El tipo Fix solo usa la recursión de tipos incorporada de Haskell para declarar el isomorfismo directamente. Pero puede implementar in / out tanto para Mu como para Nu .

Para un ejemplo concreto, simule por un momento que no puede escribir valores recursivos. Los habitantes de Mu Maybe , es decir, valores :: forall r. (Maybe r -> r) -> r :: forall r. (Maybe r -> r) -> r , son los naturales, {0, 1, 2, ...}; Los habitantes de Nu Maybe , es decir, valores :: exists x. (x, x -> Maybe x) :: exists x. (x, x -> Maybe x) , son los conaturales {0, 1, 2, ..., ∞}. Piense en los posibles valores de estos tipos para ver por qué Nu Maybe tiene un habitante adicional.

Si desea obtener algo de intuición para estos tipos, puede ser un ejercicio divertido implementar lo siguiente sin recursión (aproximadamente en orden creciente de dificultad):

• 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)

También puedes intentar implementar estos, pero requieren recursión:

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

Mu f es el punto menos fijo, y Nu f es el mejor, por lo que escribir una función :: Mu f -> Nu f es muy fácil, pero escribir una función :: Nu f -> Mu f es difícil; Es como nadar contra la corriente.

(En un momento quise escribir una explicación más detallada de estos tipos, pero podría ser demasiado largo para este formato).