这是一个例子:
{-# Language TypeFamilies, DataKinds, KindSignatures, GADTs, UndecidableInstances #-}
data Nat = Z | S Nat
type family Plus (x :: Nat) (y :: Nat) :: Nat where
Plus 'Z y = y
Plus ('S x) y = 'S (Plus x y)
data Vec :: Nat -> * -> * where
Nil :: Vec 'Z a
Cons :: a -> Vec n a -> Vec ('S n) a
append :: Vec m a -> Vec n a -> Vec (Plus m n) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
请注意,类型系列的许多/最有趣的应用程序需要UndecidableInstances
。您不应该害怕这个扩展。
另一种有用的类型族是与类相关联的类型族。举一个非常人为的例子,
class Box b where
type Elem b :: *
elem :: b -> Elem b
一个实例Box
是一种可以从中拉出某些东西的类型。例如,
instance Box (Identity x) where
type Elem (Identity x) = x
elem = runIdentity
instance Box Char where
type Elem Char = String
elem c = [c]
Now elem (Identity 3) = 3
and elem 'x' = "x"
.
您还可以使用类型族来创建奇怪的 skolem 变量。这最好在尚未发布的 GHC 8.0.1 中完成,它看起来像
type family Any :: k where {}
Any
是一种奇特的类型。它无人居住,它不能(具体来说)是类的实例,而且它是多类的。事实证明,这对于某些目的确实很有用。这种特殊类型被宣传为安全目标unsafeCoerce
, but Data.Constraint.Forall
使用相似类型的族来达到更有趣的目的。