On 16 Feb 1999, Carl R. Witty wrote:
> Lars Lundgren <[EMAIL PROTECTED]> writes:
>
> > We have already accepted undecidable type checking, so why not take a
> > big step forward, and gain expressive power of a new magnitude, by
> > extending the type system to allow dependent types.
>
> Wait a minute...who has accepted undecidable type checking? Are you
> talking about the new type class features in GHC? As far as I know,
> those are explicitly documented as experimental, and must be enabled
> by a command-line option. I'm not sure that anybody has "accepted"
> undecidable type checking.
>
Yes, I was refering to various experimental features in Gofer, and
recently also in GHC. I should not have used the word 'accepted' as I did.
What I meant was that since those features are candidates for haskell 2,
(At least, it is my impression that they are)
we can also consider other extensions wich leads to undecidable type
checking.
Of course, this is not a desirable property, but it may not be that bad in
practice. The type checker can use some default which works in in 95% of
the programs, and the really complex programs can be checked by using a
compiler flag which increases some limit.
Decidability should not be given up to easily, but i think that dependent
types has a very good price/performance ratio.
/Lars L
