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

 From: hendrik at topoi.pooq.com (hendrik at topoi.pooq.com) Date: Mon Jun 15 11:02:59 EDT 2009 Previous message: [BULK] Re: [plt-scheme] The perfect teaching language--Is this too much to ask for? Next message: [plt-scheme] The perfect teaching language--Is this too much to ask for? Messages sorted by: [date] [thread] [subject] [author]

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

```

 Posted on the users mailing list. Previous message: [BULK] Re: [plt-scheme] The perfect teaching language--Is this too much to ask for? Next message: [plt-scheme] The perfect teaching language--Is this too much to ask for? Messages sorted by: [date] [thread] [subject] [author]