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

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