77cb83c..master · type-fun

.gitignore+1

since splitsnapshots

unifiedsplit

@@ -2,3 +2,4 @@ dist

2TAGS

3.cabal-sandbox

4cabal.sandbox.config

5+.stack-work

CHANGELOG.md+15

@@ -4,5 +4,20 @@

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+

7## 0.0.1

22## 0.0.1

8First version

23First 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/Data/List.hs+17

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

40 , ElementIsUniq

41 , UniqElements

42 , UniqElements'

43+ -- * Unsafe helpers

44+ , appendId

45+ , subListId

43 ) where

46 ) where

44

47

45import Data.Type.Bool

48import Data.Type.Bool

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

48import TypeFun.Data.Eq

51import TypeFun.Data.Eq

49import TypeFun.Data.Maybe

52import TypeFun.Data.Maybe

50import TypeFun.Data.Peano

53import TypeFun.Data.Peano

54+import Unsafe.Coerce

51

55

52------------------------------------------------------------------------

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

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

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

@@ -104,6 +108,13 @@ type family (:++:) (a :: [k]) (b :: [k]) :: [k] where

104 '[] :++: b = b

108 '[] :++: b = b

105 (a ': as) :++: b = a ': (as :++: b)

109 (a ': as) :++: b = a ': (as :++: b)

106

110

111+appendId

112+ :: forall proxy l r

113+ . proxy l

114+ -> (l ~ (l :++: '[]) => r)

115+ -> r

116+appendId = unsafeCoerce id

117+

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

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

108

119

109type IndexOfMay a s = IndexOfMay' Z a s

120type IndexOfMay a s = IndexOfMay' Z a s

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

157 SubList '[] bs = ()

168 SubList '[] bs = ()

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

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

159

170

171+subListId

172+ :: forall proxy l r

173+ . proxy l

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

175+subListId _ = unsafeCoerce id

176+

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

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

161 NotSubList '[] bs = ()

178 NotSubList '[] bs = ()

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

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

src/TypeFun/Data/Peano.hs+14−3

@@ -1,5 +1,6 @@

1module TypeFun.Data.Peano

2 ( N(..)

3+ , KnownPeano(..)

3 , ToNat

4 , ToNat

4 , FromNat

5 , FromNat

5 , (:+:)

6 , (:+:)

@@ -7,14 +8,24 @@ module TypeFun.Data.Peano

7 , (:*:)

8 , (:*:)

8 ) where

9 ) where

9

10

10−import Data.Typeable

11+import Data.Typeable

11−import GHC.Generics (Generic)

12+import GHC.Generics (Generic)

12−import GHC.TypeLits

13+import GHC.TypeLits

13

14

14data N = Z | S N

15data N = Z | S N

15 deriving ( Eq, Ord, Read, Show

16 deriving ( Eq, Ord, Read, Show

16 , Generic, Typeable )

17 , Generic, Typeable )

17

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+

18type family ToNat (a :: N) :: Nat where

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

19 ToNat Z = 0

30 ToNat Z = 0

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

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

1name: type-fun

2−version: 0.0.1

2+version: 0.1.2

3synopsis: Collection of widely reimplemented type families

4license: BSD3

5license-file: LICENSE

@@ -19,10 +19,13 @@ library

19 hs-source-dirs: src

20 default-extensions: ConstraintKinds

21 , DataKinds

22+ , DeriveDataTypeable

22 , DeriveGeneric

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

@@ -33,15 +36,15 @@ library

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