type-level integers using type families
pgavin at gmail.com
Sat May 31 18:32:49 EDT 2008
Replying to myself...
I put a copy of the darcs repo at <http://code.haskell.org/~pgavin/tfp>,
if anyone is interested.
Peter Gavin wrote:
> Has anyone else tried implementing type-level integers using type families?
> I tried using a couple of other type level arithmetic libraries
> (including type-level on Hackage) and they felt a bit clumsy to use. I
> started looking at type families and realized I could pretty much build
> an entire Scheme-like language based on them.
> In short, I've got addition, subtraction, & multiplication working after
> just a days worth of hacking. I'm going to post the darcs archive
> sometime, sooner if anyone's interested.
> I really like the type-families based approach to this, it's a lot
> easier to understand, and you can think about things functionally
> instead of relationally. (Switching back and forth between Prolog-ish
> thinking and Haskell gets old quick.) Plus you can do type arithmetic
> directly in place, instead of using type classes everywhere.
> One thing that I'd like to be able to do is lazy unification on type
> instances, so that things like
> data True
> data False
> type family Cond x y z
> type instance Cond True y z = y
> type instance Cond False y z = z
> will work if the non-taken branch can't be unified with anything. Is
> this planned? Is it even feasible?
> I'm pretty sure it would be possible to implement a Lambda like this,
> but I'm not seeing it yet. Any ideas?
More information about the Libraries