Brian Hulley wrote:
Would it be possible to augment Haskell's type system so that it was
the same as that used in Epigram?
No, no! Epigram is a wonderfully pure research experiment in one corner
of the design space. The corner it is exploring is not particularly
"Haskell like", though the results of the exploration should bear fruit
for Haskell now and then [and it already has].
While I am quite sure Haskell could do with more information in its
types, proof requirements cannot be anywhere close to what it is in
Epigram. I am convinced there is a "Haskell compatible" middle road.
Also, typing is not the only issue for compile time guarantees. Consider:
[Example of coding enumeration as pattern-match vs guards vs ... deleted]
This is much more of an engineering issue than a theoretical issue. In
some cases (explicit pattern match with no guards), coverage checking is
trivial because the language you are dealing with is so simple. In
other cases (guards), in general the problem is undecidable, but there
are many many particular cases where there are applicable decision
procedures. It seems to be a common choice amongst compiler writers to
not wade into these waters -- although the people doing static analysis
have been swimming there for quite some time.
My feeling is that slowly increasing amounts of static analysis will be
done by compilers (beyond just "types" or the current strictness
analyses) to include these kinds of total/partial checks on guards,
"shape" analysis, etc. It is already happening, the one question is
what will be the speed at which it happens in Haskell. Maybe it is time
for ICFP and SAS to be held together.
Jacques
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
