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

[Jacques Carette]

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