git.iko.soy/type-fun
on master help sign in
swap
a90d4b726 ahead, 0 behind
.gitignore+3
since splitsnapshots
unifiedsplit
@@ -1,2 +1,5 @@
1dist
1dist
2TAGS
2TAGS
3+.cabal-sandbox
4+cabal.sandbox.config
5+.stack-work
CHANGELOG.mdnew file+23
@@ -0,0 +1,23 @@
1+# TODO
2+* Add doctests
3+* Add TyFun from singletons (or just depend from)?
4+
5+# CHANGELOG
6+
7+## 0.1.2
8+### Added KnownPeano
9+
10+## 0.1.1
11+### Fixed
12+* Compilable with ghc-8.0.1
13+
14+## 0.1.0
15+### Added
16+* Type family `Substract` to remove elements of one list from another
17+* Unsafe helper functions to relax constraints in some safe points. But we use
18+ `unsafeCoerce` so this functions are potentially just break constants
19+### Changed
20+* Compilable under ghc-7.8
21+
22+## 0.0.1
23+First version
example/Main.hs+5−3
@@ -18,9 +18,10 @@ sublistConstr p = elemConstr p + 1
18prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
18prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
19prefixConstr p = sublistConstr p + 1
19prefixConstr p = sublistConstr p + 1
20
20
21−-- | This function has narrower constraint __Int is inside of l and it
21+-- | This function has narrower constraint
22+-- __Int is inside of l and it is a first argument__
22−-- is a first argument__ and uses inside more wide function
23+-- and uses inside more wide function
23−indexConstr :: (('Just 'Z) ~ (IndexOf Int l)) => proxy l -> Int
24+indexConstr :: (('Just 'Z) ~ (IndexOfMay Int l)) => proxy l -> Int
24indexConstr p = elemConstr p + 1
25indexConstr p = elemConstr p + 1
25
26
26uniqConstr :: (UniqElements l) => proxy l -> Int
27uniqConstr :: (UniqElements l) => proxy l -> Int
@@ -36,4 +37,5 @@ main = do
36 print $ prefixConstr p2
37 print $ prefixConstr p2
37 print $ prefixConstr p3
38 print $ prefixConstr p3
38 print $ uniqConstr p2
39 print $ uniqConstr p2
40+ print $ peanoVal (Proxy :: Proxy (FromNat 100))
39 -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]
41 -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]
src/TypeFun/Constraint.hsnew file+10
@@ -0,0 +1,10 @@
1+module TypeFun.Constraint
2+ ( AllSatisfy
3+ ) where
4+
5+import GHC.Exts
6+
7+-- | Apply constraint for each element of list
8+type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
9+ AllSatisfy c '[] = ()
10+ AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
src/TypeFun/Data/Eq.hs+3−1
@@ -1,4 +1,6 @@
1−module TypeFun.Data.Eq where
1+module TypeFun.Data.Eq
2+ ( Equal
3+ ) where
2
4
3type family Equal (a :: k) (b :: k) :: Bool where
5type family Equal (a :: k) (b :: k) :: Bool where
4 Equal a a = 'True
6 Equal a a = 'True
src/TypeFun/Data/List.hs+175−34
@@ -1,52 +1,183 @@
1-- | Collection of type families on type lists. This module differs
1-- | Collection of type families on type lists. This module differs
2-- from __Data.Singletons.Prelude.List__ because works with __[*]__
2-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3−-- and relies on GHC's type equality (~)
3+-- and relies on GHC's type equality (~). The rest of required
4−
4+-- operations like 'Reverse' or '(:++:)' you could find in singletons
5+
5−module TypeFun.Data.List where
6+module TypeFun.Data.List
7+ ( -- * Primitive operations on lists
8+ Length
9+ , Drop
10+ , Take
11+ , Delete
12+ , Remove
13+ , (:++:)
14+ -- * Elements lookup
15+ , IndexOf
16+ , IndexOfMay
17+ , IndexOfMay'
18+ , IndicesOfMay
19+ , IndicesOf
20+ , Index
21+ , IndexMay
22+ , IndicesMay
23+ , Indices
24+ , Elem
25+ , NotElem
26+ , Count
27+ -- * Operations with lists
28+ , SubList
29+ , NotSubList
30+ , IsPrefixOf
31+ , IsNotPrefixOf
32+ , IsPrefixOfBool
33+ -- * Set operations
34+ , Union
35+ , UnionList
36+ , AppendUniq
37+ , Intersect
38+ , Substract
39+ -- * Uniqueness checking
40+ , ElementIsUniq
41+ , UniqElements
42+ , UniqElements'
43+ -- * Unsafe helpers
44+ , appendId
45+ , subListId
46+ ) where
6
47
7import Data.Type.Bool
48import Data.Type.Bool
8import GHC.Exts
49import GHC.Exts
9import GHC.TypeLits
50import GHC.TypeLits
10import TypeFun.Data.Eq
51import TypeFun.Data.Eq
11−import TypeFun.Data.List.Errors
12import TypeFun.Data.Maybe
52import TypeFun.Data.Maybe
13import TypeFun.Data.Peano
53import TypeFun.Data.Peano
54+import Unsafe.Coerce
55+
56+------------------------------------------------------------------------
57+-- NOTE: Errors type classes. These type classes are not in separate --
58+-- module because in this case user could import them and instantiate --
59+-- by mistake. The name of typeclass is an error message in fact. We --
60+-- have not any way to fail constraint explicitly, so this hack was --
61+-- introduced. --
62+------------------------------------------------------------------------
63+
64+class ElementNotFoundInList a s
65+
66+class ElementIsInList a s
67+
68+class ListIsNotPrefixOf a b
69+
70+class ListIsPrefixOf a b
71+
72+class ElementIsNotUniqInList a s
73+
74+class IndexNotFoundInList a s
75+
76+----------------------
77+-- main module code --
78+----------------------
79+
14
80
15type family Length (a :: [k]) :: N where
81type family Length (a :: [k]) :: N where
16 Length '[] = 'Z
82 Length '[] = 'Z
17 Length (a ': as) = 'S (Length as)
83 Length (a ': as) = 'S (Length as)
18
84
85+type family Drop (c :: N) (s :: [k]) :: [k] where
86+ Drop 'Z s = s
87+ Drop ('S c) '[] = '[]
88+ Drop ('S c) (a ': as) = Drop c as
89+
90+type family Take (c :: N) (s :: [k]) :: [k] where
91+ Take 'Z s = '[]
92+ Take ('S c) '[] = '[]
93+ Take ('S c) (a ': as) = a ': (Take c as)
94+
95+-- | Remove first argument type from anywhere in a list.
96+type family Delete (a :: k) (s :: [k]) :: [k] where
97+ Delete a '[] = '[]
98+ Delete a (a ': as) = Delete a as
99+ Delete a (b ': as) = b ': (Delete a as)
100+
101+-- | Remove index from the list
102+type family Remove (i :: N) (a :: [k]) :: [k] where
103+ Remove i '[] = '[]
104+ Remove 'Z (a ': as) = as
105+ Remove ('S i) (a ': as) = a ': (Remove i as)
106+
107+type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
108+ '[] :++: b = b
109+ (a ': as) :++: b = a ': (as :++: b)
110+
111+appendId
112+ :: forall proxy l r
113+ . proxy l
114+ -> (l ~ (l :++: '[]) => r)
115+ -> r
116+appendId = unsafeCoerce id
117+
118+type IndexOf a s = FromJust (IndexOfMay a s)
119+
120+type IndexOfMay a s = IndexOfMay' Z a s
121+
122+type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
123+ IndexOfMay' acc a '[] = 'Nothing
124+ IndexOfMay' acc a (a ': as) = 'Just acc
125+ IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as
126+
127+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
128+ IndicesOfMay '[] bs = '[]
129+ IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
130+
131+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
132+ IndicesOf '[] bs = '[]
133+ IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
134+
135+type Index idx s = FromJust (IndexMay idx s)
136+
137+type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where
138+ IndexMay idx '[] = 'Nothing
139+ IndexMay Z (a ': as) = 'Just a
140+ IndexMay (S idx) (a ': as) = IndexMay idx as
141+
142+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
143+ IndicesMay '[] as = '[]
144+ IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)
145+
146+type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
147+ Indices '[] as = '[]
148+ Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
149+
19-- | Generates unresolvable constraint if fists element is not
150-- | Generates unresolvable constraint if fists element is not
20-- contained inside of second
151-- contained inside of second
21−type Elem a s = NothingToConstr (IndexOf a s)
152+type Elem a s = NothingToConstr (IndexOfMay a s)
22 (ElementNotFoundInList a s)
153 (ElementNotFoundInList a s)
23
154
24-- | Reverse of 'Elem'
155-- | Reverse of 'Elem'
25−type NotElem a s = JustToConstr (IndexOf a s)
156+type NotElem a s = JustToConstr (IndexOfMay a s)
26 (ElementIsInList a s)
157 (ElementIsInList a s)
27
158
159+-- | Count elements in a list
160+type family Count (a :: k) (s :: [k]) :: N where
161+ Count a '[] = 'Z
162+ Count a (a ': as) = 'S (Count a as)
163+ Count a (b ': as) = Count a as
164+
28-- | Constanints that first argument is a sublist of second. Reduces
165-- | Constanints that first argument is a sublist of second. Reduces
29-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
166-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
30type family SubList (a :: [k]) (b :: [k]) :: Constraint where
167type family SubList (a :: [k]) (b :: [k]) :: Constraint where
31 SubList '[] bs = ()
168 SubList '[] bs = ()
32 SubList (a ': as) bs = (Elem a bs, SubList as bs)
169 SubList (a ': as) bs = (Elem a bs, SubList as bs)
33
170
171+subListId
172+ :: forall proxy l r
173+ . proxy l
174+ -> (SubList l l => r) -> r
175+subListId _ = unsafeCoerce id
176+
34type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
177type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
35 NotSubList '[] bs = ()
178 NotSubList '[] bs = ()
36 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
179 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
37
180
38−type IndexOf a s = IndexOf' Z a s
39−
40−type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
41− IndexOf' acc a '[] = 'Nothing
42− IndexOf' acc a (a ': as) = 'Just acc
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
49−
50type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
181type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
51 (() :: Constraint)
182 (() :: Constraint)
52 (ListIsNotPrefixOf a b)
183 (ListIsNotPrefixOf a b)
@@ -62,30 +193,40 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
62 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
193 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
63 IsPrefixOfBool as bs = 'False
194 IsPrefixOfBool as bs = 'False
64
195
196+-- | Appends elements from first list to second if they are not
197+-- presented in.
198+type family Union (a :: [k]) (b :: [k]) :: [k] where
199+ Union '[] bs = bs
200+ Union (a ': as) bs = Union as (AppendUniq a bs)
201+
202+type family UnionList (l :: [[k]]) :: [k] where
203+ UnionList '[] = '[]
204+ UnionList (a ': as) = Union a (UnionList as)
205+
206+-- | Append element to list if element is not already presented in
207+type family AppendUniq (a :: k) (s :: [k]) :: [k] where
208+ AppendUniq a (a ': bs) = a ': bs
209+ AppendUniq a (b ': bs) = b ': (AppendUniq a bs)
210+ AppendUniq a '[] = '[a]
211+
212+-- | Calculates intersection between two lists. Order of elements is
213+-- taken from first list
214+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
215+
216+-- | Removes from first list all elements occured in second
217+type family Substract (a :: [k]) (b :: [k]) :: [k] where
218+ Substract '[] b = '[]
219+ Substract a '[] = a
220+ Substract a (b ': bs) = Substract (Delete b a) bs
221+
65-- | Checks that element 'a' occurs in a list just once
222-- | Checks that element 'a' occurs in a list just once
66type ElementIsUniq a s = If (Equal (S Z) (Count a s))
223type ElementIsUniq a s = If (Equal (S Z) (Count a s))
67 (() :: Constraint)
224 (() :: Constraint)
68 (ElementIsNotUniqInList a s)
225 (ElementIsNotUniqInList a s)
69
226
70−-- | Count elements in a list
71−type family Count (a :: k) (s :: [k]) :: N where
72− Count a '[] = 'Z
73− Count a (a ': as) = 'S (Count a as)
74− Count a (b ': as) = Count a as
75−
76-- | Checks that all elements in list are unique
227-- | Checks that all elements in list are unique
77type UniqElements a = UniqElements' a a
228type UniqElements a = UniqElements' a a
78
229
79type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
230type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
80 UniqElements' '[] self = ()
231 UniqElements' '[] self = ()
81 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
232 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
82−
83−type family Drop (c :: N) (s :: [k]) :: [k] where
84− Drop 'Z s = s
85− Drop ('S c) '[] = '[]
86− Drop ('S c) (a ': as) = Drop c as
87−
88−type family Take (c :: N) (s :: [k]) :: [k] where
89− Take 'Z s = '[]
90− Take ('S c) '[] = '[]
91− Take ('S c) (a ': as) = a ': (Take c as)
src/TypeFun/Data/List/Errors.hsdeleted−11
@@ -1,11 +0,0 @@
1−module TypeFun.Data.List.Errors 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
10−
11−class ElementIsNotUniqInList a s
src/TypeFun/Data/Maybe.hs+16−2
@@ -1,4 +1,10 @@
1−module TypeFun.Data.Maybe where
1+module TypeFun.Data.Maybe
2+ ( MaybeCase
3+ , NothingToConstr
4+ , JustToConstr
5+ , CatMaybes
6+ , FromJust
7+ ) where
2
8
3import GHC.Exts
9import GHC.Exts
4
10
@@ -8,7 +14,6 @@ type family MaybeCase (a :: Maybe k)
8 MaybeCase 'Nothing nothing just = nothing
14 MaybeCase 'Nothing nothing just = nothing
9 MaybeCase ('Just k) nothing just = just k
15 MaybeCase ('Just k) nothing just = just k
10
16
11−
12type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
13 NothingToConstr 'Nothing c = c
18 NothingToConstr 'Nothing c = c
14 NothingToConstr ('Just a) c = ()
19 NothingToConstr ('Just a) c = ()
@@ -16,3 +21,12 @@ type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
16type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
21type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
17 JustToConstr 'Nothing c = ()
22 JustToConstr 'Nothing c = ()
18 JustToConstr ('Just a) c = c
23 JustToConstr ('Just a) c = c
24+
25+-- | Like 'catMaybes' for type lists
26+type family CatMaybes (l :: [Maybe k]) :: [k] where
27+ CatMaybes '[] = '[]
28+ CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
29+ CatMaybes ('Nothing ': as) = CatMaybes as
30+
31+type family FromJust (a :: Maybe k) :: k where
32+ FromJust ('Just a) = a
src/TypeFun/Data/Peano.hs+22−4
@@ -1,13 +1,31 @@
1−module TypeFun.Data.Peano where
1+module TypeFun.Data.Peano
2+ ( N(..)
3+ , KnownPeano(..)
4+ , ToNat
5+ , FromNat
6+ , (:+:)
7+ , (:-:)
8+ , (:*:)
9+ ) where
2
10
3−import Data.Typeable
11+import Data.Typeable
4−import GHC.Generics (Generic)
12+import GHC.Generics (Generic)
5−import GHC.TypeLits
13+import GHC.TypeLits
6
14
7data N = Z | S N
15data N = Z | S N
8 deriving ( Eq, Ord, Read, Show
16 deriving ( Eq, Ord, Read, Show
9 , Generic, Typeable )
17 , Generic, Typeable )
10
18
19+-- | @since 0.1.2
20+class KnownPeano (p :: N) where
21+ peanoVal :: proxy p -> Integer
22+
23+instance KnownPeano Z where
24+ peanoVal _ = 0
25+
26+instance (KnownPeano n) => KnownPeano (S n) where
27+ peanoVal _ = succ $ peanoVal (Proxy :: Proxy n)
28+
11type family ToNat (a :: N) :: Nat where
29type family ToNat (a :: N) :: Nat where
12 ToNat Z = 0
30 ToNat Z = 0
13 ToNat (S a) = 1 + (ToNat a)
31 ToNat (S a) = 1 + (ToNat a)
stack.yamlnew file+9
@@ -0,0 +1,9 @@
1+nix:
2+ packages:
3+ - zlib
4+ - postgresql
5+
6+resolver: lts-13.21
7+
8+packages:
9+ - .
stack.yaml.locknew file+12
@@ -0,0 +1,12 @@
1+# This file was autogenerated by Stack.
2+# You should not edit this file by hand.
3+# For more information, please see the documentation at:
4+# https://docs.haskellstack.org/en/stable/lock_files
5+
6+packages: []
7+snapshots:
8+- completed:
9+ size: 498180
10+ url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/13/21.yaml
11+ sha256: eff2de19a6d4691ccbf6edc1fba858f1918683047dce0f09adede874bbd2a8f3
12+ original: lts-13.21
type-fun.cabal+14−11
@@ -1,47 +1,50 @@
1−-- Initial type-fun.cabal generated by cabal init. For further
2−-- documentation, see http://haskell.org/cabal/users-guide/
3−
4name: type-fun
1name: type-fun
5−version: 0.0.1
2+version: 0.1.2
6synopsis: Collection of widely reimplemented type families
3synopsis: Collection of widely reimplemented type families
7−-- description:
8license: BSD3
4license: BSD3
9license-file: LICENSE
5license-file: LICENSE
10author: Aleksey Uimanov
6author: Aleksey Uimanov
11maintainer: s9gf4ult@gmail.com
7maintainer: s9gf4ult@gmail.com
12−-- copyright:
13category: Dependent Types
8category: Dependent Types
14build-type: Simple
9build-type: Simple
15−-- extra-source-files:
10+extra-source-files: CHANGELOG.md
16cabal-version: >=1.10
11cabal-version: >=1.10
12+homepage: https://github.com/s9gf4ult/type-fun
13+source-repository head
14+ type: git
15+ location: git@github.com:s9gf4ult/type-fun.git
17
16
18library
17library
19 default-language: Haskell2010
18 default-language: Haskell2010
20 hs-source-dirs: src
19 hs-source-dirs: src
21 default-extensions: ConstraintKinds
20 default-extensions: ConstraintKinds
22 , DataKinds
21 , DataKinds
22+ , DeriveDataTypeable
23 , DeriveGeneric
23 , DeriveGeneric
24 , FlexibleInstances
24 , FlexibleInstances
25 , MultiParamTypeClasses
25 , MultiParamTypeClasses
26 , PolyKinds
26 , PolyKinds
27+ , RankNTypes
28+ , ScopedTypeVariables
27 , TypeFamilies
29 , TypeFamilies
28 , TypeOperators
30 , TypeOperators
29 , UndecidableInstances
31 , UndecidableInstances
30
32
31− exposed-modules: TypeFun.Data.Eq
33+ exposed-modules: TypeFun.Constraint
34+ , TypeFun.Data.Eq
32 , TypeFun.Data.List
35 , TypeFun.Data.List
33 , TypeFun.Data.Maybe
36 , TypeFun.Data.Maybe
34 , TypeFun.Data.Peano
37 , TypeFun.Data.Peano
35
38
36− build-depends: base >=4.7 && <4.9
39+ build-depends: base >= 4.7 && < 5
37−
38
40
39test-suite example
41test-suite example
40 type: exitcode-stdio-1.0
42 type: exitcode-stdio-1.0
41 default-language: Haskell2010
43 default-language: Haskell2010
42 hs-source-dirs: example
44 hs-source-dirs: example
43 main-is: Main.hs
45 main-is: Main.hs
44− default-extensions: DataKinds
46+ default-extensions: ConstraintKinds
47+ , DataKinds
45 , GADTs
48 , GADTs
46 , TemplateHaskell
49 , TemplateHaskell
47 , TypeFamilies
50 , TypeFamilies