[ANN]: fin & vec

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

[ANN]: fin & vec

Oleg Grenrus
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
Reply | Threaded
Open this post in threaded view
|

Re: [ANN]: fin & vec

Alexey Vagarenko
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.

Virus-free. www.avg.com

2017-11-21 17:27 GMT+05:00 Oleg Grenrus <[hidden email]>:
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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: [ANN]: fin & vec

Oleg Grenrus
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
Reply | Threaded
Open this post in threaded view
|

Re: [ANN]: fin & vec

Frank Staals
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.