symantic/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         -- xs  ++ '[] = xs
  21         (x ': xs) ++ ys = x ': xs ++ ys
  22 infixr 5 ++
  23
  24 -- * Type family 'Concat'
  25 type family Concat (xs::[[k]]) :: [k] where
  26         Concat '[] = '[]
  27         Concat (x ': xs) = x ++ Concat xs
  28
  29 -- * Type family 'Concat_Constraints'
  30 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
  31         Concat_Constraints '[] = ()
  32         Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
  33
  34 -- * Type family 'DeleteAll'
  35 type family DeleteAll (x::k) (xs::[k]) :: [k] where
  36         DeleteAll x '[] = '[]
  37         DeleteAll x (x ': xs) = DeleteAll x xs
  38         DeleteAll x (y ': xs) = y ': DeleteAll x xs
  39
  40 -- * Type family 'Head'
  41 type family Head (xs::[k]) :: k where
  42         Head (x ': _xs) = x
  43
  44 -- * Type family 'Tail'
  45 type family Tail (xs::[k]) :: [k] where
  46         Tail (_x ': xs) = xs
  47
  48 -- * Type family 'Map'
  49 type family Map (f::a -> b) (cs::[a]) :: [b] where
  50         Map f '[] = '[]
  51         Map f (c ': cs) = f c ': Map f cs
  52
  53 -- * Type family 'Nub'
  54 type family Nub (xs::[k]) :: [k] where
  55         Nub '[] = '[]
  56         Nub (x ': xs) = x ': Nub (DeleteAll x xs)