C T McBride schrieb folgendes am Wed, May 16, 2001 at 01:03:25PM +0100:
On Wed, 16 May 2001, Stefan Karrmann wrote:
On Tue, May 15, 2001 at 09:14:02PM +0300, Dylan Thurston wrote:
On Tue, May 15, 2001 at 06:33:41PM +0200, Jerzy Karczmarczuk wrote: ... you really need types that depend on parameters (in particular, integer parameters). This is, indeed, a problem--currently, you have to do runtime checks.
Full-fledged dependent types à la Cayenne are undecidable, but there are weaker variants that are likely to be good enough.
What are the weaker variants? Do you know some references? Are they still decidable? That surprises me. If you allow integer arithmetic you can do already all computations (Church).
The idea that `dependent types are undecidable' is a popular but understandable misconception arising from a particular design decision in a particular system---Cayenne.
Dependent types as found in proof systems such as Coq and Lego do have decidable typechecking: programs may only use structural recursion, and hence all the evaluation which takes place during typechecking is guaranteed to terminate. However, in order to support real programming, Cayenne allows general recursion: as it makes no distinction between the programs which are executed at compile-time and those only executed at run-time, undecidability creeps in. Understandably, neither horn of this dilemma is particularly attractive to programmers who want to combine flexibility at run-time with a genuinely static notion of typechecking.
With constructor type we can do dimension checking, as shown earlier on this list. Can't we check in a similiar way an integer paramter? But is this general enough? You may compute some integer n and then do some calculations in Z/n. How can this be done? Do you need to do the calculation only with structural recursion?
(Of course, post-98 Haskell with certain type class options selected has a type-level language containing non-terminating programs, making typechecking undecidable for exactly the same reason as in Cayenne.)
If possibly non-terminating type analysis creeps into Haskell, why don't we choose the Cayenne style?
However, there is a middle way: we can distinguish compile-time programs from run-time programs and restrict the former to the structurally recursive fragment, leaving general recursion available in the latter.
Is there any (syntactical) proposal somewhere? -- Stefan Karrmann