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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
