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

[Manuel M T Chakravarty]

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.

I am glad to hear that type families work for you.

> 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 don't think i entirely understand the question.  Do you mean that  
from an equality like

   Cond b Int Bool ~ Int

you want the type checker to infer that (b ~ True)?  This is generally  
not correct reasoning as type families are open; ie, subsequent  
modules might add

   data Bogus
   type instance Bogus y z = Int

and now there are two solutions to (Cond b Int Bool ~ Int).

Manuel