master..7c20294 · type-fun

git.iko.soy/type-fun

on 7c20294 help sign in

.gitignore−3

since splitsnapshots

unifiedsplit

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

1dist

2TAGS

3−.cabal-sandbox

4−cabal.sandbox.config

5−.stack-work

CHANGELOG.mddeleted−23

@@ -1,23 +0,0 @@

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

@@ -18,10 +18,9 @@ sublistConstr p = elemConstr p + 1

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

19prefixConstr p = sublistConstr p + 1

21−-- | This function has narrower constraint

21+-- | This function has narrower constraint __Int is inside of l and it

22−-- __Int is inside of l and it is a first argument__

23−-- and uses inside more wide function

22+-- is a first argument__ and uses inside more wide function

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

23+indexConstr :: (('Just 'Z) ~ (IndexOf Int l)) => proxy l -> Int

25indexConstr p = elemConstr p + 1

24indexConstr p = elemConstr p + 1

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

26uniqConstr :: (UniqElements l) => proxy l -> Int

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

37 print $ prefixConstr p2

36 print $ prefixConstr p2

38 print $ prefixConstr p3

37 print $ prefixConstr p3

39 print $ uniqConstr p2

38 print $ uniqConstr p2

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

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

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

src/TypeFun/Constraint.hs+1−4

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

1−module TypeFun.Constraint

1+module TypeFun.Constraint where

2− ( AllSatisfy

3− ) where

5import GHC.Exts

3import GHC.Exts

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

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

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

9 AllSatisfy c '[] = ()

6 AllSatisfy c '[] = ()

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

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

src/TypeFun/Data/Eq.hs+1−3

@@ -1,6 +1,4 @@

1−module TypeFun.Data.Eq

1+module TypeFun.Data.Eq where

2− ( Equal

3− ) where

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

3type family Equal (a :: k) (b :: k) :: Bool where

6 Equal a a = 'True

4 Equal a a = 'True

src/TypeFun/Data/List.hs+17−76

@@ -9,17 +9,11 @@ module TypeFun.Data.List

9 , Drop

10 , Take

11 , Delete

12− , Remove

13− , (:++:)

14 -- * Elements lookup

12 -- * Elements lookup

15 , IndexOf

13 , IndexOf

16− , IndexOfMay

14+ , IndexOf'

17− , IndexOfMay'

18− , IndicesOfMay

19 , IndicesOf

15 , IndicesOf

20 , Index

16 , Index

21− , IndexMay

22− , IndicesMay

23 , Indices

17 , Indices

24 , Elem

18 , Elem

25 , NotElem

19 , NotElem

@@ -30,19 +24,13 @@ module TypeFun.Data.List

30 , IsPrefixOf

24 , IsPrefixOf

31 , IsNotPrefixOf

25 , IsNotPrefixOf

32 , IsPrefixOfBool

26 , IsPrefixOfBool

33− -- * Set operations

34 , Union

27 , Union

35− , UnionList

36 , AppendUniq

28 , AppendUniq

37 , Intersect

29 , Intersect

38− , Substract

39 -- * Uniqueness checking

30 -- * Uniqueness checking

40 , ElementIsUniq

31 , ElementIsUniq

41 , UniqElements

32 , UniqElements

42 , UniqElements'

33 , UniqElements'

43− -- * Unsafe helpers

44− , appendId

45− , subListId

46 ) where

34 ) where

48import Data.Type.Bool

36import Data.Type.Bool

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

51import TypeFun.Data.Eq

39import TypeFun.Data.Eq

52import TypeFun.Data.Maybe

40import TypeFun.Data.Maybe

53import TypeFun.Data.Peano

41import TypeFun.Data.Peano

54−import Unsafe.Coerce

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

43------------------------------------------------------------------------

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

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

@@ -71,8 +58,6 @@ class ListIsPrefixOf a b

72class ElementIsNotUniqInList a s

59class ElementIsNotUniqInList a s

74−class IndexNotFoundInList a s

75−

76----------------------

61----------------------

77-- main module code --

62-- main module code --

78----------------------

63----------------------

@@ -98,62 +83,34 @@ type family Delete (a :: k) (s :: [k]) :: [k] where

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

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

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

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

100

101−-- | Remove index from the list

86+type IndexOf a s = IndexOf' Z a s

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

88+type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where

128− IndicesOfMay '[] bs = '[]

89+ IndexOf' acc a '[] = 'Nothing

129− IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)

90+ IndexOf' acc a (a ': as) = 'Just acc

91+ IndexOf' acc a (b ': as) = IndexOf' (S acc) a as

130

131−type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where

