haskell lambda-calculus church-encoding

Resta de numerales de iglesia en haskell



lambda-calculus church-encoding (3)

Estoy intentando implementar números de iglesia en Haskell, pero he encontrado un problema menor. Haskell se queja de un tipo infinito con

Se produce una comprobación: no se puede construir el tipo infinito: t = (t -> t1) -> (t1 -> t2) -> t2

Cuando intento hacer la resta. Estoy 99% seguro de que mi cálculo lambda es válido (aunque si no lo es, por favor dígamelo). Lo que quiero saber es si hay algo que pueda hacer para que haskell funcione con mis funciones.

module Church where type (Church a) = ((a -> a) -> (a -> a)) makeChurch :: Int -> (Church a) makeChurch 0 = /f -> /x -> x makeChurch n = /f -> /x -> f (makeChurch (n-1) f x) numChurch x = (x succ) 0 showChurch x = show $ numChurch x succChurch = /n -> /f -> /x -> f (n f x) multChurch = /f2 -> /x2 -> /f1 -> /x1 -> f2 (x2 f1) x1 powerChurch = /exp -> /n -> exp (multChurch n) (makeChurch 1) predChurch = /n -> /f -> /x -> n (/g -> /h -> h (g f)) (/u -> x) (/u -> u) subChurch = /m -> /n -> (n predChurch) m

El problema es que predChurch es demasiado polimórfico para ser inferido correctamente por la inferencia de tipo Hindley-Milner. Por ejemplo, es tentador escribir:

predChurch :: Church a -> Church a predChurch = /n -> /f -> /x -> n (/g -> /h -> h (g f)) (/u -> x) (/u -> u)

pero este tipo no es correcto A Church a toma como primer argumento a -> a , pero está pasando n una función de dos argumentos, claramente un error de tipo.

El problema es que la Church a no caracteriza correctamente un número de Iglesia. Un número de Iglesia simplemente representa un número. ¿Qué demonios podría significar ese tipo de parámetro? Por ejemplo:

foo :: Church Int foo f x = f x `mod` 42

Eso se comprueba, pero foo ciertamente no es un número de Iglesia. Necesitamos restringir el tipo. Los números de la iglesia deben trabajar para cualquier a , no solo una específica. La definición correcta es:

type Church = forall a. (a -> a) -> (a -> a)

Necesitas tener {-# LANGUAGE RankNTypes #-} en la parte superior del archivo para habilitar tipos como este.

Ahora podemos dar el tipo de firma que esperamos:

predChurch :: Church -> Church -- same as before

Debe dar una firma de tipo aquí porque los tipos de rango más alto no son inferibles por Hindley-Milner.

Sin embargo, cuando vamos a implementar subChurch surge otro problema:

Couldn''t match expected type `Church'' against inferred type `(a -> a) -> a -> a''

No estoy 100% seguro de por qué sucede esto, creo que el forall está desplegando de manera demasiado liberal. Aunque no me sorprende; Los tipos de rango superior pueden ser un poco frágiles debido a las dificultades que presentan para un compilador. Además, no deberíamos usar un type para una abstracción , deberíamos usar un newtype (que nos da más flexibilidad en la definición, ayuda al compilador con la comprobación de tipo y marca los lugares donde usamos la implementación de la abstracción):

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

Y tenemos que modificar predChurch para rodar y desenrollar según sea necesario:

predChurch = /n -> Church $ /f -> /x -> unChurch n (/g -> /h -> h (g f)) (/u -> x) (/u -> u)

Lo mismo con subChurch :

subChurch = /m -> /n -> unChurch n predChurch m

Pero ya no necesitamos firmas de tipo: hay suficiente información en el rollo / desenrollado para inferir tipos nuevamente.

Siempre recomiendo newtype s al crear una nueva abstracción. Los sinónimos de type regular son bastante raros en mi código.

Me he encontrado con el mismo problema. Y lo resolví sin agregar tipo de firma.

Aquí está la solución, con los car copia copiados de SICP .

cons x y = /m -> m x y car z = z (/p q -> p) cdr z = z (/p q -> q) next z = cons (cdr z) (succ (cdr z)) pred n = car $ n next (cons undefined zero) sub m n = n pred m

Puedes encontrar la fuente completa here .

¡Estoy realmente sorprendido después de escribir sub mn = n pred m , y cargarlo en ghci sin error de tipo!

¡El código de Haskell es tan conciso! :-)