7.3.1 Semantics of System-F🔗

The semantics of System-F can be given in terms of substitution, just like STLC. Let’s run some example programs to get a feel for how programming in System-F looks.

First, the identity function evaluated on the number 10:

((\Lambda X . \lambda x : X . x)~[\texttt{Num}{}])~10 \xrightarrow{\text{Substitute }\texttt{Num}{}} (\lambda x : \texttt{Num}{} . x)~10 \xrightarrow{\text{Substitute }10} 10

Now let’s do a more interesting case. Let’s define a "call-twice" function that takes two arguments: a function f of type X \rightarrow X and an argument a of type X, and calls f twice with a as the initial argument:

\texttt{calltwice} = \Lambda X . \lambda f : X \rightarrow X . \lambda a : X . f~(f~a)

Let’s step through an example invocation of calltwice:

\begin{align*} &(((\Lambda X . \lambda f : X \rightarrow X . \lambda a : X . f~(f~a))~[\texttt{Num}])~(\lambda x : \texttt{Num} . x))~10 \\ &\xrightarrow{\text{substitute \texttt{Num}}} ((\lambda f : \texttt{Num} \rightarrow \texttt{Num} . \lambda a : \texttt{Num} . f~(f~a))~(\lambda x : \texttt{Num} . x))~10 \\ &\xrightarrow{\text{substitute }(\lambda x : \texttt{Num} . x)} ((\lambda a : \texttt{Num} . (\lambda x : \texttt{Num} . x)~((\lambda x : \texttt{Num} . x)~a)))~10 \\ &\xrightarrow{\text{substitute }10} ((\lambda x : \texttt{Num} . x)~((\lambda x : \texttt{Num} . x)~10)) \\ &\rightarrow (\lambda x : \texttt{Num} . x)~10 \\ &\rightarrow 10 \end{align*}

7.3.2 A Typechecker for System-F🔗

\dfrac{~}{\Gamma \vdash \texttt{n} : \texttt{Num}}~\text{(T-Num)} \qquad \dfrac{x \in \Gamma \qquad \Gamma(x) = t}{\Gamma \vdash x : t}~\text{(T-Ident)} \dfrac{\Gamma \cup \{x \mapsto t_1\} \vdash e : t_2}{\Gamma \vdash (\lambda x : t_1 . e) : t_1 \rightarrow t_2 }~\text{(T-Lam)} \qquad \dfrac{\Gamma \vdash e_1 : t_1 \rightarrow t_2 \qquad \Gamma \vdash e_2 : t_1} {\Gamma \vdash (e_1~e_2) : t_2}~\text{(T-App)} \dfrac{\Gamma \cup X \vdash e : \tau}{\Gamma \vdash \Lambda X . e : \forall X . \tau}~\text{(T-TLam)} \qquad \dfrac{\Gamma \vdash e_1 : \forall X . \tau_1 \qquad X \in \Gamma }{e_1 ~ [\tau_2] : \tau_1[X \mapsto \tau_2]}~\text{(T-TApp)}

Figure 22: Typing rules for System-F with numbers.

As an example, here is a typing derivation tree:

\dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{x:X \in \{X, x:X\}}{ \{X, x:X\} \vdash x : X}~\text{(T-Var)} } {\{X\} \vdash \lambda x : X . x : X \rightarrow X}~\text{(T-Lam)} } {\{\} \vdash (\Lambda X . \lambda x : X . x) : \forall X . X \rightarrow X}~\text{(T-TLam)} } { \{\} \vdash ((\Lambda X . \lambda x : X . x)~[\texttt{Num}]) : \texttt{Num} \rightarrow \texttt{Num}}~\text{(T-Tapp)} \qquad \{\} \vdash 10 : \texttt{Num}} { \{\}\vdash ((\Lambda X . \lambda x : X . x)~[\texttt{Num}])~10 : \texttt{Num}}~\text{(T-App)}

There is a subtlety in these rules: the (T-App) rule implicitly requires comparing two types for equality. However, it is not trivial to check whether or not two types are equal in System-F. Consider the following two terms, annotated with their types:

\Lambda X . (\lambda x : X . x) : \forall X . (X \rightarrow X) \qquad \qquad \Lambda Y . (\lambda x : Y . x) : \forall Y . (Y \rightarrow Y)

7.3.3 Implementing our typing rules🔗

Finally, we can implement our typing rules:

> (define-type-alias TEnvF (Hashof Symbol typ))

> (define mt-env-sysf (hash empty))

> (extend-sysf : (TEnvF Symbol typ -> TEnvF))

> (define (extend-sysf old-env new-name value)     (hash-set old-env new-name value))

> (typeof-sysf : (TEnvF expr -> typ))

> (define (typeof-sysf env e)     (type-case expr e                [(identF x)                 (type-case (Optionof typ) (hash-ref env x)                            [(some t) t]                            [(none) (error 'type "unbound identifier")])]                [(numF n) (numT)]                [(lamF id t body)                 (funT t (typeof-sysf (extend-sysf env id t) body))]                [(appF e1 e2)                 (let [(t-e1 (typeof-sysf env e1))                       (t-e2 (typeof-sysf env e2))]                   (type-case typ t-e1                              [(funT tau1 tau2)                               (if (type-eq? tau1 t-e2)                                   tau2                                   (error 'type-error "invalid function call"))]                              [else (error 'type-error "invalid function call")]))]                [(tlamF id body)                 (forallT id (typeof-sysf env body))]                [(tappF e t)                 (type-case typ (typeof-sysf env e)                            [(forallT id body)                             (tsubst body id t)]                            [else (error 'type "invalid type application")])]))

> (define (type-check? e)     (try      (begin        (typeof-sysf mt-env-sysf e)        #t)      (λ () #f)))

7.3.4 Consequences of System-F Types (extra content)🔗

A natural question you might have is: is System F more expressive than the simply-typed lambda calculus? The answer is yes: we can give types to programs that are not typeable in STLC. An example is the self-application term:

\lambda x . x~x

We saw how we couldn’t give a type to this program in STLC because there was no way for the argument to a function to have the same type as the function itself. In System F, we can give a type to this program by making use of type application:

\lambda x : (\forall X . X \rightarrow X) . (x~[\forall X . X \rightarrow X])~x

Note that this program has type (\forall X . X \rightarrow X) \rightarrow (\forall X . X \rightarrow X) This seems to imply that System F is extremely expressive, perhaps even so expressive that it can write all programs that can be written in the untyped lambda calculus. But in fact, this is not the case: just like STLC, System F is strongly normalizing (meaning, all well-typed System F programs terminate).

How can this be if we just typechecked self application? It seems like we should now be able to write \Omega by chaining together \omega~\omega, just like we did in the untyped lambda calculus.

You should notice that they are all observationally equivalent to the identity function!

Why is this the case? Intuitively, all programs of type \forall X . X \rightarrow X must (1) consume some unknown type X, and (2) produce an inhabitant of some unknown type X \rightarrow X. Since this function can’t know anything at all about X – including how to construct values of type X – all it can do is return the argument to the caller.

Now we are starting to see how type structure can tell us rich and interesting details about how programs behave, and can even be so restrictive that there is exactly one program that inhabits a particular type.