78ab8fd · type-fun · git.iko.soy

git.iko.soy/type-fun

on master help sign in

hacking ..

78ab8fdAleksey Uimanov11 years ago

example/Main.hs+6−1

compare with master

unifiedsplit

@@ -22,12 +22,17 @@ prefixConstr p = sublistConstr p + 1

22indexConstr :: (('Just 0) ~ (IndexOf Int l)) => proxy l -> Int

23indexConstr p = elemConstr p + 1

25+uniqConstr :: (UniqElements l) => proxy l -> Int

26+uniqConstr _ = 1

27+

25main :: IO ()

28main :: IO ()

26main = do

29main = do

27 let

30 let

28 p2 = Proxy :: Proxy '[Int, Bool]

31 p2 = Proxy :: Proxy '[Int, Bool]

29− p3 = Proxy :: Proxy '[Int, Bool, String]

32+ p3 = Proxy :: Proxy '[Int, Bool, Int]

30 print $ indexConstr p2

33 print $ indexConstr p2

31 print $ sublistConstr p2

34 print $ sublistConstr p2

32 print $ prefixConstr p2

35 print $ prefixConstr p2

33 print $ prefixConstr p3

36 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 @@

1module TypeFun.Data.Eq where

3−class Equality a b

3+type family Equal (a :: k) (b :: k) :: Bool where

4−instance Equality a a

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

7import Data.Type.Bool

8import GHC.Exts

9import GHC.TypeLits

10+import TypeFun.Data.Eq

10import TypeFun.Data.List.Internal

11import TypeFun.Data.List.Internal

11import TypeFun.Data.Maybe

12import TypeFun.Data.Maybe

14+type family Length (a :: [k]) :: Nat where

15+ Length '[] = 0

16+ Length (a ': as) = 1 + (Length as)

17+

13-- | Generates unresolvable constraint if fists element is not

18-- | Generates unresolvable constraint if fists element is not

14-- contained inside of second

19-- contained inside of second

15type Elem a s = NothingToConstr (IndexOf a s)

20type Elem a s = NothingToConstr (IndexOf a s)

@@ -19,20 +24,15 @@ type Elem a s = NothingToConstr (IndexOf a s)

19type NotElem a s = JustToConstr (IndexOf a s)

24type NotElem a s = JustToConstr (IndexOf a s)

20 (ElementIsInList a s)

25 (ElementIsInList a s)

22−

23-- | Constanints that first argument is a sublist of second. Reduces

27-- | Constanints that first argument is a sublist of second. Reduces

24-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__

28-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__

25type family SubList (a :: [k]) (b :: [k]) :: Constraint where

29type family SubList (a :: [k]) (b :: [k]) :: Constraint where

26 SubList '[] bs = ()

30 SubList '[] bs = ()

27 SubList (a ': as) bs = (Elem a bs, SubList as bs)

31 SubList (a ': as) bs = (Elem a bs, SubList as bs)

29−-- type family SubListBool (a :: [k]) (b :: [k]) :: Bool where

33+type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where

30−-- SubListBool '[] bs = 'True

34+ NotSubList '[] bs = ()

31−-- SubListBool (a ': as) bs = (ElemBool a bs) && (SubListBool as bs)

35+ NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)

32−

33−

34−-- type family UniqElemsBool (a :: [k]) :: Bool where

35−-- UniqElemsBool

37type IndexOf a s = IndexOf' 0 a s

@@ -55,3 +55,18 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where

55 IsPrefixOfBool '[] b = 'True

56 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs

57 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

7class ListIsNotPrefixOf a b

9class ListIsPrefixOf a b

10+

11+class ElementIsNotUniqInList a s