"类型家族"与"数据家族",简而言之？

Question

我很困惑如何在data family和之间做出选择type family.TypeFamilies上的维基页面详细介绍了很多.偶尔它会非正式地将Haskell data family称为散文中的"类型家族",但当然也存在type family于Haskell中.

有一个简单的例子显示了两个版本的代码的显示位置,区别仅在于a data family或a type family是否被声明:

-- BAD: f is too ambiguous, due to non-injectivity
-- type family F a

-- OK
data family F a 

f :: F a -> F a
f = undefined

g :: F Int -> F Int
g x = f x

type与data此具有相同的含义,但type family版本没有类型检查,而data family版本是好的,因为data family"创造了新的类型,因此射"(说的wiki页面).

我从这一切中得到的结论是"尝试data family简单的案例,如果它不够强大,那么试试type family".这很好,但我想更好地理解它.是否有维恩图或决策树我可以遵循以区分何时使用哪个？

Answer 1

(将评论中的有用信息提升到答案中.)

独立与班级声明

声明类型系列和/或数据系列的两种语法不同的方法,在语义上等效:

独立:

type family Foo
data family Bar

或作为类型类的一部分:

class C where
   type Foo 
   data Bar 

两者都声明了一个类型族,但在类型类中,该family部分由class上下文隐含,因此GHC/Haskell缩写声明.

"新类型"与"类型同义词"/"类型别名"

data family F创建一个新类型,类似于data F = ...创建新类型的方式.

type family F不创建新类型,类似于type F = Bar Baz不创建新类型(它只是为现有类型创建别名/同义词).

非注入性的例子 type family

来自的一个例子(稍加修改)Data.MonoTraversable.Element:

import Data.ByteString as S
import Data.ByteString.Lazy as L

-- Declare a family of type synonyms, called `Element` 
-- `Element` has kind `* -> *`; it takes one parameter, which we call `container`
type family Element container

-- ByteString is a container for Word8, so...
-- The Element of a `S.ByteString` is a `Word8`
type instance Element S.ByteString = Word8 

-- and the Element of a `L.ByteString` is also `Word8`
type instance Element L.ByteString = Word8  

在类型族中,方程的右侧Word8命名现有类型; 左边的东西创造了新的同义词:Element S.ByteString和Element L.ByteString

拥有同义词意味着我们可以 Element Data.ByteString与Word8:

-- `w` is a Word8....
>let w = 0::Word8

-- ... and also an `Element L.ByteString`
>:t w :: Element L.ByteString
w :: Element L.ByteString :: Word8

-- ... and also an `Element S.ByteString`
>:t w :: Element S.ByteString
w :: Element S.ByteString :: Word8

-- but not an `Int`
>:t w :: Int
Couldn't match expected type `Int' with actual type `Word8'

这些类型的同义词是"非内射的"("单向"),因此是不可逆的.

-- As before, `Word8` matches `Element L.ByteString` ...
>(0::Word8)::(Element L.ByteString)

-- .. but  GHC can't infer which `a` is the `Element` of (`L.ByteString` or `S.ByteString` ?):

>(w)::(Element a)
Couldn't match expected type `Element a'
            with actual type `Element a0'
NB: `Element' is a type function, and may not be injective
The type variable `a0' is ambiguous

更糟糕的是,GHC甚至无法解决非模糊的案例!:

type instance Element Int = Bool
> True::(Element a)
> NB: `Element' is a type function, and may not be injective

注意使用"可能不是"!我认为GHC是保守的,并拒绝检查是否Element真的是单射的.(也许是因为程序员可以type instance在导入预编译模块之后添加另一个,添加歧义.

注入的例子 data family

相反:在数据族中,每个右侧都包含一个唯一的构造函数,因此定义是单射("可逆")方程.

-- Declare a list-like data family
data family XList a

-- Declare a list-like instance for Char
data instance XList Char = XCons Char (XList Char) | XNil

-- Declare a number-like instance for ()
data instance XList () = XListUnit Int

-- ERROR: "Multiple declarations of `XListUnit'"
data instance XList () = XListUnit Bool
-- (Note: GHCI accepts this; the new declaration just replaces the previous one.)

随着data family,看到右边的构造函数名(XCons或XListUnit)就足以让类型inferencer知道我们必须一起工作XList ()不是XList Char.由于构造函数名称是唯一的,因此这些定义是单射/可逆的.

如果type"just"声明了一个同义词,为什么它在语义上有用？

通常,type同义词只是缩写,但是type家庭同义词增加了力量:它们可以使简单类型(种类*)成为" * -> *应用于参数的类型的类型"的同义词:

type instance F A = B

使得B比赛F a.例如,这用于Data.MonoTraversable制作类型的简单类型Word8匹配函数Element a -> a (Element如上所述).

例如,(有点傻),假设我们的版本const仅适用于"相关"类型:

> class Const a where constE :: (Element a) -> a -> (Element a)
> instance Const S.ByteString where constE = const

> constE (0::Word8) undefined
ERROR: Couldn't match expected type `Word8' with actual type `Element a0'

-- By providing a match `a = S.ByteString`, `Word8` matches `(Element S.ByteString)`
> constE (0::Word8) (undefined::S.ByteString)  
0

-- impossible, since `Char` cannot match `Element a` under our current definitions.
> constF 'x' undefined 

Answer 2

我认为任何决策树或维恩图都不会存在,因为类型和数据系列的应用程序非常广泛.

一般来说,你已经突出了主要的设计差异,我同意你的意见,首先看看你是否可以逃脱data family.

对我来说,关键点在于a的每个实例data family都会创建一个新类型,这实际上会限制功率,因为​​你不能做通常最自然的事情并使现有类型成为实例.

例如,关于"索引类型"GMapKey的Haskell wiki页面上的示例非常适合数据系列:

class GMapKey k where
  data GMap k :: * -> *
  empty       :: GMap k v
  lookup      :: k -> GMap k v -> Maybe v
  insert      :: k -> v -> GMap k v -> GMap k v

映射的键类型k是数据族的参数,实际映射类型是数据族(GMap k)的结果.作为一个GMapKey实例的用户,你可能很高兴这个GMap k类型对你来说是抽象的,只是通过类型类中的泛型map操作来操作它.

相比之下,Collects同一维基页面上的示例恰恰相反:

class Collects ce where
  type Elem ce
  empty  :: ce
  insert :: Elem ce -> ce -> ce
  member :: Elem ce -> ce -> Bool
  toList :: ce -> [Elem ce]

参数类型是集合,结果类型是集合的元素.通常,用户将希望直接使用该类型上的常规操作来操作这些元素.例如,集合可能是IntSet,元素可能是Int.将Int其包裹在其他类型中会非常不方便.

注 - 这两个示例都带有类型类,因此不需要family关键字,因为在类类中声明类型意味着它必须是一个类.完全相同的考虑因素适用于独立家庭,但这只是抽象如何组织的问题.