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
: 或在 Haskell 中表示为 ::。一般来说，该关系是“多对多”的，因此一个类型可以包含多个值，一个值也可以有多个类型。map :: (a -> b) -> [a] -> [b]
但也
map :: (Int -> Int) -> [Int] -> [Int].
t ⊑ s，则t比s更一般，意味着如果M : t，那么也必定M : s，而此类类型系统的类型规则正是允许推断出这一点。或者说s是t的一种特化。因此，在这种意义下，类型之间存在subtyping关系。forall a . a的一种特化。
对于Hindley-Milner类型系统，它允许类型推断并且是大多数函数式语言的基础，有主类型的概念：如果一个表达式M有一个（任意）类型，那么它也有其主类型，并且主类型是所有可能类型中最通用的类型。关键特征是HM类型推断算法总是找到最通用的类型。因此，可以将最通用、推断出的主类型专门化为M的任何有效类型。
M : t，那么也有 M : s”，但这似乎不太匹配。不过我可能错了。 - dfeuert更通用，则其取值范围更小（这可能是⊑的原因）。 因此，如果M：t且s是t的特化，则也有M：s。 - PetrT的表达式可以在任何期望T'的上下文中使用。但这并不是因为Haskell被设计支持子类型而出现的。相反，它是由于Haskell被设计为比对System F的忠实呈现更加用户友好而产生的偶然性。forall a. a，则其替代到Int上下文中就消失了。 a :: forall a. a是一个类型级函数，不能在期望Int的上下文中使用-您需要首先将其应用于Int以获得a Int :: Int，然后才能在Int上下文中实际使用它。 Haskell的语法隐藏了这一点，以追求用户友好性，但是在基础理论中确实存在。forall a. a的值可以用在需要Int的地方。 GHC的System F后代需要显式类型应用程序来将forall a. a值转换为Int。仅当类型推断首先添加了必要的类型应用/抽象时，该语言才会对Haskell进行建模。我想，未对类型推断进行建模既是优点也是缺点，这取决于应用程序。 - Dominique Devrieseforall a. a的值可以用在期望Int的任何地方，这意味着这两种类型之间存在一个子类型关系。其他回答试图让您相信这种“更多态性”的关系不是子类型。然而，虽然它肯定不同于典型面向对象语言中发现的子类型形式，但这并不意味着“更多态性”的关系不能被看作是一种（不同的）子类型形式。实际上，在一些多态类型系统的形式化模型中，正好将此关系建模为其子类型关系。例如，在Odersky和Läufer的论文“Putting type annotations to work”中的类型系统中就是这种情况。:: 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中类型以大写字母开头。这不是一个类型：它是一个类型变量！
我们使用多态是因为这样更容易。比如，组合是一个有用的想法：
(>>>) :: (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
id :: a -> a”，并且传入了一个Int，所以a = Int，因此id 6 :: Int。这不是子类型，而是类型统一！
a :: forall a. a
a = undefined
b :: Int
b = a
f :: (a -> Int) -> a
g :: (String -> b) -> b
h :: String -> Int
h = f g
f :: (a -> Int) -> a 表示 g 必须具有类型 a -> Int，这意味着 a -> Int 必须与 (String -> b) -> b 统一，因此 b 必须是 Int，这给出了 g 的具体类型 (String -> Int) -> Int，这意味着 a 是 String -> Int。
a -> Int 和 (String -> b) -> b 都不是对方的子类型，但它们可以作为 (String -> Int) -> Int 统一。forall a. a 和 Int 明显都是类型，对吧？ - Dominique Devriese
undefined不是 子类型化。这是一个错误。你为什么认为它是子类型化？ - AJFmempty :: forall m. Monoid m => m和let x = mempty :: [Int]。意思是，mempty是一个泛型函数，它接受一个符合 Monoid 接口的类型m并返回一个该类型的空值。在这个例子中，x被定义为[Int]类型的空值。 - rampion[Int]，但你不能写[forall a. a]（除非你启用了不太适用于类型推断的不确定性）。 - chilens库使用了全称多态和类型类编码出相当令人印象深刻的 "子类型层次结构"，所以无论这是否算作子类型，它都可以用于此目的。 - Ørjan Johansen