]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/List.hs
Fix description.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / List.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE PolyKinds #-}
4 {-# LANGUAGE UndecidableInstances #-}
5 -- | List utilities at the type-level.
6 module Language.Symantic.Typing.List where
7
8 import GHC.Exts (Constraint)
9
10 import Language.Symantic.Typing.Peano
11
12 -- ** Type 'Index'
13 -- | Return the position of a type within a list of them.
14 -- This is useful to work around @OverlappingInstances@.
15 type family Index xs x where
16 Index (x ': xs) x = Zero
17 Index (not_x ': xs) x = Succ (Index xs x)
18
19 -- * Type family @(++)@
20 type family (++) xs ys where
21 '[] ++ ys = ys
22 -- xs ++ '[] = xs
23 (x ': xs) ++ ys = x ': xs ++ ys
24 infixr 5 ++
25
26 -- * Type family 'Concat'
27 type family Concat (xs::[[k]]) :: [k] where
28 Concat '[] = '[]
29 Concat (x ': xs) = x ++ Concat xs
30
31 -- * Type family 'Concat_Constraints'
32 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
33 Concat_Constraints '[] = ()
34 Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
35
36 -- * Type family 'DeleteAll'
37 type family DeleteAll (x::k) (xs::[k]) :: [k] where
38 DeleteAll x '[] = '[]
39 DeleteAll x (x ': xs) = DeleteAll x xs
40 DeleteAll x (y ': xs) = y ': DeleteAll x xs
41
42 -- * Type family 'Head'
43 type family Head (xs::[k]) :: k where
44 Head (x ': _xs) = x
45
46 -- * Type family 'Tail'
47 type family Tail (xs::[k]) :: [k] where
48 Tail (_x ': xs) = xs
49
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
57 -- * Type family 'Nub'
58 type family Nub (xs::[k]) :: [k] where
59 Nub '[] = '[]
60 Nub (x ': xs) = x ': Nub (DeleteAll x xs)
61
62 {-
63 -- * Type family 'L'
64 type family L (xs::[k]) :: Nat where
65 L '[] = 'Z
66 L (x ': xs) = 'S (L xs)
67
68 -- ** Class 'Inj_L'
69 class Inj_L (as::[k]) where
70 inj_L :: SNat (L as)
71 instance Inj_L '[] where
72 inj_L = SNatZ
73 instance Inj_L as => Inj_L (a ': as) where
74 inj_L = SNatS (inj_L @_ @as)
75 -}
76
77 -- * Type 'Len'
78 data Len (xs::[k]) where
79 LenZ :: Len '[]
80 LenS :: Len xs -> Len (x ': xs)
81
82 instance Show (Len vs) where
83 showsPrec _p = showsPrec 10 . intLen
84
85 addLen :: Len a -> Len b -> Len (a ++ b)
86 addLen LenZ b = b
87 addLen (LenS a) b = LenS $ addLen a b
88
89 shiftLen ::
90 forall t b a.
91 Len a ->
92 Len (a ++ b) ->
93 Len (a ++ t ': b)
94 shiftLen LenZ b = LenS b
95 shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
96
97 intLen :: Len xs -> Int
98 intLen = go 0
99 where
100 go :: Int -> Len xs -> Int
101 go i LenZ = i
102 go i (LenS l) = go (1 + i) l
103
104 -- ** Class 'Inj_Len'
105 class Inj_Len (vs::[k]) where
106 inj_Len :: Len vs
107 instance Inj_Len '[] where
108 inj_Len = LenZ
109 instance Inj_Len as => Inj_Len (a ': as) where
110 inj_Len = LenS inj_Len