为什么我们不能定义封闭数据族？ [英] Why can't we define closed data families?

问题描述

所有以下工作：

  { - ＃LANGUAGE TypeFamilies＃ - } 
 
 type family TF a 
类型实例TF Int =字符串
类型实例TF Bool = Char 
 
数据族DF a 
数据实例DF Int = DFInt字符串
数据实例DF Bool = DFBool Char 
 
类型系列CTF a其中
 CTF Int =字符串
 CTF Bool = Char 
 CTF a = Double  - 重叠OK！ 
  

...但这不（如GHC-8.2）：

 数据族CDF a其中
 CDF Int = CDFInt字符串
 CDF Bool = CDFBool Char 
 CDF a = CDFOther Double 
  

  wtmpf-file24527.hs：16：19：< b>错误：解析输入错误'where'
 | 
 16 |数据族CDF a 其中 
 |  ^^^^^  
  

难道没有人会为了实施这还没有，还是有一个特殊的原因，为什么数据系列被关闭是没有意义的？我有一个数据族，我宁愿保持注入性，但也有机会做出一个不相交的catch-all实例。现在，我看到做这项工作的唯一方法是：
$ b $ pre $ newtype CDF'a = CDF'（CTF a）


解决方案

（这里我只是猜测，但我想分享一下）

假设我们可以写出

pre code数据族CDF a其中
CDF Int = CDFInt字符串
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）=>双 - > CDF a 
  

涉及不平等限制，但是这需要更多的打字机械，目前在GHC中可用。

相比之下，类型系列不包含值构造函数，所以这个类型检查/推理可以继续使用这种扩展来决定。问题不会出现在那里。

All of the following work:

{-# 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!

...but this doesn't (as of 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
   |                   ^^^^^

Is it just that nobody has bothered to implement this yet, or is there a particular reason why it wouldn't make sense for data families to be closed? I have a data family where I'd rather like to keep the injectivity, but also the opportunity to make a disjoint catch-all instance. Right now, the only way I see to make this work is

newtype CDF' a = CDF' (CTF a)

解决方案

(Here I am only guessing, but I want to share this thought.)

Assume we can write

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

Now, what is the type of the value constructors induced by this definition? I would be tempted to say:

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

... but the last one feels very wrong, since we would get

CDFOther @ Int :: Double -> CDF Int

which should be disallowed, since in a closed data family one would expect that a (non bottom) value of CDF Int must start with the CDFInt constructor.

Perhaps a proper type would be

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

involving "inequality constraints", but this would require more typing machinery that currently available in GHC. I have no idea if type checking / inference would remain decidable with such extension.

By contrast, type families involve no value constructors, so this issue does not arise there.

这篇关于为什么我们不能定义封闭数据族？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！