1 {-# LANGUAGE PolyKinds #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 -- | List utilities at the type-level.
4 module Language.Symantic.Helper.Data.Type.List where
6 import GHC.Exts (Constraint)
8 import Language.Symantic.Helper.Data.Type.Peano
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)
17 -- * Type family @(++)@
18 type family (++) xs ys where
20 (x ': xs) ++ ys = x ': xs ++ ys
23 -- * Type family 'Concat'
24 type family Concat (xs::[[k]]) :: [k] where
26 Concat (x ': xs) = x ++ Concat xs
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)
33 -- * Type family 'DeleteAll'
34 type family DeleteAll (x::k) (xs::[k]) :: [k] where
36 DeleteAll x (x ': xs) = DeleteAll x xs
37 DeleteAll x (y ': xs) = y ': DeleteAll x xs
39 -- * Type family 'Head'
40 type family Head (xs::[k]) :: k where
43 -- * Type family 'Tail'
44 type family Tail (xs::[k]) :: [k] where
47 -- * Type family 'Map'
48 type family Map (f::a -> b) (cs::[a]) :: [b] where
50 Map f (c ': cs) = f c ': Map f cs
52 -- * Type family 'Nub'
53 type family Nub (xs::[k]) :: [k] where
55 Nub (x ': xs) = x ': Nub (DeleteAll x xs)