cabal-version: >=1.10 name: vec version: 0.1.1.1 synopsis: Vec: length-indexed (sized) list category: Data, Dependent Types description: This package provides length-indexed (sized) lists, also known as vectors. . @ data Vec n a where \ VNil :: Vec 'Nat.Z a \ (:::) :: a -> Vec n a -> Vec ('Nat.S n) a @ . The functions are implemented in four flavours: . * __naive__: with explicit recursion. It's simple, constraint-less, yet slow. . * __pull__: using @Fin n -> a@ representation, which fuses well, but makes some programs hard to write. And . * __data-family__: which allows lazy pattern matching . * __inline__: which exploits how GHC dictionary inlining works, unrolling recursion if the size of 'Vec' is known statically. . As best approach depends on the application, @vec@ doesn't do any magic transformation. Benchmark your code. . This package uses [fin](https://hackage.haskell.org/package/fin), i.e. not @GHC.TypeLits@, for indexes. . See [Hasochism: the pleasure and pain of dependently typed haskell programming](https://doi.org/10.1145/2503778.2503786) by Sam Lindley and Conor McBride for answers to /how/ and /why/. Read [APLicative Programming with Naperian Functors](https://doi.org/10.1007/978-3-662-54434-1_21) by Jeremy Gibbons for (not so) different ones. . === Similar packages . * [linear](https://hackage.haskell.org/package/linear) has 'V' type, which uses 'Vector' from @vector@ package as backing store. @Vec@ is a real GADT, but tries to provide as many useful instances (upto @lens@). . * [vector-sized](https://hackage.haskell.org/package/vector-sized) Great package using @GHC.TypeLits@. Current version (0.6.1.0) uses @finite-typelits@ and @Int@ indexes. . * [sized-vector](https://hackage.haskell.org/package/sized-vector) depends on @singletons@ package. @vec@ isn't light on dependencies either, but try to provide wide GHC support. . * [fixed-vector](https://hackage.haskell.org/package/fixed-vector) . * [sized](https://hackage.haskell.org/package/sized) also depends on a @singletons@ package. The @Sized f n a@ type is generalisation of @linear@'s @V@ for any @ListLike@. . * [clash-prelude](https://hackage.haskell.org/package/clash-prelude) is a kitchen sink package, which has @CLaSH.Sized.Vector@ module. Also depends on @singletons@. homepage: https://github.com/phadej/vec bug-reports: https://github.com/phadej/vec/issues license: BSD3 license-file: LICENSE author: Oleg Grenrus maintainer: Oleg.Grenrus copyright: (c) 2017-2019 Oleg Grenrus build-type: Simple extra-source-files: ChangeLog.md tested-with: GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 source-repository head type: git location: https://github.com/phadej/vec.git library exposed-modules: Data.Vec.DataFamily.SpineStrict Data.Vec.DataFamily.SpineStrict.Pigeonhole Data.Vec.Lazy Data.Vec.Lazy.Inline Data.Vec.Pull other-modules: Data.Functor.Confusing build-depends: adjunctions >=4.4 && <4.5 , base >=4.7 && <4.13 , base-compat >=0.9.3 && <0.11 , deepseq >=1.3.0.2 && <1.5 , distributive >=0.5.3 && <0.7 , fin >=0.1 && <0.2 , hashable >=1.2.7.0 && <1.4 , lens >=4.16 && <4.18 , semigroupoids >=5.2.2 && <5.4 , transformers >=0.3.0.0 && <0.6 if !impl(ghc >=8.0) build-depends: semigroups >=0.18.4 && <0.20 ghc-options: -Wall -fprint-explicit-kinds hs-source-dirs: src other-extensions: CPP FlexibleContexts GADTs TypeOperators default-language: Haskell2010 test-suite inspection type: exitcode-stdio-1.0 main-is: Main.hs other-modules: Inspection Inspection.DataFamily.SpineStrict Inspection.DataFamily.SpineStrict.Pigeonhole ghc-options: -Wall -fprint-explicit-kinds hs-source-dirs: test default-language: Haskell2010 build-depends: base , fin , inspection-testing >=0.2.0.1 && <0.5 , tagged , vec if !impl(ghc >=8.0) buildable: False benchmark bench type: exitcode-stdio-1.0 main-is: Bench.hs ghc-options: -Wall -fprint-explicit-kinds hs-source-dirs: bench default-language: Haskell2010 other-modules: DotProduct build-depends: base , criterion >=1.4.0.0 && <1.6 , fin , vec , vector