Cálculo lambda en Haskell: ¿hay alguna manera de hacer que los números de la Iglesia se verifiquen?

lambda-calculus church-encoding

Question

Estoy jugando con algunas cosas de cálculo lambda en Haskell, específicamente los números de la iglesia. He definido lo siguiente:

let zero = (/f z -> z)
let one = (/f z -> f z)
let two = (/f z -> f (f z))
let iszero = (/n -> n (/x -> (/x y -> y)) (/x y -> x))
let mult = (/m n -> (/s z -> m (/x -> n s x) z))

Esto funciona:

:t (/n -> (iszero n) one (mult one one))

Esto falla con una verificación de ocurrencia:

:t (/n -> (iszero n) one (mult n one))

He jugado con iszero y mult con mis constantes y parecen ser correctas. ¿Hay alguna manera de hacer esto tipificable? No pensé que lo que estaba haciendo era demasiado loco, pero ¿tal vez estoy haciendo algo mal?

Answer 1

Sus definiciones son correctas, al igual que sus tipos, cuando se ven en el nivel superior. El problema es que, en el segundo ejemplo, estás usando n de dos maneras diferentes que no tienen el mismo tipo, o más bien, sus tipos no se pueden unificar, e intentar hacerlo produciría un tipo infinito . Usos similares de one obra correctamente porque cada uso está especializado de forma independiente para diferentes tipos.

Para hacer que esto funcione de una manera directa, necesita un polimorfismo de rango superior. El tipo correcto para un número de iglesia es (forall a. (a -> a) -> a -> a) , pero los tipos de rango más alto no se pueden inferir y requieren una extensión GHC como RankNTypes . Si habilita una extensión apropiada (solo creo que necesita el rango 2 en este caso) y da tipos explícitos para sus definiciones, deberían funcionar sin cambiar la implementación real.

Tenga en cuenta que existen (o al menos hubo) algunas restricciones en el uso de tipos polimórficos de rango superior. Sin embargo, puede ajustar los números de su iglesia en algo como newtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a) , lo que también les permitiría darles un ejemplo de Num .

Answer 2

Vamos a añadir algunas firmas de tipo:

type Nat a = (a -> a) -> a -> a
zero :: Nat a
zero = (/f z -> z)
one :: Nat a
one = (/f z -> f z)
two :: Nat a
two = (/f z -> f (f z))
iszero :: Nat (a -> a -> a) -> a -> a -> a
iszero = (/n -> n (/x -> (/x y -> y)) (/x y -> x))
mult :: Nat a -> Nat a -> Nat a
mult = (/m n -> (/s z -> m (/x -> n s x) z))

Como puede ver, todo parece bastante normal, excepto el tipo de iszero .

Veamos que pasa con tu expresión:

*Main> :t (/n -> (iszero n) one n)
<interactive>:1:23:
Occurs check: cannot construct the infinite type:
a0
=
((a0 -> a0) -> a0 -> a0)
-> ((a0 -> a0) -> a0 -> a0) -> (a0 -> a0) -> a0 -> a0
Expected type: Nat a0
Actual type: Nat (Nat a0 -> Nat a0 -> Nat a0)
In the third argument of `iszero'', namely `(mult n one)''
In the expression: (iszero n) one (mult n one)

¡Vea cómo el error usa nuestro alias de Nat !

Realmente podemos obtener un error similar con la expresión más simple /n -> (iszero n) one n . Esto es lo que está mal. Como llamamos iszero n , debemos tener n :: Nat (b -> b -> b) . Además, debido a que iszero s type, el segundo y tercer argumento, n y one , deben tener el tipo b . Ahora tenemos dos ecuaciones para el tipo de n :

n :: Nat (b -> b -> b)
n :: b

Que no se puede reconciliar. Gorrón.