git.iko.soy/type-fun
on master help sign in
hacking ..
commit78ab8fde60b42ec6cea6ba3555c7b34e2e25e296 authorAleksey Uimanov <s9gf4ult@gmail.com> dateSat 24 Oct 2015, 02:19 (11 years ago) parent23bb88c
4 files changed+34−11
compare with master
unifiedsplit
example/Main.hs+6−1 src/TypeFun/Data/Eq.hs+3−2 src/TypeFun/Data/List.hs+23−8 src/TypeFun/Data/List/Internal.hs+2
example/Main.hs+6−1
@@ -22,12 +22,17 @@ prefixConstr p = sublistConstr p + 1
2222indexConstr :: (('Just 0) ~ (IndexOf Int l)) => proxy l -> Int
2323indexConstr p = elemConstr p + 1
2424
25+uniqConstr :: (UniqElements l) => proxy l -> Int
26+uniqConstr _ = 1
27+
2528main :: IO ()
2629main = do
2730 let
2831 p2 = Proxy :: Proxy '[Int, Bool]
29− p3 = Proxy :: Proxy '[Int, Bool, String]
32+ p3 = Proxy :: Proxy '[Int, Bool, Int]
3033 print $ indexConstr p2
3134 print $ sublistConstr p2
3235 print $ prefixConstr p2
3336 print $ prefixConstr p3
37+ print $ uniqConstr p2
38+ -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]
src/TypeFun/Data/Eq.hs+3−2
@@ -1,4 +1,5 @@
11module TypeFun.Data.Eq where
22
3−class Equality a b
4−instance Equality a a
3+type family Equal (a :: k) (b :: k) :: Bool where
4+ Equal a a = 'True
5+ Equal a b = 'False
src/TypeFun/Data/List.hs+23−8
@@ -7,9 +7,14 @@ module TypeFun.Data.List where
77import Data.Type.Bool
88import GHC.Exts
99import GHC.TypeLits
10+import TypeFun.Data.Eq
1011import TypeFun.Data.List.Internal
1112import TypeFun.Data.Maybe
1213
14+type family Length (a :: [k]) :: Nat where
15+ Length '[] = 0
16+ Length (a ': as) = 1 + (Length as)
17+
1318-- | Generates unresolvable constraint if fists element is not
1419-- contained inside of second
1520type Elem a s = NothingToConstr (IndexOf a s)
@@ -19,20 +24,15 @@ type Elem a s = NothingToConstr (IndexOf a s)
1924type NotElem a s = JustToConstr (IndexOf a s)
2025 (ElementIsInList a s)
2126
22−
2327-- | Constanints that first argument is a sublist of second. Reduces
2428-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
2529type family SubList (a :: [k]) (b :: [k]) :: Constraint where
2630 SubList '[] bs = ()
2731 SubList (a ': as) bs = (Elem a bs, SubList as bs)
2832
29−-- type family SubListBool (a :: [k]) (b :: [k]) :: Bool where
30−-- SubListBool '[] bs = 'True
31−-- SubListBool (a ': as) bs = (ElemBool a bs) && (SubListBool as bs)
32−
33−
34−-- type family UniqElemsBool (a :: [k]) :: Bool where
35−-- UniqElemsBool
33+type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
34+ NotSubList '[] bs = ()
35+ NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
3636
3737type IndexOf a s = IndexOf' 0 a s
3838
@@ -55,3 +55,18 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
5555 IsPrefixOfBool '[] b = 'True
5656 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
5757 IsPrefixOfBool as bs = 'False
58+
59+type ElementIsUniq a s = If (Equal 1 (Count a s))
60+ (() :: Constraint)
61+ (ElementIsNotUniqInList a s)
62+
63+type family Count (a :: k) (s :: [k]) :: Nat where
64+ Count a '[] = 0
65+ Count a (a ': as) = 1 + (Count a as)
66+ Count a (b ': as) = Count a as
67+
68+type UniqElements a = UniqElements' a a
69+
70+type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
71+ UniqElements' '[] self = ()
72+ UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
src/TypeFun/Data/List/Internal.hs+2
@@ -7,3 +7,5 @@ class ElementIsInList a s
77class ListIsNotPrefixOf a b
88
99class ListIsPrefixOf a b
10+
11+class ElementIsNotUniqInList a s