7

http://muaddibspace.blogspot.com/2008/01/type-in​​ference -for-simply-typed-lambda.html は、Prolog の単純型付けラムダ計算の簡潔な定義です。

それは問題ないように見えますが、彼は Y コンビネータに型を割り当てることを主張しています... 一方、非常に現実的な意味で、ラムダ計算に型を追加する全体的な目的は、Y コンビネータのようなものに型を割り当てることを拒否することです。

彼の間違い、あるいはおそらく私の誤解がどこにあるのか、正確にわかる人はいますか?

4

2 に答える 2

8

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

于 2010-09-13T17:45:00.177 に答える
3

タイピングは自己適用を禁止する必要があり、 のタイプを見つけることができないようにする必要があります(t t)。可能であればt、 type を持ち、A -> Bを持ちA = A -> Bます。自己適用は Y コンビネーターの一部であるため、型を与えることもできません。

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

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

この問題を解決する 1 つの方法は、発生チェックを有効にするか、コード内で発生している統合を 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)
于 2011-02-10T21:12:01.247 に答える