17

Haskellのラムダ計算、特にチャーチ数で遊んでいます。私は次のように定義しています：

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

これは機能します：

:t (\n -> (iszero n) one (mult one one))

これは発生チェックで失敗します：

:t (\n -> (iszero n) one (mult n one))

私は自分の定数で遊んだことがありますが、それらは正しいようiszeroです。multこれを入力可能にする方法はありますか？自分のやっていることはあまりにもクレイジーだとは思いませんでしたが、何か間違ったことをしているのではないでしょうか。

4

2 に答える 2

20

トップレベルで見た場合、定義は正しく、タイプも正しいです。問題は、2番目の例でnは、同じタイプを持たない2つの異なる方法で使用していることです。つまり、それらのタイプを統合することはできず、そうしようとすると無限のタイプが生成されます。それぞれの用途は独立して異なるタイプに特化しているため、同様の用途はone正しく機能します。

これを簡単な方法で機能させるには、より高いランクのポリモーフィズムが必要です。チャーチ数の正しいタイプはですが(forall a. (a -> a) -> a -> a)、上位のタイプを推測することはできず、などのGHC拡張子が必要ですRankNTypes。適切な拡張機能を有効にして（この場合はランク2のみが必要だと思います）、定義に明示的な型を指定すると、実際の実装を変更せずに機能するはずです。

上位のポリモーフィック型の使用にはいくつかの制限がある（または少なくともあった）ことに注意してください。ただし、チャーチ数をのようなものでラップすることはできます。これにより、チャーチ数にもインスタンスnewtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a)を与えることができます。Num

于 2012-10-17T20:15:45.960 に答える
5

いくつかの型署名を追加しましょう：

type Nat a = (a -> a) -> a -> a

zero :: Nat a
zero = (\f z -> z)

one :: Nat a
one = (\f z -> f z)

two :: Nat a
two = (\f z -> f (f z))

iszero :: Nat (a -> a -> a) -> a -> a -> a
iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))

mult :: Nat a -> Nat a -> Nat a
mult = (\m n -> (\s z -> m (\x -> n s x) z))

ご覧のとおり、のタイプを除いて、すべてがかなり正常に見えますiszero。

あなたの表現で何が起こるか見てみましょう：

*Main> :t (\n -> (iszero n) one n)
<interactive>:1:23:
    Occurs check: cannot construct the infinite type:
      a0
      =
      ((a0 -> a0) -> a0 -> a0)
      -> ((a0 -> a0) -> a0 -> a0) -> (a0 -> a0) -> a0 -> a0
    Expected type: Nat a0
      Actual type: Nat (Nat a0 -> Nat a0 -> Nat a0)
    In the third argument of `iszero', namely `(mult n one)'
    In the expression: (iszero n) one (mult n one)

Natエラーがエイリアスをどのように使用しているかを確認してください。

より単純な式を使用すると、実際に同様のエラーが発生する可能性があります\n -> (iszero n) one n。これが問題です。を呼び出しているのでiszero n、が必要n :: Nat (b -> b -> b)です。また、iszeros型のため、2番目と3番目の引数、nおよびone、は型がである必要がありbます。これで、次のタイプの2つの方程式ができましたn。

n :: Nat (b -> b -> b)
n :: b

和解することはできません。残念。

于 2012-10-17T20:26:34.147 に答える