4

このプログラムがタイプ可能でない理由がわかりません:

type Test a = forall z. (a -> z) -> z

cons :: a -> Test a
cons = \a -> \p -> p a

type Identity = forall x. x -> x

t :: Identity
t = \x -> x

c :: Test Identity
c = cons (t :: Identity)

main :: IO ()
main = do{
  print "test"
}

-XRankNTypes私はGHC でオプションを使用します。

次のエラーがあります。

Couldn't match type `x0 -> x0' with `forall x. x -> x'
Expected type: Identity
  Actual type: x0 -> x0
In the first argument of `cons', namely `(t :: Identity)'
In the expression: cons (t :: Identity)
In an equation for `c': c = cons (t :: Identity)

誰か助けてくれませんか？

4

1 に答える 1

5

との推論RankNTypesはトリッキーです。引数の代わりに関数に注釈を付けてみてください。

c :: Test Identity
c = (cons :: Identity -> Test Identity) t

なぜそうなるのかは、型推論アルゴリズムの複雑さを掘り下げる必要があります。その背後にはいくつかの直感があります。

直観的には、ポリモーフィック値x :: forall a. F(a)が使用されるときはいつでも、型変数aがポリモーフィック型に自動的にインスタンス化されることはありません。むしろ、a「未知の」新しい変数(単相a0型に及ぶ) に置き換えられます。次に、この変数を使用して型式を生成し、後で単一化を使用して解決します。

例：

id id :: ??

id02 つの出現をと と呼びましょうid1。我々が得る

id0 id1 :: ?? 
id0 :: forall a. a->a
id1 :: forall a. a->a

新しい変数をインスタンス化する

id0 :: a0 -> a0
id1 :: a1 -> a1

引数の型を統一: a0 ~ (a1 -> a1).

id0 :: (a1 -> a1) -> (a1 -> a1)
id1 :: a1 -> a1

申し込み。

id0 id1 :: a1 -> a1

再一般化します。

id0 id1 :: forall a. a->a

この特定のケースでは、a0 ~ (forall a. a->a)代わりに統合し、新しい unknown の生成を回避することで、同じ最終結果を得ることができたことに注意してくださいa1。ただし、これは推論アルゴリズムで起こっていることではありません。

手動入力に頼れば、後者のインスタンス化を実現できます。

(id :: (forall a. a->a) -> (forall a. a->a)) id

ただし、上記の説明にはいくつかの例外があります。主なものはランク 2 (およびランク N) タイプです。GHC が関数のランクが高いことを知っている場合、その引数は別の方法で処理されます:forallその型で発生する量化された変数は未知数に置き換えられません。むしろ、forall関数が期待する型と後で照合できるように、 s は保持されます。

何が起こっているのかを少し説明しているGHCユーザーガイドを読むことをお勧めします。代わりにすべての血みどろの詳細が必要な場合は、実際の入力規則について説明している論文を参照する必要があります。(実際には、それらを読む前に、基本的な Hindley–Milner などのいくつかの単純なシステムの背景を学びます)。

于 2014-11-24T16:42:03.723 に答える