Oleg's gists — Archive

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

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

This work is licensed under a “CC BY SA 4.0” license.
Oleg's gists — Archive

twitter github email linkedin stackoverflow

Site proudly generated by Hakyll