haskell - 为什么我们不能定义封闭的数据族？

Question

以下所有工作:

{-# LANGUAGE TypeFamilies #-}

type family TF a
type instance TF Int = String
type instance TF Bool = Char

data family DF a
data instance DF Int = DFInt String
data instance DF Bool = DFBool Char

type family CTF a where
  CTF Int = String
  CTF Bool = Char
  CTF a = Double     -- Overlap OK!

...但这不是(从 GHC-8.2 开始):

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

wtmpf-file24527.hs:16:19: error: parse error on input ‘where’
   |
16 | data family CDF a where
   |                   ^^^^^

只是没有人费心去实现这一点，还是有什么特殊原因导致关闭数据家族没有意义？我有一个数据系列，我希望保持注入(inject)性，但也有机会制作一个不相交的包罗万象的实例。现在，我认为完成这项工作的唯一方法是

newtype CDF' a = CDF' (CTF a)

Answer 1

(这里我只是猜测，但我想分享这个想法。)

假设我们可以写

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

现在，这个定义引入的值构造函数的类型是什么？我很想说:

CDFInt   :: String -> CDF Int
CDFBool  :: Char   -> CDF Bool
CDFOther :: Double -> CDF a

...但最后一个感觉很不对劲，因为我们会得到

CDFOther @ Int :: Double -> CDF Int

这应该是不允许的，因为在一个封闭的数据系列中，人们会期望 CDF Int 的(非底部)值必须以 CDFInt 开头构造函数。

也许一个合适的类型是

CDFOther :: (a /~ Int, a /~ Bool) => Double -> CDF a

涉及“不平等约束”，但这将需要更多目前在 GHC 中可用的打字机器。我不知道类型检查/推理是否可以通过这种扩展来确定。

相比之下，类型族不涉及值构造函数，因此不会出现此问题。