master..5b4fad4 · type-fun

git.iko.soy/type-fun

11 files changed+18−128

unifiedsplit

.gitignore−3 CHANGELOG.md−23 example/Main.hs−1 src/TypeFun/Constraint.hs+1−4 src/TypeFun/Data/Eq.hs+1−3 src/TypeFun/Data/List.hs−31 src/TypeFun/Data/Maybe.hs+2−8 src/TypeFun/Data/Peano.hs+4−22 stack.yaml−9 stack.yaml.lock−12 type-fun.cabal+10−12

.gitignore−3

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

11dist

22TAGS

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

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

3737 print $ prefixConstr p2

3838 print $ prefixConstr p3

3939 print $ uniqConstr p2

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

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

src/TypeFun/Constraint.hs+1−4

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

1−module TypeFun.Constraint

2− ( AllSatisfy

3− ) where

1+module TypeFun.Constraint where

53import GHC.Exts

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

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

96 AllSatisfy c '[] = ()

107 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

2− ( Equal

3− ) where

1+module TypeFun.Data.Eq where

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

64 Equal a a = 'True

src/TypeFun/Data/List.hs−31

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

99 , Drop

1010 , Take

1111 , Delete

12− , Remove

1312 , (:++:)

1413 -- * Elements lookup

1514 , IndexOf

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

3534 , UnionList

3635 , AppendUniq

3736 , Intersect

38− , Substract

3937 -- * Uniqueness checking

4038 , ElementIsUniq

4139 , UniqElements

4240 , UniqElements'

43− -- * Unsafe helpers

44− , appendId

45− , subListId

4641 ) where

4742

4843import Data.Type.Bool

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

5146import TypeFun.Data.Eq

5247import TypeFun.Data.Maybe

5348import TypeFun.Data.Peano

54−import Unsafe.Coerce

5549

5650------------------------------------------------------------------------

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

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

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

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

10094

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−

10795type family (:++:) (a :: [k]) (b :: [k]) :: [k] where

10896 '[] :++: b = b

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

11098

111−appendId

112− :: forall proxy l r

113− . proxy l

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

115− -> r

116−appendId = unsafeCoerce id

117−

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

119100

120101type IndexOfMay a s = IndexOfMay' Z a s

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

168149 SubList '[] bs = ()

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

170151

171−subListId

172− :: forall proxy l r

173− . proxy l

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

175−subListId _ = unsafeCoerce id

176−

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

178153 NotSubList '[] bs = ()

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

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

213188-- taken from first list

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

215190

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−

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

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

224193 (() :: Constraint)

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

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

1−module TypeFun.Data.Maybe

2− ( MaybeCase

3− , NothingToConstr

4− , JustToConstr

5− , CatMaybes

6− , FromJust

7− ) where

1+module TypeFun.Data.Maybe where

93import GHC.Exts

104

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

148 MaybeCase 'Nothing nothing just = nothing

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

1610

11+

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

1813 NothingToConstr 'Nothing c = c

1914 NothingToConstr ('Just a) c = ()

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

2217 JustToConstr 'Nothing c = ()

2318 JustToConstr ('Just a) c = c

2419

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

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

2721 CatMaybes '[] = '[]

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

src/TypeFun/Data/Peano.hs+4−22

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

1−module TypeFun.Data.Peano

2− ( N(..)

3− , KnownPeano(..)

4− , ToNat

5− , FromNat

6− , (:+:)

7− , (:-:)

8− , (:*:)

9− ) where

1+module TypeFun.Data.Peano where

102

11−import Data.Typeable

12−import GHC.Generics (Generic)

13−import GHC.TypeLits

3+import Data.Typeable

4+import GHC.Generics (Generic)

5+import GHC.TypeLits

146

157data N = Z | S N

168 deriving ( Eq, Ord, Read, Show

179 , Generic, Typeable )

1810

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−

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

3012 ToNat Z = 0

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

14name: type-fun

2−version: 0.1.2

5+version: 0.0.1

36synopsis: Collection of widely reimplemented type families

7+-- description:

48license: BSD3

59license-file: LICENSE

610author: Aleksey Uimanov

711maintainer: s9gf4ult@gmail.com

12+-- copyright:

813category: Dependent Types

914build-type: Simple

10−extra-source-files: CHANGELOG.md

15+-- extra-source-files:

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

1617

1718library

1819 default-language: Haskell2010

1920 hs-source-dirs: src

2021 default-extensions: ConstraintKinds

2122 , DataKinds

22− , DeriveDataTypeable

2323 , DeriveGeneric

2424 , FlexibleInstances

2525 , MultiParamTypeClasses

2626 , PolyKinds

27− , RankNTypes

28− , ScopedTypeVariables

2927 , TypeFamilies

3028 , TypeOperators

3129 , UndecidableInstances

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

3634 , TypeFun.Data.Maybe

3735 , TypeFun.Data.Peano

3836

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

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

38+

4039

4140test-suite example

4241 type: exitcode-stdio-1.0

4342 default-language: Haskell2010

4443 hs-source-dirs: example

4544 main-is: Main.hs

46− default-extensions: ConstraintKinds

47− , DataKinds

45+ default-extensions: DataKinds

4846 , GADTs

4947 , TemplateHaskell

5048 , TypeFamilies