[PRL] Type question...

[Mitchell Wand]

Just back from ICFP, so I'm only getting to this now.

Of course Y (and its friends) have no simple type, because the simply-typed
lambda calculus is strongly normalizing, and Y has no normal form.

Every pure lambda term is typable with recursive types, since you can give
any pure lambda term the type  (mu t)(t -> t).  If you add constants, of
course, all bets are off.

I believe there is a theorem that says that all pure lambda terms are
typable using intersection types, but I don't know the details.

--Mitch

On 10/5/07, Felix S Klock II <pnkfelix at ccs.neu.edu> wrote:
>
>
> On Oct 3, 2007, at 11:33 PM, Riccardo Pucella wrote:
>
> >>> (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))
> >
> >> I believe it's the (f f n) and (g g (- m 1)) that shoot you down.
> >> There's no simple type for a function that accepts itself as an
> >> argument.
> >
> > Right; as Carl says, just look at (lambda (f n) (f f n))
> >
> > The best type you could give it is the recursive type:
> >    (\mu Z.( Z x a -> b)) x a -> b
>
> Or a (sufficiently large) intersection type could also type the term,
> I believe.
>
> But who wants to go down that road. . .
>
> -Felix
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
>
-------------- next part --------------
HTML attachment scrubbed and removed