git.iko.soy/type-fun
on 8832366 help sign in
a90d4b7
swap
0 ahead, 17 behind
8 files changed+13−88
since splitsnapshots
unifiedsplit
.gitignore−1 CHANGELOG.md−15 example/Main.hs−1 src/TypeFun/Data/List.hs−24 src/TypeFun/Data/Peano.hs+3−14 stack.yaml−9 stack.yaml.lock−12 type-fun.cabal+10−12
.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−24
@@ -35,14 +35,10 @@ module TypeFun.Data.List
3535 , UnionList
3636 , AppendUniq
3737 , Intersect
38− , Substract
3938 -- * Uniqueness checking
4039 , ElementIsUniq
4140 , UniqElements
4241 , UniqElements'
43− -- * Unsafe helpers
44− , appendId
45− , subListId
4642 ) where
4743
4844import Data.Type.Bool
@@ -51,7 +47,6 @@ import GHC.TypeLits
5147import TypeFun.Data.Eq
5248import TypeFun.Data.Maybe
5349import TypeFun.Data.Peano
54−import Unsafe.Coerce
5550
5651------------------------------------------------------------------------
5752-- NOTE: Errors type classes. These type classes are not in separate --
@@ -108,13 +103,6 @@ type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
108103 '[] :++: b = b
109104 (a ': as) :++: b = a ': (as :++: b)
110105
111−appendId
112− :: forall proxy l r
113− . proxy l
114− -> (l ~ (l :++: '[]) => r)
115− -> r
116−appendId = unsafeCoerce id
117−
118106type IndexOf a s = FromJust (IndexOfMay a s)
119107
120108type IndexOfMay a s = IndexOfMay' Z a s
@@ -168,12 +156,6 @@ type family SubList (a :: [k]) (b :: [k]) :: Constraint where
168156 SubList '[] bs = ()
169157 SubList (a ': as) bs = (Elem a bs, SubList as bs)
170158
171−subListId
172− :: forall proxy l r
173− . proxy l
174− -> (SubList l l => r) -> r
175−subListId _ = unsafeCoerce id
176−
177159type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
178160 NotSubList '[] bs = ()
179161 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
@@ -213,12 +195,6 @@ type family AppendUniq (a :: k) (s :: [k]) :: [k] where
213195-- taken from first list
214196type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
215197
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−
222198-- | Checks that element 'a' occurs in a list just once
223199type ElementIsUniq a s = If (Equal (S Z) (Count a s))
224200 (() :: Constraint)
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+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+
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