http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html е кратка дефиниция на просто въведеното ламбда смятане в Prolog.
Изглежда добре, но след това той претендира да присвои тип на Y комбинатора... докато в много реален смисъл цялата цел на добавянето на типове към ламбда смятането е да се откаже да се присвои тип на неща като Y комбинатора.
Може ли някой да види точно къде е неговата грешка или - по-вероятно - моето недоразумение?
Комбинаторът Y в основната му форма
Y f = (\x -> f (x x)) (\x -> f (x x))
просто не може да се въведе с помощта на простата система за въвеждане, предложена в статията.
Има други, много по-лесни, но смислени примери, които не могат да бъдат въведени на това ниво:
Вземете напр.
test f = (f 1, f "Hello")
Това очевидно работи за test (\x -> x), но не можем да дадем типа с по-висок ранг, който се изисква тук, а именно
test :: (∀a . a -> a) -> (Int, String)
Но дори в по-усъвършенствани типови системи като GHCI разширенията на Haskell, които позволяват горното, Y все още е трудно за въвеждане.
Така че, предвид възможността за рекурсия, можем просто да дефинираме и да работим с помощта на fix комбинатора
fix f = f (fix f)
с fix :: (a -> a) -> a
Въвеждането трябва да забранява самоприлагане, не трябва да е възможно да се намери тип за (t t). Ако е възможно, тогава t ще има тип A -> B, а ние ще имаме A = A -> B. Тъй като самостоятелното приложение е част от Y комбинатора, също не е възможно да му се даде тип.
За съжаление много системи Prolog позволяват решение за A = A -> B. Това се случва на много основания, или системата Prolog позволява кръгови условия, тогава обединението ще успее и получените обвързвания могат дори да бъдат допълнително обработени. Или системата Prolog не позволява кръгови условия, тогава зависи от това дали прилага проверка за възникване. Ако проверката за възникване е включена, обединяването няма да успее. Ако проверката за възникване е изключена, тогава обединението може да успее, но получените обвързвания не могат да бъдат допълнително обработени, което най-вероятно води до препълване на стека при печат или по-нататъшни обединения.
Така че предполагам, че кръгова унификация от този тип се случва в дадения код от използваната система Prolog и остава незабелязана.
Един от начините за решаване на проблема би бил или да включите проверката за възникване, или да замените всяко от възникващите обединения в кода чрез изрично извикване на unify_with_occurs_check/2.
С Най-Добри Пожелания
P.S.: Следният Prolog код работи по-добре:
/**
* 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).
Ето някои примерни изпълнения:
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)
