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-Na... 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 mailto:oleg.grenrus@iki.fi>:

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.