Posted on 2017-11-21
by Oleg Grenrus
packages

I'm happy to announce two packages:

In short they provide following types:

```
-- Natural numbers
data Nat where Z | S Nat
-- Finite numbers
data Fin (n :: Nat) where
Z :: Fin ('S n)
S :: Fin n -> Fin ('S n)
-- Length indexed (sized) list
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.

See Hasochism: the pleasure and pain of dependently typed haskell programming by Sam Lindley and Conor McBride for answers to /how/ and /why/. Read APLicative Programming with Naperian Functors by Jeremy Gibbons for (not so) different ones.

### fin

finite-typelits Is a great package, but uses

`GHC.TypeLits`

.type-natural depends on

`singletons`

package.`fin`

will try to stay light on the dependencies, and support as many GHC versions as practical.peano is very incomplete

nat as well.

PeanoWitnesses doesn't use @DataKinds@.

type-combinators is a big package.

### vec

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 Great package using

`GHC.TypeLits`

. Current version (0.6.1.0) uses`finite-typelits`

and`Int`

indexes.sized-vector depends on

`singletons`

package.`vec`

isn't light on dependencies either, but try to provide wide GHC support.sized also depends on a

`singletons`

package. The`Sized f n a`

type is generalisation of linears`V`

for any`ListLike`

.clash-prelude is a kitchen sink package, which has

`CLaSH.Sized.Vector`

module. Also depends on`singletons`

.

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*.

*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

Site proudly generated by Hakyll