Stronger static types, was Re: [Haskell-cafe] Re: Versioning

[Jan-Willem Maessen]

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  
> statically.
> 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" [1].

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).

-Jan-Willem Maessen

[PS: hadn't seen the LNCS reference before, thanks to Jacques for  
sending that along.]


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2425 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20061222/f1df8906/smime.bin