[Haskell-cafe] type-level integers using type families

[Isaac Dupree]

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.

nice, it's been tried before, etc. etc.. And of course it doesn't work 
with a released version of GHC, so maybe it's hoping too much that it 
would be on Hackage.  What I was going to say was, see if there is one 
on hackage, otherwise there should be one there to be polished.  But I 
guess searching haskell-cafe is your man :-) (your way to try to find 
any.  Or the Haskell blogosphere too.)

> One thing that I'd like to be able to do is lazy unification on type 
> instances, so that things like
> 
> ...
> 
> 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?

Yeah -- that would be neat but generally tends to lead to undecidability 
(unless you're really careful making it a lot(?) less useful).  That is, 
potential nontermination in the type inferencer/checker, not just in 
runtime.  Then you'll want it to be well-defined when something is 
type-level-lazy, so you can reliably write your type-level algorithms. 
And *that* is bound to be rather difficult to define and to implement 
and maintain.