flaw in typing rules for System F

Moderator: Type Systems of Programming Languages

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

flaw in typing rules for System F

Beitrag von AlexanderF »

hello,

in the lecture we added parametric polymorphism to the simply typed lambda calculus and obtained the so called System F.

The typing rules for this language were like this:

(x, T) in Gamma
------------------- T-Var
Gamma |- x : T

Gamma, x : T1 |- e : T2
----------------------------------- T-Abs
Gamma |- \x :T1.e : T1 -> T2

Gamma |- e1 : T1 -> T2 Gamma |- e2 : T1
---------------------------------------------------- T-App
Gamma |- e1 e2 : T2

Gamma |- e : T
------------------------------------------ T-TAbs
Gamma |- \alpha.e : forall alpha. T

Gamma |- e : forall alpha. T1
------------------------------------------ T-TApp
Gamma |- e [T] : T1[alpha := T]


I think the typing system is not quite correct, because now,
we can not only type:
\alpha. \x:alpha. x : forall alpha. alpha -> alpha
(with T-TAbs, T-Abs, T-Var)

but also:
\beta. \x:alpha. x : forall beta. alpha -> alpha
and
\x:alpha. x : alpha -> alpha

I think this is not intended.


To fix this, I think, it is necessary to introduce a second context,
or to extend the one context, s.t.
it not only contains judgments of the form: x:T, that says, that the variable x hat type T,
but also those of the form: T, that says, that T is a proper type.

together with the extended rules T-Abs and T-TAbs:

Gamma |- T1 Gamma, x : T1 |- e : T2
----------------------------------------------- T-Abs'
Gamma |- \x :T1.e : T1 -> T2

Gamma, alpha |- e : T
------------------------------------------ T-TAbs'
Gamma |- \alpha.e : forall alpha. T

and the introduction of two new (typing) rules:
(they are similar like two of the kinding rules in System F-omega)

alpha in Gamma
------------------- T-TVar
Gamma |- alpha

Gamma |- T1 Gamma |- T2
---------------------------------- T-Arr
Gamma |- T1 -> T2

the last rule says that T1 -> T2 is a proper type if T1 and T2 are proper types.
it is necessary to be able to type expressions like:
\alpha. \f:alpha->alpha. \x:alpha. f x : forall alpha. (alpha -> alpha) -> alpha -> alpha

regards,
Alexander

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

Re: flaw in typing rules for System F

Beitrag von erdweg »

You are right that System F permits the following term

Code: Alles auswählen

  \beta. \x:alpha. x : forall beta. alpha -> alpha
However, this is not a problem, because you cannot use it. When applying a type argument T, you get a term of type

Code: Alles auswählen

alpha->alpha
, where you don't know what alpha is.

Antworten

Zurück zu „Type Systems of Programming Languages“