[plt-scheme] The perfect teaching language--Is this too much to ask for?
On Jun 15, 2009, at 11:02 AM, hendrik at topoi.pooq.com wrote:
> There's a formal correspondence between statements in a formal system
> and types. I believe it's called the Curry-Howard correspondence.
Yes, I saw that in grad school.
> Roughly speaking,
>
> a proposition corresponds to a type
> a proof of a propsition corresponds to a value of the type.
> A proof that P implies Q corresponds to a function from P to Q (thus
> we can think of the function as converting proofs of P into proofs
> of Q)
> A proof of P & Q is a pair of a proof of P and a proof of Q.
> Correspondingly, we get a Catesian product of types.
>
> There are dependent types, which I write
> v : T -> S, where S contains free occurrences of v.
> This is a type for functions whose returned values have a type which
> depends on the argument. In logic, this corresponds to the universal
> quantifier,
>
> And so on.
>
> This whole thing breaks down if you have nonterminating programs,
> because a function F defined as
> let F = lambda x. F(x)
> gives an infinite recursion, and can be typed to return any type
> whatsoever, even those that correspond to false propositions.
>
> And if you let type be a type, it turns out to be possible to create
> set-theoretical paradoxes out of this stuff, whose "proofs" are
> nonterminating functions.
IIRC, under at least some definitions, typed lambda-calculus is not
only decidable but polynomial-time decidable. This is a lovely
guarantee of termination, and even termination in a reasonable length
of time, but it also means you can't write programs for problems that
don't have polynomial-time solutions -- in fact, you can't write
programs for problems without a KNOWN polynomial-time algorithm, like
CLIQUE, SAT, Travelling Salesman, etc. not to mention intentionally
non-terminating programs such as operating systems and servers, or
programs that look for counterexamples to the Riemann hypothesis. It
always seemed to me that by insisting on decidability of term
equivalence, we were throwing out a lot of practical programming
power. (Part of my dissertation was defining a functional language
in which the only programs you could write were parallelizable to O
(log(n)) time -- not that you would actually want to program in that
language, but just to show that it could be done.)
I'm reading Meyer & Reinhold's _'Type' is not a type_ paper right
now. The crucial paragraph seems to be
"The failure of property (2) (strong normalisation) is not by itself
surprising, since in a general programming language one expects terms
which define divergent computations not to have normal forms.
Similarly, the failure of property (3) (undecidability of term
equivalence) is to be expected. But the failure of property (4) means
that it is not decidable whether a term has a given type, and more
generally whether two types are equal. This undermines the
possibility of effective "static" type-checking before runtime.
Finally, the failure of property (5), conservative extension, is also
serious as we indicate in Section 4 below."
In other words, the issue isn't so much non-terminating or non-
provably-terminating programs -- those are inevitable, as I said in
my previous post -- but non-terminating compile-time type checks. If
a programmer writes a program that goes infinite, the programmer
deserves what (s)he gets, but if a programmer writes a program on
which the COMPILER goes infinite, whom do you blame?
The aforementioned Section 4 points out that
(a) having a type of all types allows you to construct a fixed-point
operator Y;
(b) having a fixed-point operator Y allows you to find a fixed-point
for the "add1" function, i.e. a number which is 1 more than itself,
and hence both even and odd, which is a little disturbing;
(c) the existence of such a number, together with an (apparently)
reasonably-defined conditional operator and (apparently) reasonable
equality axioms, allows you to prove that ANY two terms of the same
type are equal, which is even more disturbing.
As Meyer and Reinhold point out, the usual interpretation for a fixed-
point of "add1" is a nonstandard integer value that corresponds to
non-terminating computations. The difficulty can therefore be seen
as a conflict between an axiomatization that has non-standard models
and a conditional operator that makes sense on "standard" or
"convergent" values, but goes kerflooey when you bring in such
nonstandard values.
I guess it's analogous to the problem with "the set of all sets" that
led to Russell's paradox, the dismantling of naive set theory, the
_Principia Mathematica_, and thence to Goedel's incompleteness theorems.
I'll have to think about this: "type" as a type still seems so
elegant, so expressively efficient :-) My naive first impulse is to
suggest a consistent but incomplete static type-checker that never
misclassifies something's type, correctly classifies the types of
MOST expressions in practice, and when it can't, knows when to give
up so it at least terminates. Has somebody already proven that
that's unattainable too?
Stephen Bloch
sbloch at adelphi.edu