I'm happy to announce two packages:
- http://hackage.haskell.org/package/fin - http://hackage.haskell.org/package/vec In short they provide following types: data Nat where Z | S Nat data Fin (n :: Nat) where Z :: Fin ('S n) S :: Fin n -> Fin ('S n) data Vec (n :: Nat) a where VNil :: Vec 'Z a (:::) :: a -> Vec n a -> Vec ('S n) a Main motivation for creating these packages is that I didn't found anything similar on Hackage. Before comparison with the alternatives, let me mention few highlights: - `fin` and `vec` support GHC-7.8.4 .. GHC-8.2.1; and I plan to keep support window as wide as possible. - `fin` package provides `Data.Fin.Enum` module to work generically with enumerations. It's (subjectively) more ergonomic than working with `All ((:~:) a) xs => NS I xs` from `generics-sop` [1] - `fin` package defines `InlineInduction` class, letting us trick GHC to unfold recursion. One general example is unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where start :: Fix 'Z a start = Fix fix step :: Fix m a -> Fix ('S m) a step (Fix go) = Fix $ \f -> f (go f) newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a } So, for statically known @n@, GHC's inliner will "simplify": unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f))) - `fin` has very light dependency footprint: `base`, `deepseq`, `hashable` (and transitively `text`) on GHC>=8.0 - `vec` has a little more dependencies, essentially `lens`. See dependency diagram in the readme. [2] - `vec` comes in three 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 * __inline__: which uses `InlineInduction`, unrolling recursion if the size of 'Vec' is known statically. Differences with other packages ------------------------------- ### fin - [type-natural](http://hackage.haskell.org/package/type-natural) depends on @singletons@ package. `fin` will try to stay light on the dependencies, and support as many GHC versions as practical. - [peano](http://hackage.haskell.org/package/peano) is very incomplete - [nat](http://hackage.haskell.org/package/nat) as well. - [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses) doesn't use @DataKinds@. - [type-combinators](http://hackage.haskell.org/package/type-combinators) is a big package. ### vec - [linear](http://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@). - [sized-vector](http://hackage.haskell.org/package/sized-vector) depends on 'singletons' package. `vec` isn't light on dependencies either, but try to provide wide GHC support. - [sized](https://hackage.haskell.org/package/sized) also depends on a 'singletons' package. The 'Sized f n a' type is generalisation of linears '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'. Disclaimer ---------- These are the "first released versions", i.e. `fin-0` and `vec-0`. Don't be fooled by 0, we use them in production. We don't have (yet?) a use-case where proper full inlining would matter, it seems to work with simple examples. The `vec` package includes simple dot product benchmark, it gives sensible results: - *list* version sets the baseline, built-in fusion seems to kick in. - using `vector` is 3x slower (?) - naive `Vec` is even slower, not surprisingly - `Data.Vec.Pull` approach is slower, *except* - that without conversions it's up to speed with `vector` - `InlineInduction` is *fastest*. Acknowledgements ---------------- - *APLicative Programming with Naperian Functors* [3] has the very similar `Nat`, `Fin` and `Vec` (sections 2--4). I spotted few missing functions in `vec` by re-reading the paper (`vgroup` is `chunks` and `viota` is `universe`). I don't claim that my library is novel in any kind :) - I learned *Pull array* idea from Josef Svenningsson talk at SmallFP 2017 [4]. See the video [5] if interested. - Herbert Valerio Riedel for the idea to split `fin` out of `vec`. It turned out to be very light package. - Andres Löh for discussions about `generics-sop` [1], and about the static inlining idea. - Joachim Breitner for creating `inspection-testing` [6], which really helps validating optimisations working. Cheers, Oleg - [1] http://hackage.haskell.org/package/generics-sop - [2] https://github.com/phadej/vec#dependencies - [3] https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf - [4] http://clojutre.org/2017/ - [5] https://www.youtube.com/watch?v=5PZh0BcjIbY&list=PLetHPRQvX4a9uUK2JUZrgjtC_x4CeNLtN&index=5 - [6] http://hackage.haskell.org/package/inspection-testing _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. signature.asc (836 bytes) Download Attachment |
I wrote a package not long ago which also uses static inlining for similar things: https://hackage. There is also https://hackage.haskell. 2017-11-21 17:27 GMT+05:00 Oleg Grenrus <[hidden email]>: I'm happy to announce two packages: _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Oleg Grenrus
Thanks for more references! I was quite sure I didn't found all packages
around fin/nat/vec (and I feel a little bad for making "standards" problem worse :) - https://hackage.haskell.org/package/finite-typelits uses GHC.TypeLits.Nat (fair thing to do). - https://hackage.haskell.org/package/vector-sized builds on top of that and looks like a nice package too! I dislike GHC.TypeLits.Nat for doing induction over, yet for many things they (+ [1,2] or [3]) are great. I have to write that down in the description of the package(s). Hopefully the approaches: compiler built-in magic and DataKinds definition would be unified in the future. Cheers, Oleg. - [1] https://hackage.haskell.org/package/ghc-typelits-natnormalise - [2] https://hackage.haskell.org/package/ghc-typelits-extra - [3] http://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint-Nat.html On 21.11.2017 15:20, Alexey Vagarenko wrote: > I wrote a package not long ago which also uses static inlining for > similar things: https://hackage.haskell.org/package/static-tensor > > There is also https://hackage.haskell.org/package/vector-sized which > is a wrapper around 'vector' library. > > <http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> > Virus-free. www.avg.com > <http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> > > > > 2017-11-21 17:27 GMT+05:00 Oleg Grenrus <[hidden email] > <mailto:[hidden email]>>: > > I'm happy to announce two packages: > > - http://hackage.haskell.org/package/fin > <http://hackage.haskell.org/package/fin> > - http://hackage.haskell.org/package/vec > <http://hackage.haskell.org/package/vec> > > In short they provide following types: > > data Nat where Z | S Nat > > data Fin (n :: Nat) where > Z :: Fin ('S n) > S :: Fin n -> Fin ('S n) > > data Vec (n :: Nat) a where > VNil :: Vec 'Z a > (:::) :: a -> Vec n a -> Vec ('S n) a > > Main motivation for creating these packages is that I didn't found > anything > similar on Hackage. Before comparison with the alternatives, let me > mention few > highlights: > > - `fin` and `vec` support GHC-7.8.4 .. GHC-8.2.1; and I plan to > keep support > window as wide as possible. > > - `fin` package provides `Data.Fin.Enum` module to work > generically with > enumerations. It's (subjectively) more ergonomic than working with > `All ((:~:) a) xs => NS I xs` from `generics-sop` [1] > > - `fin` package defines `InlineInduction` class, > letting us trick GHC to unfold recursion. One general example is > > unfoldedFix :: forall n a proxy. InlineInduction n > => proxy n -> (a -> a) -> a > unfoldedFix _ = getFix (inlineInduction1 start step :: Fix > n a) > where > start :: Fix 'Z a > start = Fix fix > > step :: Fix m a -> Fix ('S m) a > step (Fix go) = Fix $ \f -> f (go f) > > newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a } > > So, for statically known @n@, GHC's inliner will "simplify": > > unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f))) > > - `fin` has very light dependency footprint: > `base`, `deepseq`, `hashable` (and transitively `text`) on GHC>=8.0 > > - `vec` has a little more dependencies, essentially `lens`. See > dependency > diagram in the readme. [2] > > - `vec` comes in three 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 > > * __inline__: which uses `InlineInduction`, unrolling > recursion if the size of 'Vec' is known statically. > > Differences with other packages > ------------------------------- > > ### fin > > - [type-natural](http://hackage.haskell.org/package/type-natural > <http://hackage.haskell.org/package/type-natural>) depends > on @singletons@ package. `fin` will try to stay light on the > dependencies, > and support as many GHC versions as practical. > > - [peano](http://hackage.haskell.org/package/peano > <http://hackage.haskell.org/package/peano>) is very incomplete > > - [nat](http://hackage.haskell.org/package/nat > <http://hackage.haskell.org/package/nat>) as well. > > - > [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses > <https://hackage.haskell.org/package/PeanoWitnesses>) > doesn't use @DataKinds@. > > - > [type-combinators](http://hackage.haskell.org/package/type-combinators > <http://hackage.haskell.org/package/type-combinators>) > is a big package. > > ### vec > > - [linear](http://hackage.haskell.org/package/linear > <http://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@). > > - [sized-vector](http://hackage.haskell.org/package/sized-vector > <http://hackage.haskell.org/package/sized-vector>) depends > on 'singletons' package. `vec` isn't light on dependencies either, > but try to provide wide GHC support. > > - [sized](https://hackage.haskell.org/package/sized > <https://hackage.haskell.org/package/sized>) also depends > on a 'singletons' package. The 'Sized f n a' type is > generalisation of > linears 'V' for any 'ListLike'. > > - > [clash-prelude](https://hackage.haskell.org/package/clash-prelude > <https://hackage.haskell.org/package/clash-prelude>) > is a kitchen sink package, which has 'CLaSH.Sized.Vector' module. > Also depends on 'singletons'. > > Disclaimer > ---------- > > These are the "first released versions", i.e. `fin-0` and `vec-0`. > Don't be fooled by 0, we use them in production. > > We don't have (yet?) a use-case where proper full inlining would > matter, it > seems to work with simple examples. The `vec` package includes > simple dot > product benchmark, it gives sensible results: > > - *list* version sets the baseline, built-in fusion seems to kick in. > - using `vector` is 3x slower (?) > - naive `Vec` is even slower, not surprisingly > - `Data.Vec.Pull` approach is slower, *except* > - that without conversions it's up to speed with `vector` > - `InlineInduction` is *fastest*. > > Acknowledgements > ---------------- > > - *APLicative Programming with Naperian Functors* [3] has the very > similar > `Nat`, `Fin` and `Vec` (sections 2--4). I spotted few missing > functions in > `vec` by re-reading the paper (`vgroup` is `chunks` and `viota` is > `universe`). > I don't claim that my library is novel in any kind :) > - I learned *Pull array* idea from Josef Svenningsson talk at SmallFP > 2017 [4]. > See the video [5] if interested. > - Herbert Valerio Riedel for the idea to split `fin` out of `vec`. > It turned > out to be very light package. > - Andres Löh for discussions about `generics-sop` [1], and about > the static > inlining idea. > - Joachim Breitner for creating `inspection-testing` [6], which > really helps > validating optimisations working. > > Cheers, > Oleg > > > - [1] http://hackage.haskell.org/package/generics-sop > <http://hackage.haskell.org/package/generics-sop> > - [2] https://github.com/phadej/vec#dependencies > <https://github.com/phadej/vec#dependencies> > - [3] > https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf > <https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf> > - [4] http://clojutre.org/2017/ > - [5] > https://www.youtube.com/watch?v=5PZh0BcjIbY&list=PLetHPRQvX4a9uUK2JUZrgjtC_x4CeNLtN&index=5 > <https://www.youtube.com/watch?v=5PZh0BcjIbY&list=PLetHPRQvX4a9uUK2JUZrgjtC_x4CeNLtN&index=5> > - [6] http://hackage.haskell.org/package/inspection-testing > <http://hackage.haskell.org/package/inspection-testing> > > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > <http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe> > Only members subscribed via the mailman list are allowed to post. > > _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. signature.asc (836 bytes) Download Attachment |
Oleg Grenrus <[hidden email]> writes:
> Thanks for more references! I was quite sure I didn't found all packages > around fin/nat/vec (and I feel a little bad for making "standards" > problem worse :) > There is also https://hackage.haskell.org/package/fixed-vector which I've been using for this sort of thing. -- - Frank _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |