21 Jul 04:43 2013

## ANN: data-fin

wren ng thornton <wren <at> freegeek.org>

2013-07-21 02:43:26 GMT

2013-07-21 02:43:26 GMT

-------------------------------------------- -- data-fin 0.1.0 -------------------------------------------- The data-fin package offers the family of totally ordered finite sets, implemented as newtypes of Integer, etc. Thus, you get all the joys of: data Nat = Zero | Succ !Nat data Fin :: Nat -> * where FZero :: (n::Nat) -> Fin (Succ n) FSucc :: (n::Nat) -> Fin n -> Fun (Succ n) But with the efficiency of native types instead of unary encodings. -------------------------------------------- -- Notes -------------------------------------------- I wrote this package for a linear algebra system I've been working on, but it should also be useful for folks working on Agda, Idris, etc, who want something more efficient to compile down to in Haskell. The package is still highly experimental, and I welcome any and all feedback. Note that we implement type-level numbers using [1] and [2], which works fairly well, but not as nicely as true dependent types since we can't express certain typeclass entailments. Once the constraint solver for type-level natural numbers becomes available, we'll switch over to using that.(Continue reading)