Ввод Y комбинатор - PullRequest
Новая
       23

Ввод Y комбинатор

6 голосов
/ 13 сентября 2010

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

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

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

Ответы [ 2 ]

7 голосов
/ 13 сентября 2010

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

2 голосов
/ 11 февраля 2011

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

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

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

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

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

PS: следующий код 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)
...