winterkoninkje: Shadowcrane (Default)
[personal profile] winterkoninkje

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.

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

Links

(n::Nat) is redundant

Date: 2013-07-22 08:00 am (UTC)
From: [identity profile] heisenbug.myopenid.com
`n` should suffice here as kind inference readily fills the ::Nat part in!

Profile

winterkoninkje: Shadowcrane (Default)
wren gayle romano

July 2014

S M T W T F S
   12345
678 910 11 12
1314151617 1819
20212223242526
2728293031  

Most Popular Tags

Expand Cut Tags

No cut tags

Style Credit

Page generated Jul. 26th, 2014 03:05 am
Powered by Dreamwidth Studios