git.iko.soy/type-fun
on master help sign in
explicit exports
commitda54d388f50d5c2784b2360c4069c92d93172fbe authorAleksey Uimanov <s9gf4ult@gmail.com> dateThu 29 Oct 2015, 00:53 (11 years ago) parent846c0b0
5 files changed+30−5
compare with master
unifiedsplit
src/TypeFun/Constraint.hs+4−1 src/TypeFun/Data/Eq.hs+3−1 src/TypeFun/Data/List.hs+7 src/TypeFun/Data/Maybe.hs+8−2 src/TypeFun/Data/Peano.hs+8−1
src/TypeFun/Constraint.hs+4−1
@@ -1,7 +1,10 @@
1−module TypeFun.Constraint where
1+module TypeFun.Constraint
2+ ( AllSatisfy
3+ ) where
24
35import GHC.Exts
46
7+-- | Apply constraint for each element of list
58type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
69 AllSatisfy c '[] = ()
710 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
24
35type family Equal (a :: k) (b :: k) :: Bool where
46 Equal a a = 'True
src/TypeFun/Data/List.hs+7
@@ -9,6 +9,7 @@ module TypeFun.Data.List
99 , Drop
1010 , Take
1111 , Delete
12+ , Remove
1213 , (:++:)
1314 -- * Elements lookup
1415 , IndexOf
@@ -92,6 +93,12 @@ type family Delete (a :: k) (s :: [k]) :: [k] where
9293 Delete a (a ': as) = Delete a as
9394 Delete a (b ': as) = b ': (Delete a as)
9495
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+
95102type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
96103 '[] :++: b = b
97104 (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
28
39import GHC.Exts
410
@@ -8,7 +14,6 @@ type family MaybeCase (a :: Maybe k)
814 MaybeCase 'Nothing nothing just = nothing
915 MaybeCase ('Just k) nothing just = just k
1016
11−
1217type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
1318 NothingToConstr 'Nothing c = c
1419 NothingToConstr ('Just a) c = ()
@@ -17,6 +22,7 @@ type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
1722 JustToConstr 'Nothing c = ()
1823 JustToConstr ('Just a) c = c
1924
25+-- | Like 'catMaybes' for type lists
2026type family CatMaybes (l :: [Maybe k]) :: [k] where
2127 CatMaybes '[] = '[]
2228 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
29
310import Data.Typeable
411import GHC.Generics (Generic)