type-level integers using type families

[Peter Gavin]

Replying to myself...

I put a copy of the darcs repo at <http://code.haskell.org/~pgavin/tfp>, 
if anyone is interested.

Pete

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?
> 
> Pete