为什么是forall a.一个不被认为是Int的子类型,而我可以使用类型forall a的表达式.预计会有任何一种类型的Int？

Question

考虑以下一对函数定义,它们传递类型检查器:

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

Answer 1

在类型化的lambda演算中,我们有类型关系,通常表示为:或在Haskell中::.通常,关系是"多对多",因此类型可以包含多个值,并且值可以有多种类型.

特别是在多态类型系统中,值可以具有多种类型.例如

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

但是也

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

在这种类型系统中,(有时)可以定义关于类型的关系,其含义是"比通用类型更多",类型顺序.如果t ? s那么t比一般更通用s,意味着如果M : t那时也是如此M : s,并且这种类型系统的输入规则允许准确​​地推断出那个.或者我们说这s是一个专业化t.所以在这个意义上,类型有一个子类型关系.

但是,当我们谈论面向对象语言中的子类型时,我们通常意味着名义上的子类型,也就是说,我们声明哪些类型是什么的子类型,就像我们定义类继承时一样.在Haskell中,它是类型的属性,独立于任何声明.例如,任何类型都是特化forall a . a.

对于允许类型推断并且是大多数函数式语言的基础的Hindley-Milner类型系统,存在主体类型的概念:如果表达式M具有(任何)类型,那么它也具有其主要类型,并且主体类型是所有可能类型中最常见的类型M.关键特征是HM类型推断算法总是找到最通用的类​​型.因此,最常见的推断主体类型可以专用于任何有效类型M.

Answer 2

有了这样的问题,我会退一步说,从根本上说,构成Haskell设计基础的数学理论是没有子类型概念的System F变体.

是的,可以查看Haskell的表面语法,并注意到有些情况就像你提出的那样,某些类型的表达式T可以在任何T'预期的上下文中使用.但这并不会出现,因为Haskell旨在支持子类型.相反,它出现的事实是,Haskell被设计为比系统F的忠实渲染更加用户友好.

在这种情况下,它与以下事实有关:类型级量词通常不是在Haskell代码中显式编写的,而类型级lambda和应用程序从不是.如果forall a. a从系统F角度查看类型,对Int上下文的可替代性就会消失. a :: forall a. a是一个类型级别的函数,不能在期望的上下文中使用Int- 您需要先将其应用于Intget a Int :: Int,然后才能在Int上下文中实际使用它.Haskell的语法以用户友好的名义隐藏,但它存在于基础理论中.

简而言之,虽然您可以通过将哪些表达式类型替换为哪些上下文类型并且证明存在某种加密子类型关系来分析Haskell,但它只是没有成效,因为它产生的分析与设计的当前流动相关.它不是技术问题,而是意图和其他人为因素.

Answer 3

你是正确的,类型的值forall a. a可以在任何Int预期的地方使用,这意味着两种类型之间的子类型关系.上面的其他答案试图说服你,这种"多态多于"的关系不是子类型.然而,虽然它与典型的面向对象语言中的子类型形式肯定不同,但这并不意味着"更多 - 多态"的关系不能被视为(不同的)子类型形式.实际上,多态类型系统的一些形式化在它们的子类型关系中精确地建模了这种关系.例如,在Odersky和Läufer的论文"将类型注释投入工作"中的类型系统就是这种情况.