93+type family IndicesOf (a :: [k]) (b :: [k]) :: [Maybe N] where

132 IndicesOf '[] bs = '[]

94 IndicesOf '[] bs = '[]

133 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)

95 IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)

134

135−type Index idx s = FromJust (IndexMay idx s)

97+type family Index (idx :: N) (s :: [k]) :: Maybe k where

98+ Index idx '[] = 'Nothing

99+ Index Z (a ': as) = 'Just a

100+ Index (S idx) (a ': as) = Index idx as

136

101

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

102+type family Indices (idxs :: [N]) (a :: [k]) :: [Maybe k] where

143− IndicesMay '[] as = '[]

103+ Indices '[] 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)

104 Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)

149

105

106+

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

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

151-- contained inside of second

108-- contained inside of second

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

109+type Elem a s = NothingToConstr (IndexOf a s)

153 (ElementNotFoundInList a s)

110 (ElementNotFoundInList a s)

154

111

155-- | Reverse of 'Elem'

112-- | Reverse of 'Elem'

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

113+type NotElem a s = JustToConstr (IndexOf a s)

157 (ElementIsInList a s)

114 (ElementIsInList a s)

158

115

159-- | Count elements in a list

116-- | Count elements in a list

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

168 SubList '[] bs = ()

125 SubList '[] bs = ()

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

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

170

127

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

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

178 NotSubList '[] bs = ()

129 NotSubList '[] bs = ()

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

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

@@ -199,10 +150,6 @@ type family Union (a :: [k]) (b :: [k]) :: [k] where

199 Union '[] bs = bs

150 Union '[] bs = bs

200 Union (a ': as) bs = Union as (AppendUniq a bs)

151 Union (a ': as) bs = Union as (AppendUniq a bs)

201

152

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

153-- | Append element to list if element is not already presented in

207type family AppendUniq (a :: k) (s :: [k]) :: [k] where

154type family AppendUniq (a :: k) (s :: [k]) :: [k] where

208 AppendUniq a (a ': bs) = a ': bs

155 AppendUniq a (a ': bs) = a ': bs

@@ -211,13 +158,7 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where

211

158

212-- | Calculates intersection between two lists. Order of elements is

159-- | Calculates intersection between two lists. Order of elements is

213-- taken from first list

160-- taken from first list

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

161+type Intersect a b = (CatMaybes (Indices (CatMaybes (IndicesOf 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

162

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

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

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

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

src/TypeFun/Data/Maybe.hs+2−11

@@ -1,10 +1,4 @@

1−module TypeFun.Data.Maybe

1+module TypeFun.Data.Maybe where

2− ( MaybeCase

3− , NothingToConstr

4− , JustToConstr

5− , CatMaybes

6− , FromJust

7− ) where

9import GHC.Exts

3import GHC.Exts

@@ -14,6 +8,7 @@ type family MaybeCase (a :: Maybe k)

14 MaybeCase 'Nothing nothing just = nothing

8 MaybeCase 'Nothing nothing just = nothing

15 MaybeCase ('Just k) nothing just = just k

9 MaybeCase ('Just k) nothing just = just k

11+

17type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where

12type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where

18 NothingToConstr 'Nothing c = c

13 NothingToConstr 'Nothing c = c

19 NothingToConstr ('Just a) c = ()

14 NothingToConstr ('Just a) c = ()

@@ -22,11 +17,7 @@ type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where

22 JustToConstr 'Nothing c = ()

17 JustToConstr 'Nothing c = ()

23 JustToConstr ('Just a) c = c

18 JustToConstr ('Just a) c = c

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

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

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

27 CatMaybes '[] = '[]

21 CatMaybes '[] = '[]

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

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

29 CatMaybes ('Nothing ': as) = CatMaybes as

23 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+4−22

@@ -1,31 +1,13 @@

1−module TypeFun.Data.Peano

1+module TypeFun.Data.Peano where

2− ( N(..)

3− , KnownPeano(..)

4− , ToNat

5− , FromNat

6− , (:+:)

7− , (:-:)

8− , (:*:)

9− ) where

11−import Data.Typeable

3+import Data.Typeable

12−import GHC.Generics (Generic)

4+import GHC.Generics (Generic)

13−import GHC.TypeLits

5+import GHC.TypeLits

15data N = Z | S N

7data N = Z | S N

16 deriving ( Eq, Ord, Read, Show

8 deriving ( Eq, Ord, Read, Show

17 , Generic, Typeable )

9 , Generic, Typeable )

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

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

30 ToNat Z = 0

12 ToNat Z = 0

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

13 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/

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

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

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

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

38+

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