git.iko.soy/type-fun
on master help sign in
it works
23bb88cAleksey Uimanov
example/Main.hsnew file+33
compare with master
unifiedsplit
@@ -0,0 +1,33 @@
1+module Main where
2+
3+import Data.Proxy
4+import TypeFun.Data.List
5+
6+-- | This function has wider constraint __Int is inside l__
7+elemConstr :: (Elem Int l) => proxy l -> Int
8+elemConstr p = 1
9+
10+-- | This function has narrower constraint than 'elemConstr'
11+-- __Int and Bool are contained in l__
12+sublistConstr :: (SubList '[Int, Bool] l) => proxy l -> Int
13+sublistConstr p = elemConstr p + 1
14+
15+-- | This function has narrower constraint than 'sublistConstr' (Order
16+-- of elements matters)
17+prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
18+prefixConstr p = sublistConstr p + 1
19+
20+-- | This function has narrower constraint __Int is inside of l and it
21+-- is a first argument__ and uses inside more wide function
22+indexConstr :: (('Just 0) ~ (IndexOf Int l)) => proxy l -> Int
23+indexConstr p = elemConstr p + 1
24+
25+main :: IO ()
26+main = do
27+ let
28+ p2 = Proxy :: Proxy '[Int, Bool]
29+ p3 = Proxy :: Proxy '[Int, Bool, String]
30+ print $ indexConstr p2
31+ print $ sublistConstr p2
32+ print $ prefixConstr p2
33+ print $ prefixConstr p3
src/TypeFun/Data/Eq.hsnew file+4
@@ -0,0 +1,4 @@
1+module TypeFun.Data.Eq where
2+
3+class Equality a b
4+instance Equality a a
src/TypeFun/Data/List.hsnew file+57
@@ -0,0 +1,57 @@
1+-- | Collection of type families on type lists. This module differs
2+-- from __Data.Singletons.Prelude.List__ because it polykinded and
3+-- works with __[*]__ as well
4+
5+module TypeFun.Data.List where
6+
7+import Data.Type.Bool
8+import GHC.Exts
9+import GHC.TypeLits
10+import TypeFun.Data.List.Internal
11+import TypeFun.Data.Maybe
12+
13+-- | Generates unresolvable constraint if fists element is not
14+-- contained inside of second
15+type Elem a s = NothingToConstr (IndexOf a s)
16+ (ElementNotFoundInList a s)
17+
18+-- | Reverse of 'Elem'
19+type NotElem a s = JustToConstr (IndexOf a s)
20+ (ElementIsInList a s)
21+
22+
23+-- | Constanints that first argument is a sublist of second. Reduces
24+-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
25+type family SubList (a :: [k]) (b :: [k]) :: Constraint where
26+ SubList '[] bs = ()
27+ SubList (a ': as) bs = (Elem a bs, SubList as bs)
28+
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
36+
37+type IndexOf a s = IndexOf' 0 a s
38+
39+type family IndexOf' (acc :: Nat) (a :: k) (s :: [k]) :: Maybe Nat where
40+ IndexOf' acc a '[] = 'Nothing
41+ IndexOf' acc a (a ': as) = 'Just acc
42+ IndexOf' acc a (b ': as) = IndexOf' (acc + 1) a as
43+
44+type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
45+ (() :: Constraint)
46+ (ListIsNotPrefixOf a b)
47+ , SubList a b )
48+
49+type IsNotPrefixOf a b = If (IsPrefixOfBool a b)
50+ (ListIsPrefixOf a b)
51+ (() :: Constraint)
52+
53+-- | First argument is prefix of second
54+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
src/TypeFun/Data/List/Internal.hsnew file+9
@@ -0,0 +1,9 @@
1+module TypeFun.Data.List.Internal where
2+
3+class ElementNotFoundInList a s
4+
5+class ElementIsInList a s
6+
7+class ListIsNotPrefixOf a b
8+
9+class ListIsPrefixOf a b
src/TypeFun/Data/Maybe.hsnew file+18
@@ -0,0 +1,18 @@
1+module TypeFun.Data.Maybe where
2+
3+import GHC.Exts
4+
5+type family MaybeCase (a :: Maybe k)
6+ (nothing :: r)
7+ (just :: k -> r) :: r where
8+ MaybeCase 'Nothing nothing just = nothing
9+ MaybeCase ('Just k) nothing just = just k
10+
11+
12+type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
13+ NothingToConstr 'Nothing c = c
14+ NothingToConstr ('Just a) c = ()
15+
16+type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17+ JustToConstr 'Nothing c = ()
18+ JustToConstr ('Just a) c = c
type-fun.cabal+34−10
@@ -1,24 +1,48 @@
1−-- Initial type-fun.cabal generated by cabal init. For further
1+-- Initial type-fun.cabal generated by cabal init. For further
2-- documentation, see http://haskell.org/cabal/users-guide/
2-- documentation, see http://haskell.org/cabal/users-guide/
3
3
4name: type-fun
4name: type-fun
5version: 0.0.1
5version: 0.0.1
6−-- synopsis:
6+synopsis: Collection of widely reimplemented type families
7−-- description:
7+-- description:
8license: BSD3
8license: BSD3
9license-file: LICENSE
9license-file: LICENSE
10author: Aleksey Uimanov
10author: Aleksey Uimanov
11maintainer: s9gf4ult@gmail.com
11maintainer: s9gf4ult@gmail.com
12−-- copyright:
12+-- copyright:
13category: Dependent Types
13category: Dependent Types
14build-type: Simple
14build-type: Simple
15−-- extra-source-files:
15+-- extra-source-files:
16cabal-version: >=1.10
16cabal-version: >=1.10
17
17
18library
18library
19− -- exposed-modules:
19+ default-language: Haskell2010
20− -- other-modules:
21− -- other-extensions:
22− build-depends: base >=4.8 && <4.9
23 hs-source-dirs: src
20 hs-source-dirs: src
21+ default-extensions: ConstraintKinds
22+ , DataKinds
23+ , FlexibleInstances
24+ , MultiParamTypeClasses
25+ , PolyKinds
26+ , TypeFamilies
27+ , TypeOperators
28+ , UndecidableInstances
29+
30+ exposed-modules: TypeFun.Data.Eq
31+ , TypeFun.Data.List
32+ , TypeFun.Data.Maybe
33+
34+ build-depends: base >=4.7 && <4.9
35+
36+
37+test-suite example
38+ type: exitcode-stdio-1.0
24− default-language: Haskell2010
39+ default-language: Haskell2010
40+ hs-source-dirs: example
41+ main-is: Main.hs
42+ default-extensions: DataKinds
43+ , GADTs
44+ , TemplateHaskell
45+ , TypeFamilies
46+ , UndecidableInstances
47+ build-depends: base
48+ , type-fun