git.iko.soy/type-fun
on master help sign in
explicit exports
da54d38Aleksey Uimanov
src/TypeFun/Constraint.hs+4−1
compare with master
unifiedsplit
@@ -1,7 +1,10 @@
1−module TypeFun.Constraint where
1+module TypeFun.Constraint
2+ ( AllSatisfy
3+ ) where
2
4
3import GHC.Exts
5import GHC.Exts
4
6
7+-- | Apply constraint for each element of list
5type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
8type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
6 AllSatisfy c '[] = ()
9 AllSatisfy c '[] = ()
7 AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
10 AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
src/TypeFun/Data/Eq.hs+3−1
@@ -1,4 +1,6 @@
1−module TypeFun.Data.Eq where
1+module TypeFun.Data.Eq
2+ ( Equal
3+ ) where
2
4
3type family Equal (a :: k) (b :: k) :: Bool where
5type family Equal (a :: k) (b :: k) :: Bool where
4 Equal a a = 'True
6 Equal a a = 'True
src/TypeFun/Data/List.hs+7
@@ -9,6 +9,7 @@ module TypeFun.Data.List
9 , Drop
9 , Drop
10 , Take
10 , Take
11 , Delete
11 , Delete
12+ , Remove
12 , (:++:)
13 , (:++:)
13 -- * Elements lookup
14 -- * Elements lookup
14 , IndexOf
15 , IndexOf
@@ -92,6 +93,12 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
92 Delete a (a ': as) = Delete a as
93 Delete a (a ': as) = Delete a as
93 Delete a (b ': as) = b ': (Delete a as)
94 Delete a (b ': as) = b ': (Delete a as)
94
95
96+-- | Remove index from the list
97+type family Remove (i :: N) (a :: [k]) :: [k] where
98+ Remove i '[] = '[]
99+ Remove 'Z (a ': as) = as
100+ Remove ('S i) (a ': as) = a ': (Remove i as)
101+
95type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
102type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
96 '[] :++: b = b
103 '[] :++: b = b
97 (a ': as) :++: b = a ': (as :++: b)
104 (a ': as) :++: b = a ': (as :++: b)
src/TypeFun/Data/Maybe.hs+8−2
@@ -1,4 +1,10 @@
1−module TypeFun.Data.Maybe where
1+module TypeFun.Data.Maybe
2+ ( MaybeCase
3+ , NothingToConstr
4+ , JustToConstr
5+ , CatMaybes
6+ , FromJust
7+ ) where
2
8
3import GHC.Exts
9import GHC.Exts
4
10
@@ -8,7 +14,6 @@ type family MaybeCase (a :: Maybe k)
8 MaybeCase 'Nothing nothing just = nothing
14 MaybeCase 'Nothing nothing just = nothing
9 MaybeCase ('Just k) nothing just = just k
15 MaybeCase ('Just k) nothing just = just k
10
16
11−
12type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
13 NothingToConstr 'Nothing c = c
18 NothingToConstr 'Nothing c = c
14 NothingToConstr ('Just a) c = ()
19 NothingToConstr ('Just a) c = ()
@@ -17,6 +22,7 @@ type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17 JustToConstr 'Nothing c = ()
22 JustToConstr 'Nothing c = ()
18 JustToConstr ('Just a) c = c
23 JustToConstr ('Just a) c = c
19
24
25+-- | Like 'catMaybes' for type lists
20type family CatMaybes (l :: [Maybe k]) :: [k] where
26type family CatMaybes (l :: [Maybe k]) :: [k] where
21 CatMaybes '[] = '[]
27 CatMaybes '[] = '[]
22 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
28 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
src/TypeFun/Data/Peano.hs+8−1
@@ -1,4 +1,11 @@
1−module TypeFun.Data.Peano where
1+module TypeFun.Data.Peano
2+ ( N(..)
3+ , ToNat
4+ , FromNat
5+ , (:+:)
6+ , (:-:)
7+ , (:*:)
8+ ) where
2
9
3import Data.Typeable
10import Data.Typeable
4import GHC.Generics (Generic)
11import GHC.Generics (Generic)