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

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