为什么我们不能定义封闭数据系列？

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
   |                   ^^^^^

难道只是没有人为实现这一点而烦恼,或者是否有一个特殊的原因导致数据家族被关闭是没有意义的？我有一个数据系列,我宁愿保持注入能力,也有机会制作一个不相交的全能实例.现在,我认为实现这项工作的唯一方法是

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中可用的打字机制.我不知道类型检查/推断是否仍然可以使用此类扩展进行判定.

相比之下,类型族不涉及价值构造者,因此这个问题不会出现.