5

関数型プログラミングの講義中に、次の Haskell 関数を見ました。

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

この関数は型チェックに失敗することが予想されます。しかし、これが起こる理由は説明されていませんでした。GHCIで試してみると、次の出力が得られました。

Prelude> :l test [1 of 1] Main のコンパイル ( test.hs,
解釈された）

test.hs:2:35:
    予想される型「a」を実際の型「Bool」と一致させることができませんでした
      「a」は、によって束縛される固定型変数です。
          f :: Bool -> Int -> (a -> Int) -> Int の型シグネチャ
          test.hs:1:6 で
    関連するバインディングには次のものがあります。
      z :: a -> Int (test.hs:2:7 でバインド)
      f :: Bool -> Int -> (a -> Int) -> Int (test.hs:2:1 でバインド)
    `z' の最初の引数、つまり `x'
    `(+)' の最初の引数、つまり `(zx)' で失敗しました。ロードされたモジュール: なし。

なぜこれが起こるのですか？

4

3 に答える 3

9 
f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

型シグネチャは、関数zが最初の引数で多態的であることを表明します。任意の型の値を取り、aを返しますInt。ただし、型変数のスコープは、すべての使用aにおいて同じ型でなければならないことも意味します。同じ使用サイトで異なるタイプにインスタンス化することはできません。これが「ランク1ポリモーフィズム」です。aa

タイプは実際には次のように読み取ることができます。

f :: forall a. Bool -> Int -> (a -> Int) -> Int

そう：

z (x :: Bool) + z (y :: Int)

aは、 2 つの異なる独立した型に制約されているため、無効です。

言語拡張により、 のスコープを変更しaて、ポリモーフィック変数にインスタンス化できるようにすることができます。つまり、ポリモーフィック関数型を持つことを含め、同じ使用場所で異なる型を保持できます。

Prelude> :set -XRankNTypes

Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int 
             f x y z = if x then y + y else (z x) + (z y)

現在、型aにはグローバル スコープがなく、個々のインスタンス化は異なる場合があります。これにより、「より多態的な」関数fを記述して使用できます。

Prelude> f True 7 (const 1)
14

それが、上位ポリモーフィズムのクールなところです。より多くのコードを再利用します。

于 2014-09-16T11:07:54.520 に答える
2

平

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z y) + (z y)

Haskellは式の最も一般的でない型を推測し、あなたの型は推測されたものよりも一般的であるため、(コメントで指摘されたように)型チェックを行わず、同じエラーを生成します。「Haskell のやさしい入門」で述べられているように、

式または関数のプリンシパル型は、直観的に「式のすべてのインスタンスを含む」最も一般的でない型です。

型を明示的に指定すると、Haskell は何らかの理由でそれを行ったと見なし、推論された型を指定された型に一致させることを主張します。

上記の式では、推論された型は(Num t) => Bool -> t -> (t -> t) -> tであるため、型を一致させると、 Intforを指定したことがわかりy、 の型は にzなり(Int -> Int)ます。これはよりも一般的ではありません(a -> Int)。しかし、あなたaはそこに ( ではなくInt) —固定型変数を持つことを主張しました。言い換えれば、f関数は type の関数のみを受け入れることができますが、などを含む任意のfunctionをInt -> Int指定できると主張しています(@augustsson がコメントで指摘しているように)。宣言された型が広すぎます。:: a -> Int:: String -> Int

同様に、1つしかない場合は(z x)、指定された型と一致し、関数のx宣言された型よりも狭い型に到達します。また、固定型変数について不平を言います。(Bool -> Int)z

実際には、型を宣言しました(Num t) => Bool -> t -> (t1 -> t) -> tが、実際には(Num t) => Bool -> t -> (t -> t) -> t. 違うタイプです。

于 2014-09-16T16:19:49.163 に答える