type-level integers using type families

[Peter Gavin]

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?

Pete