Y combinator in System F, or not?

Moderator: Type Systems of Programming Languages

erdweg
Moderator
Moderator
Beiträge: 60
Registriert: 28. Mär 2013 10:08

Y combinator in System F, or not?

Beitrag von erdweg »

Consider the following well-typed System F program:

Code: Alles auswählen

\x:(∀α. α). x[∀α. α] x
.

In our discussion on fixpoint combinators, we saw that the application of a term to itself was the critical property required to define a fixpoint combinator. It seems System F supports such self-application.

Why is System F still too weak to define a fixpoint combinator as a well-typed program? What is the “flaw” in above program?

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Re: Y combinator in System F, or not?

Beitrag von AlexanderF »

the term
\x:(∀α. α). x[∀α. α] x
has type
∀α. α -> ∀α. α

and I think,
(\x:(∀α. α). x[∀α. α] x) (\x:(∀α. α). x[∀α. α] x)
or similar constructs like fixpoint operators are still not typable,
but Im not sure.

erdweg
Moderator
Moderator
Beiträge: 60
Registriert: 28. Mär 2013 10:08

Re: Y combinator in System F, or not?

Beitrag von erdweg »

Hint: Find a program of type ∀α. α, that you can pass to

Code: Alles auswählen

\x:(∀α. α). x[∀α. α] x
as argument.

Antworten

Zurück zu „Type Systems of Programming Languages“