16

型チェッカーを通過する次の関数定義のペアを考えてみましょう。

a :: forall a. a
a = undefined

b :: Int
b = a

つまり、forall a. a型の式が期待される場所で、型の式を使用できますInt。これはサブタイピングによく似ているように思えますが、Haskell の型システムにはサブタイピングがないと言われています。これらの代替可能性の形態はどのように異なるのでしょうか?

この質問は に固有のものではありませんforall a. a。その他の例は次のとおりです。

id :: forall a. a -> a
id x = x

idInt :: Int -> Int
idInt = id
4

5 に答える 5

11

このような質問があれば、私は一歩下がって、基本的に、Haskell の設計の根底にある数学的理論は、サブタイプの概念を持たない System Fバリアントであると言います。

Tはい、Haskell の表面構文を見て、予想される任意のコンテキストで何らかの型の式を使用できる、あなたが持ち出したようなケースがあることに気付くことができますT'。しかし、Haskell はサブタイプをサポートするように設計されているため、これは発生しません。むしろ、Haskell が System F の忠実なレンダリングよりもユーザーフレンドリーになるように設計されたという事実の偶然として生じます。

この場合、型レベルの量指定子は通常、Haskell コードで明示的に記述されておらず、型レ​​ベルのラムダとアプリケーションは決して明示的に記述されていないという事実に関係しています。forall a. aSystem F の角度から型を見ると、Intコンテキストへの代入可能性は失われます。 a :: forall a. aは型レベルの関数であり、期待されるコンテキストでは使用できません。最初に getにInt適用する必要があります。これは、コンテキストで実際に使用できるものです。Haskell の構文は、使いやすさという名目でそれを隠していますが、基礎となる理論にはそれがあります。Inta Int :: IntInt

つまり、どの式の型をどのコンテキストの型に代入できるかを表にして Haskell を分析し、ある種の暗号サブタイプの関係があることを示すことはできますが、設計の流れに逆らって泳ぐ分析が得られるため、実りはありません。 . そして、それは意図やその他の人的要因の問題であるため、技術的な問題ではありません.

于 2015-09-23T19:34:34.703 に答える
3

これ:: aは「任意のタイプ」を意味しますが、サブタイプではありません。、または、またはであるa 可能性がありますが、特にありません。正確には型ではなく、型変数です。IntBoolIO (Maybe Ordering)a

次のような関数があるとします。

id x = x

コンパイラは、引数に特定の型がないことを理解していますx。id から得られるものと同等である限り、任意の型をに使用できます。xしたがって、署名を次のように記述します。

--    /- Any type in...
--    |    /- ...same type out.
--    V    V
id :: a -> a

Haskell では、型は大文字で始まることに注意してください。これは型ではありません: 型変数です!

ポリモーフィズムを使用するのは、そのほうが簡単だからです。たとえば、コンポジションは便利なアイデアです。

(>>>) :: (a -> b) -> (b -> c) -> (a -> c)
(>>>) f g a = g (f a)

したがって、次のように書くことができます。

plusOneTimesFive :: Int -> Int
plusOneTimesFive = (+1) >>> (* 5)

reverseHead :: [Bool] -> Bool
reverseHead = reverse >>> head

しかし、すべての型を次のように書き出す必要があるとしたらどうでしょうか。

(>>>) :: (Bool -> Int) -> (Int -> String) -> (Bool -> String)
(>>>) f g a = g (f a)

(>>>') :: (Ordering -> Double) -> (Double -> IO ()) -> (Ordering -> IO ())
(>>>') f g a = g (f a)

(>>>'') :: (Int -> Int) -> (Int -> Bool) -> (Int -> Bool)
(>>>'') f g a = g (f a)

-- ...and so on.

それはばかげているでしょう。

したがって、コンパイラは次のように型の統合を使用して型を推測します。

これをGHCiに入力するとしましょう。ここでは簡単6にするために で言いましょう。Int

id 6

コンパイラは次のように考えます: " 、そして、 , so , soid :: a -> aが渡されます。Inta = Intid 6 :: Int

これはサブタイプではありません。サブタイプは型クラスを使用してキャプチャできますが、これは基本的なポリモーフィズムです。

于 2015-09-23T19:14:12.013 に答える
2

サブタイプ化ではなく、型の統合です!

a :: forall a. a
a = undefined

b :: Int
b = a

では、 と が同じ型になるようにb = a制約bしaているため、コンパイラはそれが可能かどうかをチェックします。atypeforall a. aは、定義により、すべての型と統合されるため、コンパイラは制約を受け入れます。

型の統一により、次のようなこともできます。

f :: (a -> Int) -> a
g :: (String -> b) -> b
h :: String -> Int
h = f g

統合をたどると、f :: (a -> Int) -> a手段はgtype を持つ必要があります。これは、と統合する必要がa -> Intあることを意味a -> Intし(String -> b) -> b、 so bmust bbeIntである必要があります。g(String -> Int) -> IntaString -> Int

どちらa -> Intも(String -> b) -> b他方のサブタイプではありませんが、 として統合できます(String -> Int) -> Int。

于 2015-09-23T19:10:33.500 に答える