# ANN: fin and vec

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.

## #Similar other packages

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

• fixed-vector

• 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`.

## #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

Site proudly generated by Hakyll