type-list 0.2.0.0 → 0.5.0.0
raw patch · 4 files changed
Files
- README.md +2/−0
- changelog.md +21/−0
- src/Data/Type/List.hs +26/−5
- type-list.cabal +18/−10
+ README.md view
@@ -0,0 +1,2 @@+# type-list+Common list and tuple operations rewritten as type families that operate in the type level, on data-kinded types. Both uncurried (type family) and curried (GADTs to be used with the Apply type family from Singletons) are provided, to work around the inability to partially apply type families.
+ changelog.md view
@@ -0,0 +1,21 @@+0.3.0.0+------++* Added ZipWith family.++0.2.0.0+-------++* Added lengthVal function, replacing the functionality of the removed TypeLength typeclass together with the Length family.++0.1.0.0+-------++* Changed TypeLength type class to a Length family.+* Fixed Intersection.++0.0.0.0+------++* Initial commit.+
src/Data/Type/List.hs view
@@ -26,7 +26,6 @@ import GHC.TypeLits import Data.Type.Bool-import Data.Type.Equality import Data.Singletons -- |Maps a curried type function over a type list.@@ -43,11 +42,31 @@ type instance Apply Map'' f = Map' f type instance Apply (Map' f) l = Map f l +-- |Zip two list with a curried two-argument type function.+type family ZipWith (f :: TyFun a (TyFun b c -> *) -> *) (xs :: [a]) (ys :: [b]) where+ ZipWith f '[] '[] = '[]+ ZipWith f (x ': xs) (y ': ys) = (Apply (Apply f x) y) ': ZipWith f xs ys++data ZipWith''' :: TyFun (TyFun a (TyFun b c -> *) -> *) (TyFun [a] (TyFun [b] [c] -> *) -> *) -> * where+ ZipWith''' :: ZipWith''' f++data ZipWith'' :: (TyFun a (TyFun b c -> *) -> *) -> TyFun [a] (TyFun [b] [c] -> *) -> * where+ ZipWith'' :: ZipWith'' f xs++data ZipWith' :: (TyFun a (TyFun b c -> *) -> *) -> [a] -> TyFun [b] [c] -> * where+ ZipWith' :: ZipWith' f xs ys++type instance Apply ZipWith''' f = ZipWith'' f+type instance Apply (ZipWith'' f) xs = ZipWith' f xs+type instance Apply (ZipWith' f xs) ys = ZipWith f xs ys++-- | Length of a type-level list, as a type-level natural number. type family Length xs where Length '[] = 0 Length (x ': xs) = 1 + (Length xs) lengthVal :: forall sing xs. KnownNat (Length xs) => sing xs -> Integer+-- ^Length of a type-level list, as an integer. lengthVal _ = natVal (undefined :: proxy (Length xs)) data Length' :: TyFun [a] Nat -> * where@@ -99,6 +118,7 @@ type instance Apply Remove'' x = Remove' x type instance Apply (Remove' x) xs = Remove x xs +-- |Set difference over type lists. type family Difference xs ys where Difference '[] ys = ys Difference (x ': xs) ys = Remove x (Difference xs ys)@@ -112,10 +132,12 @@ type instance Apply Difference'' xs = Difference' xs type instance Apply (Difference' xs) ys = Difference xs ys +-- |Helper type family for 'Reverse'. type family ReverseAcc xs acc where ReverseAcc '[] acc = acc ReverseAcc (x ': xs) acc = ReverseAcc xs (x ': acc) +-- |Reverse a type-level list. type family Reverse xs where Reverse xs = ReverseAcc xs '[] @@ -126,8 +148,8 @@ -- | Type list membership test. type family Find x ys where- Find x '[] = False- Find x (x ': ys) = True+ Find x '[] = 'False+ Find x (x ': ys) = 'True Find x (y ': ys) = Find x ys data Find'' :: TyFun k (TyFun [k] Bool -> *) -> * where@@ -156,7 +178,7 @@ -- |Test if two list do not contain any equal elements. type family Distinct xs ys where- Distinct '[] '[] = False+ Distinct '[] '[] = 'False Distinct (x ': xs) (x ': ys) = Distinct xs ys Distinct (x ': xs) (y ': ys) = Not (Find x (y ': ys)) && Distinct xs ys @@ -234,5 +256,4 @@ Swap' :: Swap' f type instance Apply Swap' '(a,b) = Swap '(a,b)-
type-list.cabal view
@@ -1,28 +1,36 @@--- Initial type-list.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/- name: type-list-version: 0.2.0.0+version: 0.5.0.0 synopsis: Operations on type-level lists and tuples. description: Operations on type-level lists and tuples, together with their curried versions. license: BSD3 license-file: LICENSE author: Marcin Mrotek maintainer: marcin.jan.mrotek@gmail.com--- copyright: +copyright: (c) Marcin Mrotek, 2015 category: Data build-type: Simple--- extra-source-files: +extra-source-files: README.md changelog.md+tested-with: GHC == 7.8.4+ , GHC == 7.10.1+ , GHC == 7.10.2+ , GHC == 8.0.1 cabal-version: >=1.10 source-repository head type: git location: https://github.com/marcinmrotek/type-list +flag devel+ description: "Development mode (-Werror)"+ default: False+ manual: True+ library exposed-modules: Data.Type.List- -- other-modules: - -- other-extensions: - build-depends: base >=4.7 && <4.9- ,singletons >= 1.0 && < 1.2+ build-depends: base >=4.7 && < 6+ ,singletons >= 1.0 && < 2.3 hs-source-dirs: src default-language: Haskell2010+ ghc-options: -Wall + if flag(devel)+ ghc-options: -Werror+