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

[Jacques Carette]

Yes, dependent types have a lot to do with all this.  And I am an eager 
lurker of all this Epigram.

Scott Brickner wrote:
> Jacques Carette wrote:
>> Array out-of-bounds, fromJust, head on an empty list, and 
>> pattern-match failures are in my list of things I wish the type 
>> system could help me with.  And sometimes it can [again, see Oleg's 
>> posts].  But is definitely where I am *eager* to see developments.
> I agree with you, though - I'm very eager to see further developments 
> along these lines. It's the main reason I started learning Haskell, 
> and I'm absolutely convinced that functional programming and this kind 
> of increasingly strong typing are the way of the future for programming.
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].

Jacques

[1]
@book{SymbolicAnalysis,
  author    = {Thomas Fahringer and
               Bernhard Scholz},
  title     = {Advanced Symbolic Analysis for Compilers: New Techniques
               and Algorithms for Symbolic Program Analysis and 
Optimization},
  publisher = pub-SV,
  series    = {Lecture Notes in Computer Science},
  volume    = {2628},
  year      = {2003},
  isbn      = {3-540-01185-4}
}