master..8832366 · type-fun

.gitignore−1

since splitsnapshots

unifiedsplit

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

2TAGS

3.cabal-sandbox

4cabal.sandbox.config

5−.stack-work

CHANGELOG.md−15

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

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

7## 0.0.1

23First version

8First version

example/Main.hs−1

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

37 print $ prefixConstr p2

38 print $ prefixConstr p3

39 print $ uniqConstr p2

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

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

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

src/TypeFun/Data/List.hs−24

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

35 , UnionList

36 , AppendUniq

37 , Intersect

38− , Substract

39 -- * Uniqueness checking

38 -- * Uniqueness checking

40 , ElementIsUniq

39 , ElementIsUniq

41 , UniqElements

40 , UniqElements

42 , UniqElements'

41 , UniqElements'

43− -- * Unsafe helpers

44− , appendId

45− , subListId

46 ) where

42 ) where

47

43

48import Data.Type.Bool

44import Data.Type.Bool

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

51import TypeFun.Data.Eq

47import TypeFun.Data.Eq

52import TypeFun.Data.Maybe

48import TypeFun.Data.Maybe

53import TypeFun.Data.Peano

49import TypeFun.Data.Peano

54−import Unsafe.Coerce

55

50

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

51------------------------------------------------------------------------

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

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

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

108 '[] :++: b = b

103 '[] :++: b = b

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

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

110

105

111−appendId

112− :: forall proxy l r

113− . proxy l

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

115− -> r

116−appendId = unsafeCoerce id

117−

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

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

119

107

120type IndexOfMay a s = IndexOfMay' Z a s

108type IndexOfMay a s = IndexOfMay' Z a s

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

168 SubList '[] bs = ()

156 SubList '[] bs = ()

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

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

170

158

171−subListId

172− :: forall proxy l r

173− . proxy l

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

175−subListId _ = unsafeCoerce id

176−

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

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

178 NotSubList '[] bs = ()

160 NotSubList '[] bs = ()

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

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

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

213-- taken from first list

195-- taken from first list

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

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

215

197

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

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

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

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

224 (() :: Constraint)

200 (() :: Constraint)

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

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

1module TypeFun.Data.Peano

2 ( N(..)

3− , KnownPeano(..)

4 , ToNat

3 , ToNat

5 , FromNat

4 , FromNat

6 , (:+:)

5 , (:+:)

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

8 , (:*:)

7 , (:*:)

9 ) where

8 ) where

10

9

11−import Data.Typeable

10+import Data.Typeable

12−import GHC.Generics (Generic)

11+import GHC.Generics (Generic)

13−import GHC.TypeLits

12+import GHC.TypeLits

14

13

15data N = Z | S N

14data N = Z | S N

16 deriving ( Eq, Ord, Read, Show

15 deriving ( Eq, Ord, Read, Show

17 , Generic, Typeable )

16 , Generic, Typeable )

18

17

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−

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

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

30 ToNat Z = 0

19 ToNat Z = 0

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

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

stack.yamldeleted−9

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

1−nix:

2− packages:

3− - zlib

4− - postgresql

5−

6−resolver: lts-13.21

7−

8−packages:

9− - .

stack.yaml.lockdeleted−12

@@ -1,12 +0,0 @@

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

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

1+-- Initial type-fun.cabal generated by cabal init. For further

2+-- documentation, see http://haskell.org/cabal/users-guide/

3+

1name: type-fun

4name: type-fun

2−version: 0.1.2

5+version: 0.0.1

3synopsis: Collection of widely reimplemented type families

6synopsis: Collection of widely reimplemented type families

7+-- description:

4license: BSD3

8license: BSD3

5license-file: LICENSE

9license-file: LICENSE

6author: Aleksey Uimanov

10author: Aleksey Uimanov

7maintainer: s9gf4ult@gmail.com

11maintainer: s9gf4ult@gmail.com

12+-- copyright:

8category: Dependent Types

13category: Dependent Types

9build-type: Simple

14build-type: Simple

10−extra-source-files: CHANGELOG.md

15+-- extra-source-files:

11cabal-version: >=1.10

16cabal-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

16

17

17library

18library

18 default-language: Haskell2010

19 default-language: Haskell2010

19 hs-source-dirs: src

20 hs-source-dirs: src

20 default-extensions: ConstraintKinds

21 default-extensions: ConstraintKinds

21 , DataKinds

22 , DataKinds

22− , DeriveDataTypeable

23 , DeriveGeneric

24 , FlexibleInstances

25 , MultiParamTypeClasses

26 , PolyKinds

27− , RankNTypes

28− , ScopedTypeVariables

29 , TypeFamilies

27 , TypeFamilies

30 , TypeOperators

28 , TypeOperators

31 , UndecidableInstances

29 , UndecidableInstances

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

36 , TypeFun.Data.Maybe

34 , TypeFun.Data.Maybe

37 , TypeFun.Data.Peano

35 , TypeFun.Data.Peano

38

36

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

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

38+

40

39

41test-suite example

40test-suite example

42 type: exitcode-stdio-1.0

41 type: exitcode-stdio-1.0

43 default-language: Haskell2010

42 default-language: Haskell2010

44 hs-source-dirs: example

43 hs-source-dirs: example

45 main-is: Main.hs

44 main-is: Main.hs

46− default-extensions: ConstraintKinds

45+ default-extensions: DataKinds

47− , DataKinds

48 , GADTs

46 , GADTs

49 , TemplateHaskell

47 , TemplateHaskell

50 , TypeFamilies

48 , TypeFamilies