Lars Lundgren wrote:
> Decidability should not be given up to easily, but i think that dependent
> types has a very good price/performance ratio.
And you don't have to give up decidable type checking to have dependent
types! Dependent types per se do not make type checking undecidable. It is
the combination of general recursion and dependent types that gives
undecidability. (Correct me if I am wrong!)
The undecidability comes from the fact that the type checker needs to compare
types for equality (or inclusion, if you have subtypes), so if you have
general recursion in type expressions, you need to solve the halting problem
to get decidable type checking.
By restricting recursion in type expression just enough to get decidable
equality, you can have the cake and eat it too! The interesting problem then
is finding the largest possible class of recursive definitions that you can
allow...
Perhaps it would be a good idea to consider the work done on "Strong
Functional Programming"as part of the Haskell 2 design process. Here is one
link:
http://www.cs.ukc.ac.uk/people/staff/ajt/ESFP/Published/
--
Thomas Hallgren
