[BULK] Re: [plt-scheme] The perfect teaching language--Is this too much to ask for?
On Sun, Jun 14, 2009 at 02:32:49PM -0400, Stephen Bloch wrote:
> I wrote:
> >>I'm missing something. Why shouldn't type be a type?
>
> To which Hendrik replied:
> >No good reason at all, unles syou're into formal logic and type
> >theory,
> >in which case you find there are metarecursive loopholes which admit
> >infinite proofs and nonterminating programs.
> >
> >So if you don't mind being able to write a nonterminating program
> >occasionally, there's no particular reason why type shouldn't be a
> >type.
>
> For those of us who have studied logic but not (much) language theory,
> could you elaborate on this?
There's a formal correspondence between statements in a formal system
and types. I believe it's called the Curry-Howard correspondence.
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.
> Obviously a program that keeps iterating
> "type-of" until reaching something that doesn't have a type will go
> infinite if everything (including "type") has a type, but that's
> inevitable; is there a more interesting and reasonably short example?
>
> Steve Bloch