git.iko.soy/type-fun
on master help sign in
rewrite with peano
commit640a2874b8abd241f79e23a10f6643805cfe9e9e authorAleksey Uimanov <s9gf4ult@gmail.com> dateSat 24 Oct 2015, 22:14 (11 years ago) parent8c32be3
2 files changed+18−11
compare with master
unifiedsplit
example/Main.hs+2−1 src/TypeFun/Data/List.hs+16−10
example/Main.hs+2−1
@@ -2,6 +2,7 @@ module Main where
22
33import Data.Proxy
44import TypeFun.Data.List
5+import TypeFun.Data.Peano
56
67-- | This function has wider constraint __Int is inside l__
78elemConstr :: (Elem Int l) => proxy l -> Int
@@ -19,7 +20,7 @@ prefixConstr p = sublistConstr p + 1
1920
2021-- | This function has narrower constraint __Int is inside of l and it
2122-- 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
2324indexConstr p = elemConstr p + 1
2425
2526uniqConstr :: (UniqElements l) => proxy l -> Int
src/TypeFun/Data/List.hs+16−10
@@ -10,10 +10,11 @@ import GHC.TypeLits
1010import TypeFun.Data.Eq
1111import TypeFun.Data.List.Errors
1212import TypeFun.Data.Maybe
13+import TypeFun.Data.Peano
1314
14−type family Length (a :: [k]) :: Nat where
15− Length '[] = 0
16− Length (a ': as) = 1 + (Length as)
15+type family Length (a :: [k]) :: N where
16+ Length '[] = 'Z
17+ Length (a ': as) = 'S (Length as)
1718
1819-- | Generates unresolvable constraint if fists element is not
1920-- contained inside of second
@@ -34,12 +35,17 @@ type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
3435 NotSubList '[] bs = ()
3536 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
3637
37−type IndexOf a s = IndexOf' 0 a s
38+type IndexOf a s = IndexOf' Z a s
3839
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
4041 IndexOf' acc a '[] = 'Nothing
4142 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
4349
4450type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
4551 (() :: Constraint)
@@ -56,13 +62,13 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
5662 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
5763 IsPrefixOfBool as bs = 'False
5864
59−type ElementIsUniq a s = If (Equal 1 (Count a s))
65+type ElementIsUniq a s = If (Equal (S Z) (Count a s))
6066 (() :: Constraint)
6167 (ElementIsNotUniqInList a s)
6268
63−type family Count (a :: k) (s :: [k]) :: Nat where
64− Count a '[] = 0
65− Count a (a ': as) = 1 + (Count a as)
69+type family Count (a :: k) (s :: [k]) :: N where
70+ Count a '[] = 'Z
71+ Count a (a ': as) = 'S (Count a as)
6672 Count a (b ': as) = Count a as
6773
6874type UniqElements a = UniqElements' a a