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

[Lennart Augustsson]

Yes, Bluespec has efficient type level naturals.  But it only has  
arithmetic and some trivial decision procedures.  The slogan is "the  
type checker knows arithmetic, not algebra".
It worked pretty well.  But you soon get into situations where you  
need polymorphic recursion of functions with type level naturals.  It  
needs careful consideration (I never implemented that for Bluespec).

	-- Lennart

On Dec 22, 2006, at 14:28 , Jan-Willem Maessen wrote:

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