Набрав Y combinator

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html - краткое определение просто типизированного лямбда-исчисления в Prolog.

Это выглядит нормально, но тогда он намерен присвоить тип Y комбинатору ... тогда как в самом реальном смысле цель цели добавления типов в лямбда-исчисление - отказаться от присвоения типа вещам типа Y комбинатор.

Может ли кто-нибудь увидеть, где его ошибка или, скорее, мое недоразумение?

Answer 1

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

Answer 2

Typing должны запретить само приложение, оно не должно быть возможно найти тип для (t t). Если это возможно, то t будет иметь тип A -> B, и у нас было бы A = A -> B. Поскольку само приложение является частью комбинатора Y, его также невозможно указать на него.

К сожалению, многие системы Prolog позволяют решение для A = A -> B. Это происходит по многим причинам: либо система Пролога допускает круговые термины, то унификация будет успешной, и результирующие привязки могут быть еще обработаны. Или система Prolog не разрешает круговые термины, тогда это зависит от того, реализует ли она проверку на наличие. Если проверка происходит, то объединение не будет выполнено. Если проверка выполнения отключена, то унификация может завершиться успешно, но результирующие привязки больше не могут быть обработаны, что, скорее всего, приведет к переполнению стека при печати или дальнейших унификациях.

Таким образом, я думаю, что круговое объединение такого типа происходит в данном коде с помощью используемой системы Prolog, и это становится незамеченным.

Одним из способов решения проблемы является либо включение проверки на происшествие, либо замена любого из возможных объединений в коде явным вызовом unify_with_occurs_check/2.

С наилучшими пожеланиями

P.S.: Следующий код Пролог работает лучше:

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