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 Data.Bool (Bool(..))
   9 import Language.Symantic.Helper.Data.Type.Peano
  10
  11 -- ** Type 'Index'
  12 -- | Return the position of a type within a list of them.
  13 -- This is useful to work around @OverlappingInstances@.
  14 type family Index xs x where
  15         Index (x     ': xs) x = Zero
  16         Index (not_x ': xs) x = Succ (Index xs x)
  17
  18 -- * Type family @(++)@
  19 type family (++) xs ys where
  20         '[] ++ ys  = ys
  21         -- xs  ++ '[] = xs
  22         (x ': xs) ++ ys = x ': xs ++ ys
  23 infixr 5 ++
  24
  25 -- * Type family 'Concat'
  26 type family Concat (xs::[[k]]) :: [k] where
  27         Concat '[] = '[]
  28         Concat (x ': xs) = x ++ Concat xs
  29
  30 -- * Type family 'Concat_Constraints'
  31 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
  32         Concat_Constraints '[] = ()
  33         Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
  34
  35 -- * Type family 'DeleteAll'
  36 type family DeleteAll (x::k) (xs::[k]) :: [k] where
  37         DeleteAll x '[] = '[]
  38         DeleteAll x (x ': xs) = DeleteAll x xs
  39         DeleteAll x (y ': xs) = y ': DeleteAll x xs
  40
  41 -- * Type family 'Head'
  42 type family Head (xs::[k]) :: k where
  43         Head (x ': _xs) = x
  44
  45 -- * Type family 'Tail'
  46 type family Tail (xs::[k]) :: [k] where
  47         Tail (_x ': xs) = xs
  48
  49 -- * Type family 'Map'
  50 type family Map (f::a -> b) (cs::[a]) :: [b] where
  51         Map f '[] = '[]
  52         Map f (c ': cs) = f c ': Map f cs
  53
  54 -- * Type family 'Nub'
  55 type family Nub (xs::[k]) :: [k] where
  56         Nub '[] = '[]
  57         Nub (x ': xs) = x ': Nub (DeleteAll x xs)
  58
  59 -- * Type family 'Exists'
  60 type family Exists (x::k) (xs::[k]) :: Bool where
  61         Exists x '[] = 'False
  62         Exists x (x ': xs) = 'True
  63         Exists x (y ': xs) = Exists x xs
  64
  65 -- * Type family 'If'
  66 type family If (b::Bool) (ok::k) (ko::k) :: k where
  67         If 'True  ok ko = ok
  68         If 'False ok ko = ko