haskell - GHC 类型家族是系统 F-omega 的一个例子吗？

Question

我正在阅读有关 Lambda-Cube 的信息，并且我对 System F-omega 特别感兴趣，它允许“类型运算符”，即类型取决于类型。这听起来很像 GHC 的类型族。例如

type family Foo a
type instance Foo Int = Int
type instance Foo Float = ...
...

其中实际类型取决于类型参数 a .我认为类型族是类型运算符 ala 系统 F-omega 的一个例子是否正确？还是我在左外野？

Answer 1

系统 F-omega 允许在更高种类上进行通用量化、抽象和应用，因此不仅在类型上(在种类 * 上)，而且在种类 k1 -> k2 上, 其中 k1和 k2本身是从 * 生成的种类和 -> .因此，类型级别本身变成了简单类型的 lambda 演算。

Haskell 提供的比 F-omega 略少，因为类型系统允许在更高种类上进行量化和应用，但不允许抽象。更高种类的量化是我们如何拥有类似的类型

fmap :: forall f, s, t. Functor f => (s -> t) -> f s -> f t

与 f :: * -> * .相应地，像 f 这样的变量可以用更高级的类型表达式来实例化，例如 Either String .缺乏抽象使得通过支持 Hindley-Milner 类型系统的标准一阶技术解决类型表达式中的统一问题成为可能。

然而，类型族并不是真正引入高级类型的另一种方法，也不是缺失的类型级 lambda 的替代品。至关重要的是，它们必须得到充分应用。所以你的例子，

type family Foo a
type instance Foo Int = Int
type instance Foo Float = ...
....

不应被视为引入一些

Foo :: * -> * -- this is not what's happening

因为 Foo就其本身而言不是有意义的类型表达式。我们只有较弱的规则 Foo t :: *每当 t :: * .

然而，类型族确实充当了超越 F-omega 的独特类型级计算机制，因为它们在类型表达式之间引入了方程。系统 F 与方程的扩展是我们今天 GHC 使用的“系统 Fc”。方程 s ~ t类型表达式之间 *诱导从 s 传输值的强制至 t .计算是通过从定义类型族时给出的规则推导出方程来完成的。

此外，您可以为类型族赋予更高种类的返回类型，如

type family Hoo a
type instance Hoo Int = Maybe
type instance Hoo Float = IO
...

这样 Hoo t :: * -> *每当 t :: * ，但我们仍然不能让 Hoo独立。

我们有时用来绕过这个限制的技巧是 newtype包装:

newtype Noo i = TheNoo {theNoo :: Foo i}

这确实给了我们

Noo :: * -> *

但意味着我们必须应用投影来进行计算，所以 Noo Int和 Int可以证明是不同的类型，但是

theNoo :: Noo Int -> Int

所以它有点笨拙，但我们可以补偿一个事实，即类型族不直接对应于 F-omega 意义上的类型运算符。