Dependent types (Was: Re: BAL paper available)

[Stefan Karrmann]

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