Wpisywanie kombinatorki Y

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html to zwięzła definicja prosto wpisanego rachunku lambda w Prologu.

Wygląda dobrze, ale potem wydaje się, że przypisuje typ kombinatorowi Y ... podczas gdy w bardzo realnym sensie celem dodawania typów do rachunku lambda jest odmawianie przypisania typu do elementów takich jak Y kombinator.

Czy ktoś może zobaczyć, gdzie dokładnie znajduje się jego błąd lub - co bardziej prawdopodobne - moje nieporozumienie?

Answer 1

syntezatora Y w swojej podstawowej formie

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

tylko nie może być wpisany pomocą prostego systemu typu proponowanego w artykule.

Istnieją inne, o wiele łatwiej, ale znaczące przykłady, które nie mogą być wpisane na tym poziomie:

Weźmy na przykład

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

To oczywiście działa na test (\x -> x) ale nie możemy dać wyższą rangą typ, który był wymagany tutaj, mianowicie

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

ale nawet w bardziej zaawansowanych systemach typu jak rozszerzeń GHCI o Haskell, które pozwalają powyżej, Y jest nadal trudny do wpisania.

więc, biorąc pod uwagę możliwość rekursji, możemy wystarczy zdefiniować i pracę przy użyciu fix syntezatora

fix f = f (fix f) 

z fix :: (a -> a) -> a

Answer 2

Typing należy zabronić stosowania siebie, to nie powinno być możliwe, aby znaleźć typ dla (t t). Jeśli to możliwe, to t będzie miał typ A -> B, a my będziemy mieć A = A -> B. Ponieważ samozastosowanie jest częścią kombinatora Y, nie można go również podać.

Niestety wiele systemów Prolog pozwala na rozwiązanie dla A = A -> B. Dzieje się tak na wielu podstawach: albo system Prolog zezwala na terminy kołowe, a następnie proces unifikacji powiedzie się, a wynikowe powiązania będą dalej przetwarzane. Lub system Prolog nie zezwala na terminy kołowe, a następnie zależy od tego, czy implementuje sprawdzanie występowania. Jeśli wystąpi zaznaczenie, to zjednoczenie się nie powiedzie. Jeśli sprawdzenie jest wyłączone, to zjednoczenie może się powieść, ale wynikowe wiązania nie mogą być dalej przetwarzane, najprawdopodobniej prowadząc do przepełnienia stosu podczas drukowania lub dalszych unifikacji.

Sądzę więc, że cykliczne ujednolicenie tego typu dzieje się w danym kodzie przez używany system Prolog i zostaje niezauważone.

Jednym ze sposobów rozwiązania tego problemu może być włączenie sprawdzania występowania lub zastąpienie dowolnej z występujących unifikacji w kodzie za pomocą wyraźnego wywołania unify_with_occurs_check/2.

Pozdrowienia

P.S.: Poniższy kod Prolog działa lepiej:

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

Oto kilka biegnie przykładowe:

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)