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:
vector
is 3x slower (?)Vec
is even slower, not surprisinglyData.Vec.Pull
approach is slower, exceptvector
InlineInduction
is fastest.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 :)fin
out of vec
. It turned out to be very light package.generics-sop
[1], and about the static inlining idea.inspection-testing
[6], which really helps validating optimisations working.Cheers, Oleg