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