[PRL] Type question...

[Matthias Felleisen]

On Oct 3, 2007, at 11:17 PM, Bryan Chadwick wrote:

>    Quick question.   After thinking about a complex lambda term  
> (really
> just a poor man's recursion),  I don't think it can be hand annotated
> with simple types (if the language was extended to do so).
>
> Is this correct?  Thoughts?
>
> Here's factorial without letrec...
>
> (let ((fact (lambda (num)
>                 ((lambda (f n) (f f n))
>                  (lambda (g m)
>                    (if (< m 2) 1
>                        (* m (g g (- m 1))))) num))))
>    (fact 5))


Pascal used to assign types to this kind of program :-)
(not quite the (f f n) part) and I bet you can still get
it thru the C type checker but I assume you mean "sound"
type system (and so did everyone else who responded).

I wish regular programmers could distinguish these
two kinds of systems.

Why don't you post this kind of question on a forum
where you can evaluate the reactions of regular
programmers. I wonder how much this idea of 'safety'
has sunk in (and what this says about PL education
at the undergraduate level. I used to cover Type
Soundness in "311" aka "660". I doubt it is still
mentioned.)

-- Matthias