Haskell中的封闭类型族和类型推导

Question

在 GHC-7.7（和7.8）中引入了封闭类型族：

封闭类型族的所有等式都定义在一个地方，无法扩展，而开放式类型族可以在多个模块中具有实例。封闭类型族的优点是它的等式按顺序尝试，类似于术语级函数定义。

我想问您，为什么以下代码无法编译？ GHC 应该能够推断出所有类型 - GetTheType 仅针对类型 X 定义，如果我们注释掉标记行，则代码可以编译。

这是 GHC 的 bug 还是封闭类型族尚未具备此类优化？

代码:

{-# LANGUAGE TypeFamilies #-}

data X = X 

type family GetTheType a where
    GetTheType X = X

class TC a where
    tc :: GetTheType a -> Int

instance TC X where
    tc X = 5 

main = do
    -- if we comment out the following line, the code compiles
    let x = tc X
    print "hello"

错误提示：

Couldn't match expected type ‛GetTheType a0’ with actual type ‛X’
The type variable ‛a0’ is ambiguous
In the first argument of ‛tc’, namely ‛X’
In the expression: tc X

- Wojciech Danilo

---

1. GHC 7.8.X 还没有发布，所以现在称其为 bug 有点早。
2. 你确定封闭类型族将成为默认选项而不需要任何标志或编译指示吗？

- Thomas M. DuBuisson

我在一周前刚问过Richard Eisenberg这个问题，可以在这里底部的评论中看到。我对这个潜力也非常兴奋。我已经在纸上勾画出我认为推理应该如何工作的机制，并且正在逐渐准备尝试进入GHC的黑客行列，但老实说，我不太有信心能在合理的时间内完成。 - jberryman

@ThomasM.DuBuisson：我们还不确定，但由于这个功能在GHC 7.7中可用，我们可以测试它并考虑一些行为是否为错误。我认为GHC 7.8应该很快就会发布。 - Wojciech Danilo

Answer 1

闭合类型家族并没有什么问题。问题在于并非所有类型函数都是单射的。

比如，你可以拥有这个闭合类型函数：

data X = X
data Y = Y

type family GetTheType a where
    GetTheType X = X
    GetTheType Y = X

您无法从结果类型X推断出参数类型。

数据族是可注入的，但不是封闭的：

{-# LANGUAGE TypeFamilies #-}

data X = X

data family GetTheType a

data instance GetTheType X = RX

class TC a where
    tc :: (GetTheType a) -> Int

instance TC X where
    tc RX = 5

main = do
    let x = tc RX
    print "hello"

- mgampkay

---

有了封闭类型族，GHC可以检查类型函数是否是单射的。我认为这也是拥有它们的原因之一。我不知道是否有人正在研究这个问题。 - Sjoerd Visscher

这个功能在论文的未来工作部分被提及。它可能会在未来实现 :) - mgampkay

@mgampkay：在哪篇论文中？你能发个链接吗？ - Wojciech Danilo

@SjoerdVisscher 闭合的类型族与重叠方程式 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf - mgampkay

哦，这解释了那个晦涩的 GHC 错误信息，大概是“类型函数 Foo 可能不是单射的”。当我看到那个时，我想，“你说的‘可能’是什么意思？它是还是不是？” - misterbee