[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