GHC的类型Famlies是系统F-omega的一个例子吗？ [英] Are GHC's Type Famlies An Example of System F-omega?

问题描述

我正在读Lambda-Cube，我对系统F-omega特别感兴趣，它允许使用类型操作符，即类型取决于类型。这听起来很像GHC的类型家庭。例如

 类型系列Foo a 
类型实例Foo Int = Int 
类型实例Foo Float =。 .. 
 ... 
  

实际类型取决于类型参数 A 。我是否认为类型族是类型运算符ala system 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 
  

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

然而，类型族并不是引入更高级别类型的另一种方法，也不是替代缺少的类型级lambda。至关重要的是，它们必须完全适用。所以你的例子，

  type family Foo a 
类型实例Foo Int = Int 
类型实例Foo Float = ... 
 .... 
  

不应被视为引入一些 p>

  Foo :: *  - > *  - 这不是发生的事情
  

因为 Foo 本身并不是一个有意义的类型表达式。每当 t :: * 。

$ b时，我们只有弱的规则 Foo t :: *
$ b

然而，类型族确实是超越F-Ω的独特类型级计算机制，因为它们在类型表达式之间引入了方程。系统F通过方程式扩展是GHC今天使用的系统Fc。 * 类型表达式之间的等式 s〜t 会导致从 s 到 t 。计算是通过从定义类型系列时给出的规则中推导方程来完成的。

此外，您可以为类型系列提供更高版本返回类型，如

 类型系列Hoo a 
类型实例Hoo Int =也许
类型实例Hoo Float = IO 
 ... 
  

使 Hoo t： ：* - > * 每当 t :: * ，但仍然不能让 Hoo 独立。 / p>

我们有时用来解决这个限制的诀窍是 newtype 包装：

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

确实给了我们

  Noo :: *  - > * 
  

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

  theNoo :: Noo Int  - > Int 
  

所以它有点笨重，但我们可以弥补类型系列没有的事实直接对应于F-omega意义上的类型运算符。

I'm reading up about the Lambda-Cube, and I'm particularly interested in System F-omega, which allows for "type operators" i.e. types depending on types. This sounds a lot like GHC's type families. For example

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

where the actual type depends on the type parameter a. Am I right in thinking that type families are an example of the type operators ala system F-omega? Or am I out in left field?

解决方案

System F-omega allows universal quantification, abstraction and application at higher kinds, so not only over types (at kind *), but also at kinds k1 -> k2, where k1 and k2 are themselves kinds generated from * and ->. Hence, the type level itself becomes a simply typed lambda-calculus.

Haskell delivers slightly less than F-omega, in that the type system allows quantification and application at higher kinds, but not abstraction. Quantification at higher kinds is how we have types like

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

with f :: * -> *. Correspondingly, variables like f can be instantiated with higher-kinded type expressions, such as Either String. The lack of abstraction makes it possible to solve unification problems in type expressions by the standard first-order techniques which underpin the Hindley-Milner type system.

However, type families are not really another means to introduce higher-kinded types, nor a replacement for the missing type-level lambda. Crucially, they must be fully applied. So your example,

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

should not be considered as introducing some

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

because Foo on its own is not a meaningful type expression. We have only the weaker rule that Foo t :: * whenever t :: *.

Type families do, however, act as a distinct type-level computation mechanism beyond F-omega, in that they introduce equations between type expressions. The extension of System F with equations is what gives us the "System Fc" which GHC uses today. Equations s ~ t between type expressions of kind * induce coercions transporting values from s to t. Computation is done by deducing equations from the rules you give when you define type families.

Moreover, you can give type families a higher-kinded return type, as in

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

so that Hoo t :: * -> * whenever t :: *, but still we cannot let Hoo stand alone.

The trick we sometimes use to get around this restriction is newtype wrapping:

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

which does indeed give us

Noo :: * -> *

but means that we have to apply the projection to make computation happen, so Noo Int and Int are provably distinct types, but

theNoo :: Noo Int -> Int

So it's a bit clunky, but we can kind of compensate for the fact that type families do not directly correspond to type operators in the F-omega sense.

这篇关于GHC的类型Famlies是系统F-omega的一个例子吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！