Escribir el combinador Y

Question

http: //muaddibspace.blogspot. com / 2008/01 / mecanografiado simplemente de tipo inferencia-para-lambda.html- es una definición concisa del cálculo lambda simplemente escrito en Prolog.

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

Puede alguien ver exactamente donde su error o - más probablemente - mi malentendido es

Answer 1

The Y combinador en su forma básica

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

Sólo no puede ser escrito 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 puede dar el tipo de mayor puntuación que se requiere aquí, a saber

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

Sin embargo, incluso en los sistemas de tipo más avanzadas como las extensiones ghci de Haskell que permiten lo anterior, Y es todavía difícil de escribir.

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

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 de (t t). Si en lo posible t entonces tendría un A -> B tipo, y que tendríamos que A = A -> B. Como la aplicación de auto es parte de Y Combinator, su también no es posible dar un tipo a ella.

Desafortunadamente muchos sistemas Prolog permiten una solución para A = A -> B. Esto sucede por muchas razones, ya sea el sistema Prolog permite términos circulares, entonces la unificación tendrán éxito y los enlaces resultantes pueden aún más ser procesada. O el sistema de Prolog no permite términos circulares, entonces depende de si se implementa un cheque ocurre. Si se efectúe la verificación está activada, entonces la unificación no tendrá éxito. Si el cheque se produce está apagado, entonces la unificación podría tener éxito, pero los enlaces resultantes no pueden ser además procesados, más probable es que lleva a desbordamiento de pila en la impresión o más unificaciones.

Así que supongo que una unificación circular de este tipo que ocurre en el código dado por el sistema Prolog usado y se pone desapercibido.

Una manera de resolver el problema sería la de cualquiera de los interruptores se produce en el cheque o para sustituir a cualquiera de las unificaciones que ocurren en el código mediante una llamada explícita a unify_with_occurs_check / 2.

Saludos

P.S .: funciona El siguiente código Prolog 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).

Aquí están algunas carreras de ejemplo:

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)