4819b04..master · type-fun

.gitignore+3

since splitsnapshots

unifiedsplit

@@ -1,2 +1,5 @@

1dist

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+1

@@ -37,4 +37,5 @@ main = do

37 print $ prefixConstr p2

38 print $ prefixConstr p3

39 print $ uniqConstr p2

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

40 -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]

41 -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]

src/TypeFun/Constraint.hs+4−1

@@ -1,7 +1,10 @@

1−module TypeFun.Constraint where

1+module TypeFun.Constraint

2+ ( AllSatisfy

3+ ) where

2

4

3import GHC.Exts

5import GHC.Exts

4

6

7+-- | Apply constraint for each element of list

5type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where

8type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where

6 AllSatisfy c '[] = ()

9 AllSatisfy c '[] = ()

7 AllSatisfy c (a ': as) = (c a, AllSatisfy c as)

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

@@ -9,6 +9,8 @@ module TypeFun.Data.List

9 , Drop

10 , Take

11 , Delete

12+ , Remove

13+ , (:++:)

12 -- * Elements lookup

14 -- * Elements lookup

13 , IndexOf

15 , IndexOf

14 , IndexOfMay

16 , IndexOfMay

@@ -33,10 +35,14 @@ module TypeFun.Data.List

33 , UnionList

35 , UnionList

34 , AppendUniq

36 , AppendUniq

35 , Intersect

37 , Intersect

38+ , Substract

36 -- * Uniqueness checking

39 -- * Uniqueness checking

37 , ElementIsUniq

40 , ElementIsUniq

38 , UniqElements

41 , UniqElements

39 , UniqElements'

42 , UniqElements'

43+ -- * Unsafe helpers

44+ , appendId

45+ , subListId

40 ) where

46 ) where

41

47

42import Data.Type.Bool

48import Data.Type.Bool

@@ -45,6 +51,7 @@ import GHC.TypeLits

45import TypeFun.Data.Eq

51import TypeFun.Data.Eq

46import TypeFun.Data.Maybe

52import TypeFun.Data.Maybe

47import TypeFun.Data.Peano

53import TypeFun.Data.Peano

54+import Unsafe.Coerce

48

55

49------------------------------------------------------------------------

56------------------------------------------------------------------------

50-- NOTE: Errors type classes. These type classes are not in separate --

57-- NOTE: Errors type classes. These type classes are not in separate --

@@ -91,6 +98,23 @@ type family Delete (a :: k) (s :: [k]) :: [k] where

91 Delete a (a ': as) = Delete a as

98 Delete a (a ': as) = Delete a as

92 Delete a (b ': as) = b ': (Delete a as)

99 Delete a (b ': as) = b ': (Delete a as)

93

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+

94type IndexOf a s = FromJust (IndexOfMay a s)

118type IndexOf a s = FromJust (IndexOfMay a s)

95

119

96type IndexOfMay a s = IndexOfMay' Z a s

120type IndexOfMay a s = IndexOfMay' Z a s

@@ -144,6 +168,12 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where

144 SubList '[] bs = ()

168 SubList '[] bs = ()

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

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

146

170

171+subListId

172+ :: forall proxy l r

173+ . proxy l

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

175+subListId _ = unsafeCoerce id

176+

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

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

148 NotSubList '[] bs = ()

178 NotSubList '[] bs = ()

149 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)

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

@@ -183,6 +213,12 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where

183-- taken from first list

213-- taken from first list

184type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)

214type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)

185

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+

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

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

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

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

188 (() :: Constraint)

224 (() :: Constraint)

src/TypeFun/Data/Maybe.hs+8−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 = ()

@@ -17,6 +22,7 @@ type 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

19

24

25+-- | Like 'catMaybes' for type lists

20type family CatMaybes (l :: [Maybe k]) :: [k] where

26type family CatMaybes (l :: [Maybe k]) :: [k] where

21 CatMaybes '[] = '[]

27 CatMaybes '[] = '[]

22 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)

28 CatMaybes (('Just a) ': as) = a ': (CatMaybes as)

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

@@ -1,29 +1,31 @@

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

24 , FlexibleInstances

25 , MultiParamTypeClasses

26 , PolyKinds

27+ , RankNTypes

28+ , ScopedTypeVariables

27 , TypeFamilies

29 , TypeFamilies

28 , TypeOperators

30 , TypeOperators

29 , UndecidableInstances

31 , UndecidableInstances

@@ -34,15 +36,15 @@ library

34 , TypeFun.Data.Maybe

36 , TypeFun.Data.Maybe

35 , TypeFun.Data.Peano

37 , TypeFun.Data.Peano

36

38

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

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

38−

39

40

40test-suite example

41test-suite example

41 type: exitcode-stdio-1.0

42 type: exitcode-stdio-1.0

42 default-language: Haskell2010

43 default-language: Haskell2010

43 hs-source-dirs: example

44 hs-source-dirs: example

44 main-is: Main.hs

45 main-is: Main.hs

45− default-extensions: DataKinds

46+ default-extensions: ConstraintKinds

47+ , DataKinds

46 , GADTs

48 , GADTs

47 , TemplateHaskell

49 , TemplateHaskell

48 , TypeFamilies

50 , TypeFamilies