git.iko.soy/type-fun
on 77cb83c help sign in
a90d4b7
swap
0 ahead, 15 behind
8 files changed+7−76
since splitsnapshots
unifiedsplit
.gitignore−1 CHANGELOG.md−15 example/Main.hs−1 src/TypeFun/Data/List.hs−17 src/TypeFun/Data/Peano.hs+3−14 stack.yaml−9 stack.yaml.lock−12 type-fun.cabal+4−7
.gitignore−1
@@ -2,4 +2,3 @@ dist
22TAGS
33.cabal-sandbox
44cabal.sandbox.config
5−.stack-work
CHANGELOG.md−15
@@ -4,20 +4,5 @@
44
55# CHANGELOG
66
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−
227## 0.0.1
238First 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/Data/List.hs−17
@@ -40,9 +40,6 @@ module TypeFun.Data.List
4040 , ElementIsUniq
4141 , UniqElements
4242 , UniqElements'
43− -- * Unsafe helpers
44− , appendId
45− , subListId
4643 ) where
4744
4845import Data.Type.Bool
@@ -51,7 +48,6 @@ import GHC.TypeLits
5148import TypeFun.Data.Eq
5249import TypeFun.Data.Maybe
5350import TypeFun.Data.Peano
54−import Unsafe.Coerce
5551
5652------------------------------------------------------------------------
5753-- NOTE: Errors type classes. These type classes are not in separate --
@@ -108,13 +104,6 @@ type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
108104 '[] :++: b = b
109105 (a ': as) :++: b = a ': (as :++: b)
110106
111−appendId
112− :: forall proxy l r
113− . proxy l
114− -> (l ~ (l :++: '[]) => r)
115− -> r
116−appendId = unsafeCoerce id
117−
118107type IndexOf a s = FromJust (IndexOfMay a s)
119108
120109type IndexOfMay a s = IndexOfMay' Z a s
@@ -168,12 +157,6 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
168157 SubList '[] bs = ()
169158 SubList (a ': as) bs = (Elem a bs, SubList as bs)
170159
171−subListId
172− :: forall proxy l r
173− . proxy l
174− -> (SubList l l => r) -> r
175−subListId _ = unsafeCoerce id
176−
177160type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
178161 NotSubList '[] bs = ()
179162 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
src/TypeFun/Data/Peano.hs+3−14
@@ -1,6 +1,5 @@
11module TypeFun.Data.Peano
22 ( N(..)
3− , KnownPeano(..)
43 , ToNat
54 , FromNat
65 , (:+:)
@@ -8,24 +7,14 @@ module TypeFun.Data.Peano
87 , (:*:)
98 ) where
109
11−import Data.Typeable
12−import GHC.Generics (Generic)
13−import GHC.TypeLits
10+import Data.Typeable
11+import GHC.Generics (Generic)
12+import GHC.TypeLits
1413
1514data N = Z | S N
1615 deriving ( Eq, Ord, Read, Show
1716 , Generic, Typeable )
1817
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−
2918type family ToNat (a :: N) :: Nat where
3019 ToNat Z = 0
3120 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+4−7
@@ -1,5 +1,5 @@
11name: type-fun
2−version: 0.1.2
2+version: 0.0.1
33synopsis: Collection of widely reimplemented type families
44license: BSD3
55license-file: LICENSE
@@ -19,13 +19,10 @@ library
1919 hs-source-dirs: src
2020 default-extensions: ConstraintKinds
2121 , DataKinds
22− , DeriveDataTypeable
2322 , DeriveGeneric
2423 , FlexibleInstances
2524 , MultiParamTypeClasses
2625 , PolyKinds
27− , RankNTypes
28− , ScopedTypeVariables
2926 , TypeFamilies
3027 , TypeOperators
3128 , UndecidableInstances
@@ -36,15 +33,15 @@ library
3633 , TypeFun.Data.Maybe
3734 , TypeFun.Data.Peano
3835
39− build-depends: base >= 4.7 && < 5
36+ build-depends: base >=4.7 && <4.9
37+
4038
4139test-suite example
4240 type: exitcode-stdio-1.0
4341 default-language: Haskell2010
4442 hs-source-dirs: example
4543 main-is: Main.hs
46− default-extensions: ConstraintKinds
47− , DataKinds
44+ default-extensions: DataKinds
4845 , GADTs
4946 , TemplateHaskell
5047 , TypeFamilies