なぜフォーオールですか？ Intのサブタイプとは見なされませんが、forall型の式を使用できます。 Int型のどこでも期待されていますか？</p> <pre><code>a :: forall a. a a = undefined b :: Int b = a </code></pre><p>即ち：

Question

型チェッカーを渡す関数定義の次の対を、検討しますタイプforall a. aの表現は、タイプIntの1つが予想される場合に使用できます。これはサブタイピングに似ているようですが、Haskellの型システムにはサブタイプがないと主張されています。これらの代替可能性の形式はどのように異なるのですか？

この質問は、forall a. aに特定されていません。その他の例としては、以下が挙げられる：

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

idInt :: Int -> Int 
idInt = id 

Answer 1

型付きラムダ計算では、通常、:と表示されるか、またはハスケルで::と表示されます。一般的に、関係は「多対多」なので、型は複数の値を含むことができ、値も多くの型を持つことができます。

特に、多型システムでは、値に複数の型を持たせることができます。このようなタイプのシステムの例

map :: (a -> b) -> [a] -> [b] 

も

map :: (Int -> Int) -> [Int] -> [Int]. 

ことが意味「より一般的なタイプ」、type orderと種類に関係を定義するために（時々）が可能です。 t ⊑ sならばtはsよりも一般的であり、M : tならばM : sであり、そのようなタイプのシステムのタイピング規則はそれを正確に推論することを意味する。または、sはtの特殊化です。したがって、この意味で、型にはsubtypingの関係があります。

しかし、我々はオブジェクト指向言語でサブタイピングについて話すとき、私たちは通常nominal subtypingを意味し、つまり、私たちは、クラスの継承を定義するときのように、種類は何のサブタイプであるを宣言。 Haskellでは、宣言とは無関係に、型のプロパティです。たとえば、任意のタイプはforall a . aの特殊化です。型推論とどれが最も関数型言語のためのベースであることができHindley-Milner type systemについて

は、principal typeの概念がある：式Mは（任意）タイプを有する場合、それはまた、その主要型を有し、かつプリンシパルタイプは、Mのすべての可能なタイプの中で最も一般的なタイプです。重要な特徴は、HM型推論アルゴリズムが常に最も一般的な型を見つけることである。したがって、最も一般的で推論されたプリンシパルタイプは、有効なタイプのMに特化できます。

Answer 2

それはサブタイプではないです、それはb = aでtype unification!

a :: forall a. a 
a = undefined 

b :: Int 
b = a 

だ、我々は同じタイプであることをbとaを制約しているので、コンパイラはそれが可能であることを確認します。 aの型はforall a. aであり、これは定義によってすべての型と統一されているため、コンパイラは私たちの制約に従います。 f :: (a -> Int) -> aがgがどのので、bはbIntでなければならない必要があり、a -> Intは(String -> b) -> bで統一しなければならないことを意味タイプa -> Intを、持っていなければならないことを意味し、統一を歩い

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

：

タイプの統一も、私たちのようなものを行うことができますコンクリートタイプ(String -> Int) -> Intをgとする。これは、aがString -> Intであることを意味する。

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

Answer 3

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

は、我々はこのような機能を持っているとしましょう：

id x = x 

コンパイラは、私たちの引数xのための特定のタイプが存在しないことを理解しています。私たちはのタイプをxに使用することができます。それはidから出てくるものと同等である限りです。署名を以下のように書く：

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

タイプはHaskellの大文字で始まることに注意してください。これは型ではありません：型変数です！

私たちは多型を使用する方が簡単だからです。

(>>>) :: (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. 

：私たちは、このようにすべてのタイプを書かなければならなかった場合

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

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

しかし、どのような：

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

だから私たちはのようなものを書くことができます：例えば、組成物は、便利なアイデアですそれはただばかだ。

ので、コンパイラはそうのようなタイプの統一を使用してタイプを推測：

はのはGHCiのにI入力にこのことを言ってみましょう。ここでは簡略化のためをIntとしましょう。

id 6 

コンパイラは考えて：id 6 :: Intので、id :: a -> a」、そしてそれがIntを渡されていますので、a = Int

これはないサブタイプであるサブタイピングは、型クラスを使用して取得することができますが、これは基本的な多型です。

Answer 4

このような質問で、私は元に戻って、基本的には、ハスケルの設計の基礎をなす数学的理論は、System Fがないサブタイプのncept。

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

この場合、型レベルの量指定子は一般的にHaskellコードでは明示的に書かれておらず、型レ​​ベルlambdasとアプリケーションは決してであるという事実と関係がある。システムFの角度からタイプforall a. aを見ると、Intコンテキストへの代入可能性はなくなります。 a :: forall a. aは型レベル関数であり、Intが必要なコンテキストでは使用できません。Intに最初に適用してa Int :: Intを取得する必要があります。Intコンテキストで実際に使用できるものです。 Haskellの構文は、使いやすさという意味でそれを隠していますが、それは基本的な理論にあります。

要するに、Haskellをどのコンテキストタイプに置き換えることができ、どの種類の暗号 - サブタイプ関係があるのか​​を示すことによって、Haskellを分析することができますが、それは実際には効果がありません。設計の電流。それは意図や他の人的要因のように、技術的な問題ではありません。

Answer 5

タイプforall a. aのタイプは、Intが期待されているどこにでも使用でき、これは2つのタイプ間のサブタイプの関係を意味するとします。上記の他の答えは、この "多型よりも"相関がサブタイプではないことをあなたに説得しようとします。しかし、典型的なオブジェクト指向言語で見られるサブタイプの形式とは確かに異なるが、これは「多型よりも高い」相関がサブタイプの（異なる）形式とみなされることを意味しない。実際に、多型型システムのいくつかの形式化は、そのサブタイプ関係においてこの関係を正確にモデル化する。これは、例えばOderskyとLäuferの論文"Putting type annotations to work"のタイプシステムの場合です。