Taper le Y Combinator

Question

http: //muaddibspace.blogspot. com / 2008/01 / type inférence pour-simplement typé-lambda.html est une définition concise du lambda-calcul simplement typé en Prolog.

Il a l'air bien, mais il prétend attribuer un type à Y Combinator ... alors que dans un sens très réel tout l'objet de l'ajout de types de lambda-calcul est de refuser d'attribuer un type à des choses comme le Y Combinator .

Quelqu'un peut-il voir exactement où son erreur ou - plus probablement - mon malentendu est

Answer 1

Le combinateur Y sous sa forme de base

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

juste ne peut pas être typé en utilisant le système de type simple proposé dans l'article.

Il existe d'autres, beaucoup plus facile, mais des exemples significatifs qui ne peuvent être tapés à ce niveau:

Prenez par exemple.

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

Cela fonctionne évidemment pour test (\x -> x) mais nous ne pouvons donner le type de rang supérieur qui était nécessaire ici, à savoir

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

Mais même dans les systèmes de type plus avancés comme les extensions ghci de Haskell qui permettent au-dessus, Y est encore difficile à saisir.

Ainsi, compte tenu de la possibilité de récursivité, nous pouvons définir simplement et le travail en utilisant le fix Combinator

fix f = f (fix f) 

avec fix :: (a -> a) -> a

Answer 2

Le texte dactylographié doit interdire l'application de l'auto, il ne devrait pas être possible de trouver un type pour (t t). S'il si possible t aurait alors un A -> B de type, et nous aurions A = A -> B. Depuis l'application de l'auto fait partie de Y Combinator, son pas possible de donner un type à lui.

Malheureusement, de nombreux systèmes Prolog permettent une solution pour A = A -> B. Cela se produit pour plusieurs raisons, que ce soit le système Prolog permet termes circulaires, puis l'unification réussiront et les liaisons résultantes peuvent encore être traitées. Ou le système Prolog ne permet pas de termes circulaires, il dépend si elle met en œuvre un contrôle se produit. Si le contrôle se produit est activé, l'unification ne réussira pas. Si le contrôle se produit est éteint, l'unification pourrait réussir, mais les liaisons résultantes ne peut pas encore être traitées, la plupart des principales susceptibles de débordement de la pile dans l'impression ou unifications autres.

Je suppose une unification circulaire de ce type se produit dans le code donné par le système Prolog utilisé et il obtient inaperçu.

Une façon de résoudre le problème serait soit d'activer la vérification se produit ou pour remplacer l'un des unifications de INTERVENUES dans le code par un appel explicite à unify_with_occurs_check / 2.

Cordialement

P.S .: Le code suivant Prolog fonctionne mieux:

/**
 * 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).

Voici quelques exemples de pistes:

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)