Language/Symantic/Lib/Data/Type/List.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 -- | List utilities at the type-level.
   3 module Language.Symantic.Lib.Data.Type.List where
   4
   5 import GHC.Exts (Constraint)
   6
   7 import Language.Symantic.Lib.Data.Type.Peano
   8
   9 -- ** Type 'Index'
  10 -- | Return the position of a type within a list of them.
  11 -- This is useful to work around @OverlappingInstances@.
  12 type family Index xs x where
  13         Index (x     ': xs) x = Zero
  14         Index (not_x ': xs) x = Succ (Index xs x)
  15
  16 -- * Type family @(++)@
  17 type family (++) xs ys where
  18         '[] ++ ys = ys
  19         (x ': xs) ++ ys = x ': xs ++ ys
  20 infixr 5 ++
  21
  22 -- * Type family 'Concat'
  23 type family Concat (xs::[[k]]) :: [k] where
  24         Concat '[] = '[]
  25         Concat (x ': xs) = x ++ Concat xs
  26
  27 -- * Type family 'Concat_Constraints'
  28 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
  29         Concat_Constraints '[] = ()
  30         Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
  31
  32 -- * Type family 'DeleteAll'
  33 type family DeleteAll (x::k) (xs::[k]) :: [k] where
  34         DeleteAll x '[] = '[]
  35         DeleteAll x (x ': xs) = DeleteAll x xs
  36         DeleteAll x (y ': xs) = y ': DeleteAll x xs
  37
  38 -- * Type family 'Head'
  39 type family Head (xs::[k]) :: k where
  40         Head (x ': _xs) = x
  41
  42 -- * Type family 'Tail'
  43 type family Tail (xs::[k]) :: [k] where
  44         Tail (_x ': xs) = xs
  45
  46 -- * Type family 'Map'
  47 type family Map (f::a -> b) (cs::[a]) :: [b] where
  48         Map f '[] = '[]
  49         Map f (c ': cs) = f c ': Map f cs
  50
  51 -- * Type family 'Nub'
  52 type family Nub (xs::[k]) :: [k] where
  53         Nub '[] = '[]
  54         Nub (x ': xs) = x ': Nub (DeleteAll x xs)