Escribiendo el combinador Y

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html es una definición concisa del cálculo lambda simplemente tipeado en Prolog.

Se ve bien, pero luego pretende asignar un tipo al combinador Y ... mientras que en un sentido muy real, el propósito de agregar tipos al cálculo lambda es negarse a asignar un tipo a cosas como el Y combinador.

¿Alguien puede ver exactamente dónde está su error o, más probablemente, mi malentendido?

Answer 1

El combinador Y en su forma básica

Y f = (\x -> f (x x)) (\x -> f (x x)) 

simplemente no puede ser mecanografiadas utilizando el sistema de tipo simple propuesto en el artículo.

Hay otra, mucho más fácil, pero ejemplos significativos que no se pueden escribir en ese nivel:

Tome por ejemplo,

test f = (f 1, f "Hello") 

Obviamente, esto funciona para test (\x -> x) pero no podemos dar el tipo de mayor puntuación que se requiere aquí, a saber

test :: (∀a . a -> a) -> (Int, String) 

Pero incluso en los sistemas de tipo más avanzadas como las extensiones ghci de Haskell que permiten la arriba, Y todavía es difícil de escribir.

Por lo tanto, dada la posibilidad de recursividad, podemos acaba de definir y el trabajo con el fix combinador

fix f = f (fix f) 

con fix :: (a -> a) -> a

Answer 2

Typing debe no permitir la aplicación de auto, que no debería ser posible encontrar un tipo para (t t). Si fuera posible, entonces t tendría un tipo A -> B, y tendríamos A = A -> B. Como la autoaplicación es parte del combinador Y, tampoco es posible darle un tipo.

Desafortunadamente, muchos sistemas Prolog permiten una solución para A = A -> B. Esto sucede por muchas razones, ya sea que el sistema Prolog permita términos circulares, luego la unificación tendrá éxito y las consolidaciones resultantes pueden procesarse aún más. O el sistema Prolog no permite términos circulares, entonces depende de si implementa un cheque de ocurrencia. Si la comprobación de ocurrencia está activada, la unificación no tendrá éxito. Si la comprobación de ocurrencia está desactivada, entonces la unificación puede tener éxito, pero los enlaces resultantes no pueden procesarse más, lo que probablemente conduzca al desbordamiento de la pila en la impresión o en otras unificaciones.

Supongo que una unificación circular de este tipo ocurre en el código dado por el sistema Prolog usado y pasa inadvertido.

Una forma de resolver el problema sería activar la comprobación de ocurrencias o reemplazar alguna de las uniones existentes en el código mediante una llamada explícita a unify_with_occurs_check/2.

Saludos cordiales

P.S.: El siguiente código Prolog funciona mejor:

/** 
* Simple type inference for lambda expression. 
* 
* Lambda expressions have the following syntax: 
* apply(A,B): The application. 
* [X]>>A: The abstraction. 
* X: A variable. 
* 
* Type expressions have the following syntax: 
* A>B: Function domain 
* 
* To be on the save side, we use some unify_with_occurs_check/2. 
*/ 

find(X,[Y-S|_],S) :- X==Y, !. 
find(X,[_|C],S) :- find(X,C,S). 

typed(C,X,T) :- var(X), !, find(X,C,S), 
       unify_with_occurs_check(S,T). 
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T). 
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
       unify_with_occurs_check(S,T). 

Estas son algunas carreras de muestra:

Jekejeke Prolog, Development Environment 0.8.7 
(c) 1985-2011, XLOG Technologies GmbH, Switzerland 
?- typed([F-A,G-B],apply(F,G),C). 
A = B > C 
?- typed([F-A],apply(F,F),B). 
No 
?- typed([],[X]>>([Y]>>apply(Y,X)),T). 
T = _T > ((_T > _Q) > _Q)