<div dir="ltr"><span style="font-size:12.8px">I wrote a package not long ago which also uses static inlining for similar things: </span><a href="https://hackage.haskell.org/package/static-tensor" target="_blank" style="font-size:12.8px">https://hackage.<wbr>haskell.org/package/static-<wbr>tensor</a><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">There is also <a href="https://hackage.haskell.org/package/vector-sized" target="_blank">https://hackage.haskell.<wbr>org/package/vector-sized</a> which is a wrapper around 'vector' library.</div></div><div id="DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2"><br>
<table style="border-top:1px solid #d3d4de">
<tr>
<td style="width:55px;padding-top:13px"><a href="http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail" target="_blank"><img src="https://ipmcdn.avast.com/images/icons/icon-envelope-tick-green-avg-v1.png" alt="" width="46" height="29" style="width: 46px; height: 29px;"></a></td>
<td style="width:470px;padding-top:12px;color:#41424e;font-size:13px;font-family:Arial,Helvetica,sans-serif;line-height:18px">Virus-free. <a href="http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail" target="_blank" style="color:#4453ea">www.avg.com</a>
</td>
</tr>
</table><a href="#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2" width="1" height="1"></a></div><div class="gmail_extra"><br><div class="gmail_quote">2017-11-21 17:27 GMT+05:00 Oleg Grenrus <span dir="ltr"><<a href="mailto:oleg.grenrus@iki.fi" target="_blank">oleg.grenrus@iki.fi</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm happy to announce two packages:<br>
<br>
- <a href="http://hackage.haskell.org/package/fin" rel="noreferrer" target="_blank">http://hackage.haskell.org/<wbr>package/fin</a><br>
- <a href="http://hackage.haskell.org/package/vec" rel="noreferrer" target="_blank">http://hackage.haskell.org/<wbr>package/vec</a><br>
<br>
In short they provide following types:<br>
<br>
data Nat where Z | S Nat<br>
<br>
data Fin (n :: Nat) where<br>
Z :: Fin ('S n)<br>
S :: Fin n -> Fin ('S n)<br>
<br>
data Vec (n :: Nat) a where<br>
VNil :: Vec 'Z a<br>
(:::) :: a -> Vec n a -> Vec ('S n) a<br>
<br>
Main motivation for creating these packages is that I didn't found anything<br>
similar on Hackage. Before comparison with the alternatives, let me<br>
mention few<br>
highlights:<br>
<br>
- `fin` and `vec` support GHC-7.8.4 .. GHC-8.2.1; and I plan to keep support<br>
window as wide as possible.<br>
<br>
- `fin` package provides `Data.Fin.Enum` module to work generically with<br>
enumerations. It's (subjectively) more ergonomic than working with<br>
`All ((:~:) a) xs => NS I xs` from `generics-sop` [1]<br>
<br>
- `fin` package defines `InlineInduction` class,<br>
letting us trick GHC to unfold recursion. One general example is<br>
<br>
unfoldedFix :: forall n a proxy. InlineInduction n<br>
=> proxy n -> (a -> a) -> a<br>
unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a)<br>
where<br>
start :: Fix 'Z a<br>
start = Fix fix<br>
<br>
step :: Fix m a -> Fix ('S m) a<br>
step (Fix go) = Fix $ \f -> f (go f)<br>
<br>
newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }<br>
<br>
So, for statically known @n@, GHC's inliner will "simplify":<br>
<br>
unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f)))<br>
<br>
- `fin` has very light dependency footprint:<br>
`base`, `deepseq`, `hashable` (and transitively `text`) on GHC>=8.0<br>
<br>
- `vec` has a little more dependencies, essentially `lens`. See dependency<br>
diagram in the readme. [2]<br>
<br>
- `vec` comes in three flavours:<br>
<br>
* __naive__: with explicit recursion. It's simple, constraint-less,<br>
yet slow.<br>
<br>
* __pull__: using `Fin n -> a` representation, which fuses well,<br>
but makes some programs hard to write. And<br>
<br>
* __inline__: which uses `InlineInduction`, unrolling<br>
recursion if the size of 'Vec' is known statically.<br>
<br>
Differences with other packages<br>
------------------------------<wbr>-<br>
<br>
### fin<br>
<br>
- [type-natural](<a href="http://hackage.haskell.org/package/type-natural" rel="noreferrer" target="_blank">http://hackage.<wbr>haskell.org/package/type-<wbr>natural</a>) depends<br>
on @singletons@ package. `fin` will try to stay light on the dependencies,<br>
and support as many GHC versions as practical.<br>
<br>
- [peano](<a href="http://hackage.haskell.org/package/peano" rel="noreferrer" target="_blank">http://hackage.<wbr>haskell.org/package/peano</a>) is very incomplete<br>
<br>
- [nat](<a href="http://hackage.haskell.org/package/nat" rel="noreferrer" target="_blank">http://hackage.haskell.<wbr>org/package/nat</a>) as well.<br>
<br>
- [PeanoWitnesses](<a href="https://hackage.haskell.org/package/PeanoWitnesses" rel="noreferrer" target="_blank">https://<wbr>hackage.haskell.org/package/<wbr>PeanoWitnesses</a>)<br>
doesn't use @DataKinds@.<br>
<br>
- [type-combinators](<a href="http://hackage.haskell.org/package/type-combinators" rel="noreferrer" target="_blank">http://<wbr>hackage.haskell.org/package/<wbr>type-combinators</a>)<br>
is a big package.<br>
<br>
### vec<br>
<br>
- [linear](<a href="http://hackage.haskell.org/package/linear" rel="noreferrer" target="_blank">http://hackage.<wbr>haskell.org/package/linear</a>) has 'V' type,<br>
which uses 'Vector' from @vector@ package as backing store.<br>
`Vec` is a real GADT, but tries to provide as many useful instances (upto<br>
@lens@).<br>
<br>
- [sized-vector](<a href="http://hackage.haskell.org/package/sized-vector" rel="noreferrer" target="_blank">http://hackage.<wbr>haskell.org/package/sized-<wbr>vector</a>) depends<br>
on 'singletons' package. `vec` isn't light on dependencies either,<br>
but try to provide wide GHC support.<br>
<br>
- [sized](<a href="https://hackage.haskell.org/package/sized" rel="noreferrer" target="_blank">https://hackage.<wbr>haskell.org/package/sized</a>) also depends<br>
on a 'singletons' package. The 'Sized f n a' type is generalisation of<br>
linears 'V' for any 'ListLike'.<br>
<br>
- [clash-prelude](<a href="https://hackage.haskell.org/package/clash-prelude" rel="noreferrer" target="_blank">https://<wbr>hackage.haskell.org/package/<wbr>clash-prelude</a>)<br>
is a kitchen sink package, which has 'CLaSH.Sized.Vector' module.<br>
Also depends on 'singletons'.<br>
<br>
Disclaimer<br>
----------<br>
<br>
These are the "first released versions", i.e. `fin-0` and `vec-0`.<br>
Don't be fooled by 0, we use them in production.<br>
<br>
We don't have (yet?) a use-case where proper full inlining would matter, it<br>
seems to work with simple examples. The `vec` package includes simple dot<br>
product benchmark, it gives sensible results:<br>
<br>
- *list* version sets the baseline, built-in fusion seems to kick in.<br>
- using `vector` is 3x slower (?)<br>
- naive `Vec` is even slower, not surprisingly<br>
- `Data.Vec.Pull` approach is slower, *except*<br>
- that without conversions it's up to speed with `vector`<br>
- `InlineInduction` is *fastest*.<br>
<br>
Acknowledgements<br>
----------------<br>
<br>
- *APLicative Programming with Naperian Functors* [3] has the very similar<br>
`Nat`, `Fin` and `Vec` (sections 2--4). I spotted few missing functions in<br>
`vec` by re-reading the paper (`vgroup` is `chunks` and `viota` is<br>
`universe`).<br>
I don't claim that my library is novel in any kind :)<br>
- I learned *Pull array* idea from Josef Svenningsson talk at SmallFP<br>
2017 [4].<br>
See the video [5] if interested.<br>
- Herbert Valerio Riedel for the idea to split `fin` out of `vec`. It turned<br>
out to be very light package.<br>
- Andres Löh for discussions about `generics-sop` [1], and about the static<br>
inlining idea.<br>
- Joachim Breitner for creating `inspection-testing` [6], which really helps<br>
validating optimisations working.<br>
<br>
Cheers,<br>
Oleg<br>
<br>
<br>
- [1] <a href="http://hackage.haskell.org/package/generics-sop" rel="noreferrer" target="_blank">http://hackage.haskell.org/<wbr>package/generics-sop</a><br>
- [2] <a href="https://github.com/phadej/vec#dependencies" rel="noreferrer" target="_blank">https://github.com/phadej/vec#<wbr>dependencies</a><br>
- [3]<br>
<a href="https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf" rel="noreferrer" target="_blank">https://www.cs.ox.ac.uk/<wbr>people/jeremy.gibbons/<wbr>publications/aplicative.pdf</a><br>
- [4] <a href="http://clojutre.org/2017/" rel="noreferrer" target="_blank">http://clojutre.org/2017/</a><br>
- [5]<br>
<a href="https://www.youtube.com/watch?v=5PZh0BcjIbY&list=PLetHPRQvX4a9uUK2JUZrgjtC_x4CeNLtN&index=5" rel="noreferrer" target="_blank">https://www.youtube.com/watch?<wbr>v=5PZh0BcjIbY&list=<wbr>PLetHPRQvX4a9uUK2JUZrgjtC_<wbr>x4CeNLtN&index=5</a><br>
- [6] <a href="http://hackage.haskell.org/package/inspection-testing" rel="noreferrer" target="_blank">http://hackage.haskell.org/<wbr>package/inspection-testing</a><br>
<br>
<br>
<br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br></div>