haskell - 为什么是forall a。 a 不被视为 Int 的子类型，而我可以使用 forall a 类型的表达式。任何地方都需要 Int 类型？

Question

考虑以下通过类型检查器的函数定义对:

a :: forall a. a
a = undefined

b :: Int
b = a

IE。 forall a. a 类型的表达式可用于 Int 类型之一是期待。在我看来，这很像子类型，但据称 Haskell 的类型系统缺少子类型。这些形式的可替代性有何不同？

此问题并非特定于 forall a. a .其他示例包括:

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

idInt :: Int -> Int
idInt = id

Answer 1

在类型化 lambda 演算中，我们有类型关系，通常表示为 :或在 Haskell 中为 :: .一般来说，关系是“多对多”，所以一个类型可以包含多个值，一个值也可以有多个类型。

特别是在多态类型系统中，一个值可以有多种类型。例如

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有一个(any)类型，那么它也有它的主体类型，主体类型是 M的所有可能类型中最通用的类​​型.关键特征是 HM 类型推理算法总是找到最一般的类型。因此，最一般的推断主体类型可以专门化为 M 的任何有效类型。 .