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.
>
> Cayenne, http://www.cs.chalmers.se/~augustss/cayenne, already has
> dependent types, but seems to be an experimental language only with a very
> small user base.
I fear my previous response to this message was a little hasty and
overly forceful. Let me try again.
I think dependent types are great; I'd love to have the most powerful
type system possible. However, I'm also very wary of undecidable type
checking.
I worry about undecidable type checking mostly from the viewpoint of
the novice programmer; can we make compilers that give good error
messages that make sense to the novice?
It is my impression that the current instances of undecidable type
checking in GHC and Gofer are not a problem in practice. The compiler
puts a limit on the amount of effort it is going to expend to infer
types, and this limit is basically never exceeded for reasonable
programs. While it may be possible to encode arbitrary computations
in the type inference process, this encoding is rather bizarre, and is
not something you would find in a real program. (This is basically
the same reason that Hindley-Milner typechecking works in practice,
even though it is PSPACE-complete.)
I think you're advocating a dependent type system where the compiler
must evaluate arbitrary user-written code in order to typecheck. If
so, I fear it will be quite difficult for a compiler to "do the right
thing". Some people will inevitably add dependent types which take
a very long time to evaluate (and hence typecheck). Is "the right
thing" for the compiler to go ahead and evaluate these no matter how
long it takes (so that you can write a quite simple program which
takes longer than the lifetime of the universe to compile)? Or should
the compiler give up and print an error message? The latter choice
will reduce portability of Haskell programs, unless all compilers can
agree on the exact bound.
Maybe this undecidability won't be a problem in practice. On the
other hand, perhaps we can come up with a type system which has most
of the benefits we want but still allows decidable (and efficient)
type checking. I'd like for us to explore that option before we
commit to a language with undecidable type checking.
Carl Witty
[EMAIL PROTECTED]
