23bb88c..master · type-fun

git.iko.soy/type-fun

on master help sign in

.gitignorenew file+5

since splitsnapshots

unifiedsplit

@@ -0,0 +1,5 @@

1+dist

2+TAGS

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)?

5+# CHANGELOG

7+## 0.1.2

8+### Added KnownPeano

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+12−4

@@ -2,6 +2,7 @@ module Main where

3import Data.Proxy

4import TypeFun.Data.List

5+import TypeFun.Data.Peano

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

@@ -17,17 +18,24 @@ sublistConstr p = elemConstr p + 1

17prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int

18prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int

18prefixConstr p = sublistConstr p + 1

19prefixConstr p = sublistConstr p + 1

20−-- | 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__

21−-- is a first argument__ and uses inside more wide function

23+-- and uses inside more wide function

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

24+indexConstr :: (('Just 'Z) ~ (IndexOfMay Int l)) => proxy l -> Int

23indexConstr p = elemConstr p + 1

25indexConstr p = elemConstr p + 1

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

28+uniqConstr _ = 1

29+

25main :: IO ()

30main :: IO ()

26main = do

31main = do

27 let

32 let

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

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

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

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

30 print $ indexConstr p2

35 print $ indexConstr p2

31 print $ sublistConstr p2

36 print $ sublistConstr p2

32 print $ prefixConstr p2

37 print $ prefixConstr p2

33 print $ prefixConstr p3

38 print $ prefixConstr p3

39+ print $ uniqConstr p2

40+ print $ peanoVal (Proxy :: Proxy (FromNat 100))

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

5+import GHC.Exts

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+6−3

@@ -1,4 +1,7 @@

1−module TypeFun.Data.Eq where

1+module TypeFun.Data.Eq

2+ ( Equal

3+ ) where

3−class Equality a b

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

4−instance Equality a a

6+ Equal a a = 'True

7+ Equal a b = 'False

src/TypeFun/Data/List.hs+194−19

@@ -1,24 +1,166 @@

1-- | Collection of type families on type lists. This module differs

2−-- from __Data.Singletons.Prelude.List__ because it polykinded and

2+-- from __Data.Singletons.Prelude.List__ because works with __[*]__

3−-- works with __[*]__ as well

3+-- and relies on GHC's type equality (~). The rest of required

4+-- operations like 'Reverse' or '(:++:)' you could find in singletons

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

7import Data.Type.Bool

48import Data.Type.Bool

8import GHC.Exts

49import GHC.Exts

9import GHC.TypeLits

50import GHC.TypeLits

10−import TypeFun.Data.List.Internal

51+import TypeFun.Data.Eq

11import TypeFun.Data.Maybe

52import TypeFun.Data.Maybe

53+import 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+

80+

81+type family Length (a :: [k]) :: N where

82+ Length '[] = 'Z

83+ Length (a ': as) = 'S (Length as)

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

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

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

14-- contained inside of second

151-- contained inside of second

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

152+type Elem a s = NothingToConstr (IndexOfMay a s)

16 (ElementNotFoundInList a s)

153 (ElementNotFoundInList a s)

154

18-- | Reverse of 'Elem'

155-- | Reverse of 'Elem'

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

156+type NotElem a s = JustToConstr (IndexOfMay a s)

20 (ElementIsInList a s)

157 (ElementIsInList a s)

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

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

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

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

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

@@ -26,20 +168,15 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where

26 SubList '[] bs = ()

168 SubList '[] bs = ()

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

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

170

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

171+subListId

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

172+ :: forall proxy l r

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

173+ . proxy l

32−

174+ -> (SubList l l => r) -> r

33−

175+subListId _ = unsafeCoerce id

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

35−-- UniqElemsBool

36−

37−type IndexOf a s = IndexOf' 0 a s

176

39−type family IndexOf' (acc :: Nat) (a :: k) (s :: [k]) :: Maybe Nat where

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

40− IndexOf' acc a '[] = 'Nothing

178+ NotSubList '[] bs = ()

41− IndexOf' acc a (a ': as) = 'Just acc

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

