[Haskell-cafe] type-level integers using type families
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Thu May 29 23:04:18 EDT 2008
> Has anyone else tried implementing type-level integers using type
> 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
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
type instance Bogus y z = Int
and now there are two solutions to (Cond b Int Bool ~ Int).
More information about the Libraries