git.iko.soy/type-fun
on master help sign in
rewrite with peano
640a287Aleksey Uimanov
example/Main.hs+2−1
compare with master
unifiedsplit
@@ -2,6 +2,7 @@ module Main where
2
2
3import Data.Proxy
3import Data.Proxy
4import TypeFun.Data.List
4import TypeFun.Data.List
5+import TypeFun.Data.Peano
5
6
6-- | This function has wider constraint __Int is inside l__
7-- | This function has wider constraint __Int is inside l__
7elemConstr :: (Elem Int l) => proxy l -> Int
8elemConstr :: (Elem Int l) => proxy l -> Int
@@ -19,7 +20,7 @@ prefixConstr p = sublistConstr p + 1
19
20
20-- | This function has narrower constraint __Int is inside of l and it
21-- | This function has narrower constraint __Int is inside of l and it
21-- is a first argument__ and uses inside more wide function
22-- is a first argument__ and uses inside more wide function
22−indexConstr :: (('Just 0) ~ (IndexOf Int l)) => proxy l -> Int
23+indexConstr :: (('Just 'Z) ~ (IndexOf Int l)) => proxy l -> Int
23indexConstr p = elemConstr p + 1
24indexConstr p = elemConstr p + 1
24
25
25uniqConstr :: (UniqElements l) => proxy l -> Int
26uniqConstr :: (UniqElements l) => proxy l -> Int
src/TypeFun/Data/List.hs+16−10
@@ -10,10 +10,11 @@ import GHC.TypeLits
10import TypeFun.Data.Eq
10import TypeFun.Data.Eq
11import TypeFun.Data.List.Errors
11import TypeFun.Data.List.Errors
12import TypeFun.Data.Maybe
12import TypeFun.Data.Maybe
13+import TypeFun.Data.Peano
13
14
14−type family Length (a :: [k]) :: Nat where
15+type family Length (a :: [k]) :: N where
15− Length '[] = 0
16+ Length '[] = 'Z
16− Length (a ': as) = 1 + (Length as)
17+ Length (a ': as) = 'S (Length as)
17
18
18-- | Generates unresolvable constraint if fists element is not
19-- | Generates unresolvable constraint if fists element is not
19-- contained inside of second
20-- contained inside of second
@@ -34,12 +35,17 @@ type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
34 NotSubList '[] bs = ()
35 NotSubList '[] bs = ()
35 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
36 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
36
37
37−type IndexOf a s = IndexOf' 0 a s
38+type IndexOf a s = IndexOf' Z a s
38
39
39−type family IndexOf' (acc :: Nat) (a :: k) (s :: [k]) :: Maybe Nat where
40+type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
40 IndexOf' acc a '[] = 'Nothing
41 IndexOf' acc a '[] = 'Nothing
41 IndexOf' acc a (a ': as) = 'Just acc
42 IndexOf' acc a (a ': as) = 'Just acc
42− IndexOf' acc a (b ': as) = IndexOf' (acc + 1) a as
43+ IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
44+
45+type family Index (idx :: N) (s :: [k]) :: Maybe k where
46+ Index idx '[] = 'Nothing
47+ Index Z (a ': as) = 'Just a
48+ Index (S idx) (a ': as) = Index idx as
43
49
44type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
50type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
45 (() :: Constraint)
51 (() :: Constraint)
@@ -56,13 +62,13 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
56 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
62 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
57 IsPrefixOfBool as bs = 'False
63 IsPrefixOfBool as bs = 'False
58
64
59−type ElementIsUniq a s = If (Equal 1 (Count a s))
65+type ElementIsUniq a s = If (Equal (S Z) (Count a s))
60 (() :: Constraint)
66 (() :: Constraint)
61 (ElementIsNotUniqInList a s)
67 (ElementIsNotUniqInList a s)
62
68
63−type family Count (a :: k) (s :: [k]) :: Nat where
69+type family Count (a :: k) (s :: [k]) :: N where
64− Count a '[] = 0
70+ Count a '[] = 'Z
65− Count a (a ': as) = 1 + (Count a as)
71+ Count a (a ': as) = 'S (Count a as)
66 Count a (b ': as) = Count a as
72 Count a (b ': as) = Count a as
67
73
68type UniqElements a = UniqElements' a a
74type UniqElements a = UniqElements' a a