Y コンビネータを入力する

Question

http://muaddibspace.blogspot.com/2008/01/type-in​​ference-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)  

しかし、上記を可能にする Haskell の GHCI 拡張機能のような、より高度な型システムでも、 Y まだ入力するのが難しいです。

したがって、再帰の可能性を考えると、次のようになります。 ただ定義するだけ を使用して作業します fix コンビネータ

fix f = f (fix f) 

と fix :: (a -> a) -> a

Answer 2

入力では自己適用を禁止する必要があり、タイプを見つけることができないようにする必要があります。 (t t). 。可能であれば、 t タイプがあるだろう A -> B, 、そして私たちはそうするでしょう A = A -> B. 。自己アプリケーションは Y コンビネータの一部であるため、それに型を与えることもできません。

残念ながら、多くの Prolog システムでは次のような問題を解決できます。 A = A -> B. 。これはさまざまな理由で発生します。Prolog システムで循環用語が許可されている場合、統合が成功し、結果として得られるバインディングをさらに処理できるようになります。または、Prolog システムが循環用語を許可していない場合は、発生チェックを実装するかどうかによって異なります。発生チェックがオンになっている場合、統合は成功しません。発生チェックがオフの場合、統合は成功する可能性がありますが、結果のバインディングをそれ以上処理することはできず、印刷時またはさらなる統合でスタック オーバーフローが発生する可能性が高くなります。

したがって、このタイプの循環統合は、使用されている Prolog システムによって指定されたコード内で発生し、気付かれないのだと思います。

この問題を解決する 1 つの方法は、発生チェックをオンにするか、コード内で発生する統合を unify_with_occurs_check/2 への明示的な呼び出しによって置き換えることです。

よろしくお願いします

追記：次の 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)