2

単純に型指定されたラムダ計算型チェッカーを実装しようとしています。サニティ テストを実行しているときに (SKK) と入力しようとすると、型チェッカーが次のエラーをスローします。

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

問題のある用語は明らかに（SKK）です

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

この Haskell コードをタイプチェックすると正常に動作するため、ポリモーフィズムの欠如から問題が発生すると思います。

k x y = x
s x y z = x z (y z)
test = s k k -- type checks

しかし、私がタイプを特化した場合:

k :: () -> () -> ()
k x y = x
s :: (() -> () -> ()) -> (() -> ()) -> () -> ()
s x y z = x z (y z)
test = s k k -- doesn't type check

参考までに、私の型システムは次のように単純です。

data Type = T | TArr Type Type

完全なソース

4

1 に答える 1

9

私の以前の回答からアイデアを盗んで、ghciに質問する方法を示します。しかし、最初に、あなたの質問を少し再定式化します。

Haskell では、

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: a -> b -> a

そして、私たちが聞きたい質問は、「これらの型は、型チェック後にどのように見えるs k kか?」です。さらに言えば、それらを個別の統一変数で書き直すと、

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
k :: d -> e -> d
k :: f -> g -> f
s k k :: h

s次に、問題は統一の問題になります。 の型を、それが使用されている型、つまり で統一しようとしています(d -> e -> d) -> (f -> g -> f) -> h。統一の質問が手元にあるので、他の回答に示されている形式で質問できます。

> :{
| :t undefined
| ::   ((a -> b -> c) -> (a -> b) -> (a -> c))
|    ~ ((d -> e -> d) -> (f -> g -> f) -> h)
| => (a, b, c, d, e, f, g, h)
| :}
undefined
::   ((a -> b -> c) -> (a -> b) -> (a -> c))
   ~ ((d -> e -> d) -> (f -> g -> f) -> h)
=> (a, b, c, d, e, f, g, h)
  :: (f, g -> f, f, f, g -> f, f, g, f -> f)

これで、バージョンが機能しない理由がわかります。バージョンでは、すべてのポリモーフィック変数を基本型にインスタンス化しましたT。しかし、b ~ g -> f、e ~ g -> f、およびh ~ f -> fは明らかに矢印タイプであるため、それは確かに機能しません! ただし、上記の置換を尊重すればf、 との任意の選択が機能します。g特に、 と を選択するf ~ Tとg ~ T、次のようになります。

s :: (T -> (T -> T) -> T) -> (T -> (T -> T)) -> (T -> T)
k1 :: T -> (T -> T) -> T
k2 :: T -> T -> T
s k1 k2 :: T -> T
于 2016-03-10T00:37:00.510 に答える