[BULK] Re: [plt-scheme] The perfect teaching language--Is this too much to ask for?

[Stephen Bloch]

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?  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