[Haskell-cafe] type-level integers using type families
isaacdupree at charter.net
Thu May 29 05:54:03 EDT 2008
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
More information about the Libraries