ANN: data-fin

[wren ng thornton]

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

[1] Oleg Kiselyov and Chung-chieh Shan. (2007) Lightweight static
resources: Sexy types for embedded and systems programming. Proc. Trends
in Functional Programming. New York, 2--4 April 2007.
http://okmij.org/ftp/Haskell/types.html#binary-arithm

[2] Oleg Kiselyov and Chung-chieh Shan. (2004) Implicit configurations:
or, type classes reflect the values of types. Proc. ACM SIGPLAN 2004
workshop on Haskell. Snowbird, Utah, USA, 22 September 2004. pp.33--44.
http://okmij.org/ftp/Haskell/types.html#Prepose


--------------------------------------------
-- Links
--------------------------------------------

Homepage:
    http://code.haskell.org/~wren/

Hackage:
    http://hackage.haskell.org/package/data-fin

Darcs:
    http://community.haskell.org/~wren/data-fin

Haddock (Darcs version):
    http://community.haskell.org/~wren/data-fin/dist/doc/html/data-fin

-- 
Live well,
~wren