我正在阅读有关 Lambda-Cube 的信息,并且我对 System F-omega 特别感兴趣,它允许“类型运算符”,即类型取决于类型。这听起来很像 GHC 的类型族。例如
type family Foo a
type instance Foo Int = Int
type instance Foo Float = ...
...
其中实际类型取决于类型参数
a
.我认为类型族是类型运算符 ala 系统 F-omega 的一个例子是否正确?还是我在左外野?
最佳答案
系统 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 意义上的类型运算符。
关于haskell - GHC 类型家族是系统 F-omega 的一个例子吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/21219773/