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意义上的类型运算符这一事实.