37a5192...master · type-fun

git.iko.soy/type-fun

8 files changed+58−8

since splitsnapshots

unifiedsplit

.gitignore+1 CHANGELOG.md+15 example/Main.hs+1 src/TypeFun/Data/List.hs+1−1 src/TypeFun/Data/Peano.hs+14−3 stack.yaml+9 stack.yaml.lock+12 type-fun.cabal+5−4

.gitignore+1

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

22TAGS

33.cabal-sandbox

44cabal.sandbox.config

5+.stack-work

CHANGELOG.md+15

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

55# CHANGELOG

7+## 0.1.2

8+### Added KnownPeano

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+

722## 0.0.1

823First version

example/Main.hs+1

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

3737 print $ prefixConstr p2

3838 print $ prefixConstr p3

3939 print $ uniqConstr p2

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

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

src/TypeFun/Data/List.hs+1−1

@@ -40,7 +40,7 @@ module TypeFun.Data.List

4040 , ElementIsUniq

4141 , UniqElements

4242 , UniqElements'

43− -- * Helpers

43+ -- * Unsafe helpers

4444 , appendId

4545 , subListId

4646 ) where

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

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

11module TypeFun.Data.Peano

22 ( N(..)

3+ , KnownPeano(..)

34 , ToNat

45 , FromNat

56 , (:+:)

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

78 , (:*:)

89 ) where

910

10−import Data.Typeable

11−import GHC.Generics (Generic)

12−import GHC.TypeLits

11+import Data.Typeable

12+import GHC.Generics (Generic)

13+import GHC.TypeLits

1314

1415data N = Z | S N

1516 deriving ( Eq, Ord, Read, Show

1617 , Generic, Typeable )

1718

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+

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

1930 ToNat Z = 0

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

stack.yamlnew file+9

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

1+nix:

2+ packages:

3+ - zlib

4+ - postgresql

6+resolver: lts-13.21

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

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

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

11name: type-fun

2−version: 0.0.1

2+version: 0.1.2

33synopsis: Collection of widely reimplemented type families

44license: BSD3

55license-file: LICENSE

@@ -19,6 +19,7 @@ library

1919 hs-source-dirs: src

2020 default-extensions: ConstraintKinds

2121 , DataKinds

22+ , DeriveDataTypeable

2223 , DeriveGeneric

2324 , FlexibleInstances

2425 , MultiParamTypeClasses

@@ -35,15 +36,15 @@ library

3536 , TypeFun.Data.Maybe

3637 , TypeFun.Data.Peano

3738

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

39−

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

4040

4141test-suite example

4242 type: exitcode-stdio-1.0

4343 default-language: Haskell2010

4444 hs-source-dirs: example

4545 main-is: Main.hs

46− default-extensions: DataKinds

46+ default-extensions: ConstraintKinds

47+ , DataKinds

4748 , GADTs

4849 , TemplateHaskell

4950 , TypeFamilies