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

15

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

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

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

但是也

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

在这样的类型系统中，（有时）可以定义类型上的关系，其含义是“比类型更通用”，即类型顺序。if t ⊑ sthent比 更一般s，意味着 if M : tthen 也是M : s，并且这种类型系统的类型规则允许准确​​推断。或者我们说这s是t. 所以从这个意义上说，类型上存在子类型关系。

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

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

于 2015-09-23T20:18:44.257 回答
11

对于这样的问题，我会退后一步说，从根本上说，作为 Haskell 设计基础的数学理论是没有子类型概念的 System F变体。

是的，可以查看 Haskell 的表面语法并注意到有些情况，例如您提出的情况，其中某种类型的表达式T可以在T'预期的任何上下文中使用。但这不会出现，因为 Haskell 旨在支持子类型。相反，它的出现是因为 Haskell 被设计为比 System F 的忠实呈现更用户友好这一事实。

在这种情况下，这与以下事实有关：类型级别的量词通常不会在 Haskell 代码中显式编写，而类型级别的 lambdas 和应用程序从来没有。如果你forall a. a从 System F 的角度来看这个类型，Int上下文的可替代性就消失了。 a :: forall a. a是一个类型级别的函数，不能在期望的上下文中使用Int——你需要首先将它应用Int到 get a Int :: Int，然后你才能在Int上下文中实际使用它。Haskell 的语法以用户友好的名义隐藏了这一点，但它存在于底层理论中。

所以简而言之，虽然你可以通过列出哪些表达式类型可以替换到哪些上下文类型来分析 Haskell，并证明存在某种加密子类型关系，但它只是没有成果，因为它产生的分析与设计的潮流背道而驰. 这与其说是技术问题，不如说是意图和其他人为因素。

于 2015-09-23T19:34:34.703 回答
5

你是正确的，类型的值forall a. a可以在任何需要的地方使用Int，这意味着两种类型之间的子类型关系。上面的其他答案试图说服你这种“多态多于”的关系不是子类型。然而，虽然它肯定不同于典型的面向对象语言中的子类型化形式，但这并不意味着“多态多于”关系不能被视为子类型化的（不同）形式。事实上，多态类型系统的一些形式化在它们的子类型关系中准确地模拟了这种关系。例如，在 Odersky 和 ​​Läufer 的论文“Putting type annotations to work”中的类型系统中就是这种情况。

于 2015-09-23T19:52:34.523 回答
3

我们:: a的意思是“任何类型”，但不是子类型。a 可以是Int, 或Bool, 或IO (Maybe Ordering), 但没有特别的。a不完全是类型，而是类型变量。

假设我们有一个这样的函数：

id x = x

编译器知道我们的参数没有特定的类型x。我们可以使用任何类型 for 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, so a = Int, so id 6 :: Int。

这不是子类型。可以使用类型类捕获子类型，但这是基本的多态性。

于 2015-09-23T19:14:12.013 回答
2

这不是子类型，而是类型统一！

a :: forall a. a
a = undefined

b :: Int
b = a

在b = a中，我们限制b和a是同一类型，因此编译器检查这是可能的。a具有 type forall a. 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必有，即给出具体的型，即是。bIntg(String -> Int) -> IntaString -> Int

两者都不a -> Int是(String -> b) -> b另一个的子类型，但它们可以统一为(String -> Int) -> Int.

于 2015-09-23T19:10:33.500 回答