Stronger static types, was Re: [Haskell-cafe] Re: Versioning
jmaessen at alum.mit.edu
Fri Dec 22 08:28:01 EST 2006
On Dec 21, 2006, at 5:03 PM, Jacques Carette wrote:
> What must be remembered is that full dependent types are NOT needed
> to get a lot of the benefits of dependent-like types. This is what
> some of Oleg's type gymnastics shows (and others too). My interest
> right now lies in figuring out exactly how much can be done
> For example, if one had decent naturals at the type level (ie
> naturals encoded not-in-unary) with efficient arithmetic AND a few
> standard decision procedures (for linear equalities and
> inequalities say), then most of the things that people currently
> claim need dependent types are either decidable or have very strong
> heuristics that "work" .
My understanding is that BlueSpec did roughly this. As we're
discovering in Fortress, type-level naturals are a big help; faking
it really is horrible, as unary representations are unusable for real
work and digital representations require a ton of stunts to get the
constraints to solve in every direction (and they're still ugly).
I for one would welcome a simple extension of Haskell with type-level
nats (the implementor gets to decide if they're a new kind, or can
interact with * somehow).
[PS: hadn't seen the LNCS reference before, thanks to Jacques for
sending that along.]
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2425 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20061222/f1df8906/smime.bin
More information about the Haskell-Cafe