BAL paper available

[C T McBride]

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:
> > > Serge Mechveliani :
> > > > ...
> > > > The matter was always in parametric domains ...
> > > > Whoever tried to program real CA in Haskell, would agree that such =
a
> > > > problem exists.
> >=20
> > Can you be more precise what the problem is?  One problem I see is
> > that referred to in Section 3 of the paper: you really need types that
> > depend on parameters (in particular, integer parameters).  This is,
> > indeed, a problem--currently, you have to do runtime checks.
> >=20
> > Full-fledged dependent types =E0 la Cayenne are undecidable, but there
> > are weaker variants that are likely to be good enough.
>=20
> 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.=20

(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.)

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.=20
In this way, all the programs we know and love remain available at
run-time, whilst the type system acquires a large yet decidable extension
to its expressive power.  The key is the application rule, for it is here
that programs leak into types.

 G |- f :: all x::S . T   G |- s :: S
--------------------------------------
         G |- f s :: [s/x]T

If s is potentially non-terminating, typechecking becomes undecidable:
[s/x]T may not have a normal form.=20

Now let's separate compile-time programs (typed with `|-') from run-time
programs (typed with `/-', say). Restricting the compile-time language to
structural recursion, the above rule poses no threat. We can add

 G |- t :: T
-------------  (a compile-time program is a run-time program)
 G /- t :: T

 G /- f :: all x::S . T   G |- s :: S
-------------------------------------- x free in T
        G /- f s :: [s/x]T

 G /- f :: S -> T   G /- s :: S
-------------------------------- (S -> T abbreviates all x::S. T
         G /- f s :: T            when x is not free in T)

  G /- f :: T -> T
-------------------- (fixpoint)
 G /- Y f :: T -> T

compile-time structurally recursive programs, extending with general
recursion only at run-time. Typechecking is thus decidable, with all your
old code intact.=20

Structural recursion is a syntactically checkable notion which allows a
large, but obviously not complete language of terminating programs to be
recognized as such. How large? Well, first-order unification is
structurally recursive, and so is normalization for simply-typed
lambda-calculus. As decidable type systems go, this one is better than a
poke in the eye.=20

I respectfully suggest that dependent types are worth a second look.

Cheers

Conor