42− IndexOf' acc a (b ': as) = IndexOf' (acc + 1) a as

180

44type IsPrefixOf a b = ( If (IsPrefixOfBool a b)

181type IsPrefixOf a b = ( If (IsPrefixOfBool a b)

45 (() :: Constraint)

182 (() :: Constraint)

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

55 IsPrefixOfBool '[] b = 'True

192 IsPrefixOfBool '[] b = 'True

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

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

57 IsPrefixOfBool as bs = 'False

194 IsPrefixOfBool as bs = 'False

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+

222+-- | Checks that element 'a' occurs in a list just once

223+type ElementIsUniq a s = If (Equal (S Z) (Count a s))

224+ (() :: Constraint)

225+ (ElementIsNotUniqInList a s)

226+

227+-- | Checks that all elements in list are unique

228+type UniqElements a = UniqElements' a a

229+

230+type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where

231+ UniqElements' '[] self = ()

232+ UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)

src/TypeFun/Data/List/Internal.hsdeleted−9

@@ -1,9 +0,0 @@

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.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

3import GHC.Exts

9import GHC.Exts

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

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.hsnew file+48

@@ -0,0 +1,48 @@

1+module TypeFun.Data.Peano

2+ ( N(..)

3+ , KnownPeano(..)

4+ , ToNat

5+ , FromNat

6+ , (:+:)

7+ , (:-:)

8+ , (:*:)

9+ ) where

10+

11+import Data.Typeable

12+import GHC.Generics (Generic)

13+import GHC.TypeLits

14+

15+data N = Z | S N

16+ deriving ( Eq, Ord, Read, Show

17+ , Generic, Typeable )

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+

29+type family ToNat (a :: N) :: Nat where

30+ ToNat Z = 0

31+ ToNat (S a) = 1 + (ToNat a)

32+

33+type family FromNat (a :: Nat) :: N where

34+ FromNat 0 = Z

35+ FromNat a = S (FromNat (a - 1))

36+

37+type family (:+:) (a :: N) (b :: N) :: N where

38+ Z :+: b = b

39+ (S a) :+: b = a :+: (S b)

40+

41+type family (:-:) (a :: N) (b :: N) :: N where

42+ a :-: Z = a

43+ (S a) :-: (S b) = a :-: b

44+

45+type family (:*:) (a :: N) (b :: N) :: N where

46+ Z :*: b = Z

47+ a :*: Z = Z

48+ (S a) :*: b = b :+: (a :*: b)

stack.yamlnew file+9

@@ -0,0 +1,9 @@

1+nix:

2+ packages:

3+ - zlib

4+ - postgresql

6+resolver: lts-13.21

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

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+16−11

@@ -1,45 +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

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 , FlexibleInstances

24 , FlexibleInstances

24 , MultiParamTypeClasses

25 , MultiParamTypeClasses

25 , PolyKinds

26 , PolyKinds

27+ , RankNTypes

28+ , ScopedTypeVariables

26 , TypeFamilies

29 , TypeFamilies

27 , TypeOperators

30 , TypeOperators

28 , UndecidableInstances

31 , UndecidableInstances

30− exposed-modules: TypeFun.Data.Eq

33+ exposed-modules: TypeFun.Constraint

34+ , TypeFun.Data.Eq

31 , TypeFun.Data.List

35 , TypeFun.Data.List

32 , TypeFun.Data.Maybe

36 , TypeFun.Data.Maybe

37+ , TypeFun.Data.Peano

34− build-depends: base >=4.7 && <4.9

39+ build-depends: base >= 4.7 && < 5

35−

37test-suite example

41test-suite example

38 type: exitcode-stdio-1.0

42 type: exitcode-stdio-1.0

39 default-language: Haskell2010

43 default-language: Haskell2010

40 hs-source-dirs: example

44 hs-source-dirs: example

41 main-is: Main.hs

45 main-is: Main.hs

42− default-extensions: DataKinds

46+ default-extensions: ConstraintKinds

47+ , DataKinds

43 , GADTs

48 , GADTs

44 , TemplateHaskell

49 , TemplateHaskell

45 , TypeFamilies

50 , TypeFamilies