Typisierung des Y-Kombinators

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html ist eine präzise Definition des einfach typisierten Lambda-Kalküls in Prolog.

Es sieht okay aus, aber dann gibt er vor, dem Y-Kombinator einen Typ zuzuordnen ... wohingegen der gesamte Zweck des Hinzufügens von Typen zu Lambda-Kalkül in einem sehr realen Sinn darin besteht, einen Typ auf Dinge wie das Y zu verzichten Kombinator.

Kann jemand genau sehen, wo sein Fehler oder - wahrscheinlicher - mein Missverständnis ist?

Answer 1

Die Y Combinator in seiner Grundform

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

nur nicht mit dem einfachen Art System in dem Artikel vorgeschlagen eingegeben werden kann.

Es gibt noch andere, viel einfacher, aber aussagekräftige Beispiele, die nicht auf dieser Ebene eingegeben werden können:

Nehmen Sie zum Beispiel

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

Dies funktioniert natürlich für test (\x -> x) aber wir können nicht die ranghöheren Art geben, die hier erforderlich war, nämlich

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

Aber auch in fortgeschritteneren Typ Systeme wie die GHCI Erweiterungen von Haskell, die das ermöglichen, oben, Y ist immer noch schwer zu tippen.

also die Möglichkeit der Rekursion gegeben, können wir nur und Arbeit definieren mit dem fix combinator

fix f = f (fix f) 

mit fix :: (a -> a) -> a

Answer 2

Typing sollte Selbst Anwendung nicht zulassen, sollte es nicht möglich sein, zu finden ein Typ für (t t). Wenn es möglich wäre, dann hätte t einen Typ A -> B, und wir hätten A = A -> B. Da die Selbstanwendung Teil des Y-Kombinators ist, ist es auch nicht möglich, einen Typ anzugeben.

Leider erlauben viele Prolog-Systeme eine Lösung für A = A -> B. Dies geschieht aus vielen Gründen, entweder erlaubt das Prolog-System zirkuläre Terme, dann wird die Vereinigung erfolgreich sein und die resultierenden Bindungen können noch weiter verarbeitet werden. Oder das Prolog-System erlaubt keine zirkulären Terme, dann kommt es darauf an, ob es eine Vorkommnis-Prüfung implementiert. Wenn die Überprüfung aktiviert ist, ist die Vereinigung nicht erfolgreich. Wenn die Prüfung auf tritt aus ist, kann die Vereinigung erfolgreich sein, aber die resultierenden Bindungen können nicht weiter verarbeitet werden, was höchstwahrscheinlich zu einem Stapelüberlauf beim Drucken oder weiteren Vereinheitlichungen führt.

Also ich denke, eine kreisförmige Vereinheitlichung dieses Typs geschieht in dem angegebenen Code durch das verwendete Prolog-System und es wird unbemerkt.

Eine Möglichkeit, das Problem zu lösen, wäre, entweder die Vorkommnisprüfung zu aktivieren oder eine der auftretenden Unifikationen im Code durch einen expliziten Aufruf von unify_with_occurs_check/2 zu ersetzen.

Mit freundlichen Grüßen

P.S.: Der folgende Prolog-Code funktioniert besser:

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

Hier sind einige Beispiele für Läufe:

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)