Набрать комбинатор Y

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html это краткое определение простого напечатанного исчисления Lambda в 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

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

К сожалению, многие системы пролога позволяют решению для 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)