let id = \x.x in id succ(id 0)

# System F

Simply typed lambda calculus is restrictive. The let-polymorphism of Hindley-Milner gives us more breathing room, but can we do better?

System F frees the type system further by introducing parts of lambda calculus
at the type level. We have *type abstraction* terms and *type application*
terms, which define and apply functions that take types as arguments and return
terms. At the same time, System F remains normalizing.

System F is rich enough that the self-application `\x.x x`

is typable.

If we focus on the types, System F is a gentle generalization of
Hindley-Milner. In the latter, any universal
quantifiers `(∀)`

must appear at the beginning of type, meaning they are scoped
over the entire type. In System F, they can be arbitrary scoped. For example.
`(∀X.X->X)->(∀X.X->X)`

is a System F type, but not a Hindley-Milner type,
while `∀X.(X->X)->X->X`

is a type in both systems.

This seemingly small change has deep consequences. Recall Hindley-Milner allows:

but rejects:

(\f.f succ(f 0)) (\x.x)

This is because algorithm W assigns `x`

a type variable, say `X`

, then finds
the conflicting constraints `X = Nat`

and `X = Nat → Nat`

. A locally scoped
generalized variable fixes this by causing fresh type variables to be generated
for each use, so the resulting constraints, say, `X = Nat`

and
`Y = Nat -> Nat`

, live and let live. Let-free let-polymorphism!

It’s easy to demonstrate this in Haskell. The following fails:

(\f->f succ(f 0))(\x->x)

We can make it run by enabling an extension, and annotating the identity function appropriately:

:set -XRankNTypes ((\f->f succ(f 0)) :: ((forall x.x->x)->Int))(\x->x)

We write type abstractions as lambda abstractions without a type annotation.
The simplest example is the *polymorphic identity function*:

id=\X.\x:X.x

For clarity, we capitalize the first letter of type variables in our examples.

The above represents a function that takes a type, and then returns an identity function for that type.

We write type applications like term applications except we surround the argument with square brackets. For example:

id [Nat] 42

evaluates to 42.

## Type spam

Our new features have a heavy price tag. In System F, type reconstruction is undecidable. We must add explicit types to every binding in every lambda abstraction. Moreover, applying type abstractions require us to state even more types.

Haskell magically fills in missing types if enough hints are given, which is why our example above got away with relatively little annotation. Our implementation of System F lacks this ability, so we must always supply types. (This is why we used Haskell above instead of our System F interpreter!)

Because types must frequently be specified, few practical languages are built on System F. (Perhaps it’s also because System F is a relatively recent discovery?) The Hindley-Milner system is often preferable, due to type inference.

However, behind the scenes, modern Haskell is an extension of System F. Certain language features require type annotation, and they generate unseen intermediate code full of type abstractions and type applications.

Type operators make types less eye-watering.

## Definitions

We replace the `GV`

constructor representing Hindley-Milner generalized
variables with its scoped version `Forall`

.

We add type applications and type abstractions to the `Term`

data type. A type
application is like a term application, except it expects a type as input (and
during printing should enclose it within square brackets). A type abstraction
is like a term abstraction, except its variable, being a type variable, has no
type annotation.

{-# LANGUAGE CPP #-} #ifdef __HASTE__ import Haste.DOM import Haste.Events #else import System.Console.Haskeline #endif import Control.Monad import Data.Char import Data.List import Data.Tuple import Text.Parsec data Type = TV String | Forall String Type | Type :-> Type data Term = Var String | App Term Term | Lam (String, Type) Term | Let String Term Term | TLam String Term | TApp Term Type instance Show Type where show (TV s) = s show (Forall s t) = '\8704':(s ++ "." ++ show t) show (t :-> u) = showL t ++ " -> " ++ showR u where showL (Forall _ _) = "(" ++ show t ++ ")" showL (_ :-> _) = "(" ++ show t ++ ")" showL _ = show t showR (Forall _ _) = "(" ++ show u ++ ")" showR _ = show u instance Show Term where show (Lam (x, t) y) = "\0955" ++ x ++ showT t ++ showB y where showB (Lam (x, t) y) = " " ++ x ++ showT t ++ showB y showB expr = '.':show expr showT (TV "_") = "" showT t = ':':show t show (TLam s t) = "\0955" ++ s ++ showB t where showB (TLam s t) = " " ++ s ++ showB t showB expr = '.':show expr show (Var s) = s show (App x y) = showL x ++ showR y where showL (Lam _ _) = "(" ++ show x ++ ")" showL _ = show x showR (Var s) = ' ':s showR _ = "(" ++ show y ++ ")" show (TApp x y) = showL x ++ "[" ++ show y ++ "]" where showL (Lam _ _) = "(" ++ show x ++ ")" showL _ = show x show (Let x y z) = "let " ++ x ++ " = " ++ show y ++ " in " ++ show z

Universal types complicate type comparison, because bound type variables
may be renamed arbitrarily. That is, types are unique up to *alpha-conversion*.

instance Eq Type where t1 == t2 = f [] t1 t2 where f alpha (TV s) (TV t) | Just t' <- lookup s alpha = t' == t | Just _ <- lookup t (swap <$> alpha) = False | otherwise = s == t f alpha (Forall s x) (Forall t y) | s == t = f alpha x y | otherwise = f ((s, t):alpha) x y f alpha (a :-> b) (c :-> d) = f alpha a c && f alpha b d f alpha _ _ = False

## Parsing

Parsing is trickier because elements of lambda calculus have invaded the type level. For each abstraction, we look for a type binding to determine if it’s at the term or type level. For applications, we look for square brackets to decide.

We follow Haskell and accept `forall`

as well as the harder-to-type `∀`

symbol.
Conventionally, the arrow type constructor `(->)`

has higher precedence.

We accept inputs that omit all but the last period and all but the first quantifier in a sequence of universal quantified type variables, an abbreviation similar to the one we’ve been using in sequences of abstractions.

data FLine = None | TopLet String Term | Run Term deriving Show line :: Parsec String () FLine line = (<* eof) . (ws >>) $ option None $ (try $ TopLet <$> v <*> (str "=" >> term)) <|> (Run <$> term) where term = letx <|> lam <|> app letx = Let <$> (str "let" >> v) <*> (str "=" >> term) <*> (str "in" >> term) lam = flip (foldr pickLam) <$> between lam0 lam1 (many1 vt) <*> term where lam0 = str "\\" <|> str "\0955" lam1 = str "." vt = (,) <$> v <*> optionMaybe (str ":" >> typ) pickLam (s, Nothing) = TLam s pickLam (s, Just t) = Lam (s, t) typ = forallt <|> fun forallt = flip (foldr Forall) <$> between fa0 fa1 (many1 v) <*> fun where fa0 = str "forall" <|> str "\8704" fa1 = str "." fun = ((TV <$> v) <|> between (str "(") (str ")") typ) `chainr1` (str "->" >> pure (:->)) app = termArg >>= moreArg termArg = (Var <$> v) <|> between (str "(") (str ")") term moreArg t = option t $ ((App t <$> termArg) <|> (TApp t <$> between (str "[") (str "]") typ)) >>= moreArg v = try $ do s <- many1 alphaNum when (s `elem` words "let in forall") $ fail "unexpected keyword" ws pure s str = try . (>> ws) . string ws = spaces >> optional (try $ string "--" >> many anyChar)

## Typing

We’ve abandoned type inference, which simplifies typing. Nonetheless, we must handle the new terms. Type abstractions are trivial. As for type applications, once again, a routine used at the term level must now be written at the type level: we must rename type variables when they conflict with free type variables.

The `shallow`

feature will be explained later.

typeOf :: [(String, Type)] -> Term -> Either String Type typeOf gamma t = case t of App (Var "shallow") y -> pure $ fst $ shallow gamma y Var s | Just t <- lookup s gamma -> pure t | otherwise -> Left $ "undefined " ++ s App x y -> do tx <- rec x ty <- rec y case tx of ty' :-> tz | ty == ty' -> pure tz _ -> Left $ show tx ++ " apply " ++ show ty Lam (x, t) y -> do u <- typeOf ((x, t):gamma) y pure $ t :-> u TLam s t -> Forall s <$> typeOf gamma t TApp x y -> do tx <- typeOf gamma x case tx of Forall s t -> pure $ beta t where beta (TV v) | s == v = y | otherwise = TV v beta (Forall u v) | s == u = Forall u v | u `elem` fvs = let u1 = newName u fvs in Forall u1 $ beta $ tRename u u1 v | otherwise = Forall u $ beta v beta (m :-> n) = beta m :-> beta n fvs = tfv [] y _ -> Left $ "TApp " ++ show tx Let s t u -> do tt <- typeOf gamma t typeOf ((s, tt):gamma) u where rec = typeOf gamma tfv vs (TV s) | s `elem` vs = [] | otherwise = [s] tfv vs (x :-> y) = tfv vs x `union` tfv vs y tfv vs (Forall s t) = tfv (s:vs) t tRename x x1 ty = case ty of TV s | s == x -> TV x1 | otherwise -> ty Forall s t | s == x -> ty | otherwise -> Forall s (rec t) a :-> b -> rec a :-> rec b where rec = tRename x x1

## Evaluation

Evaluation remains about the same. We erase types as we go.

As usual, the function `eval`

takes us to weak head normal form:

eval env (App (Var "shallow") t) = snd $ shallow (fst env) t eval env (Let x y z) = eval env $ beta (x, y) z eval env (App m a) = let m' = eval env m in case m' of Lam (v, _) f -> eval env $ beta (v, a) f _ -> App m' a eval env (TApp m _) = eval env m eval env (TLam _ t) = eval env t eval env term@(Var v) | Just x <- lookup v (snd env) = case x of Var v' | v == v' -> x _ -> eval env x eval _ term = term beta (v, a) f = case f of Var s | s == v -> a | otherwise -> Var s Lam (s, _) m | s == v -> Lam (s, TV "_") m | s `elem` fvs -> let s1 = newName s $ v : fvs `union` fv [] m in Lam (s1, TV "_") $ rec $ rename s s1 m | otherwise -> Lam (s, TV "_") (rec m) App m n -> App (rec m) (rec n) TLam s t -> TLam s (rec t) TApp t ty -> TApp (rec t) ty Let x y z -> Let x (rec y) (rec z) where fvs = fv [] a rec = beta (v, a) fv vs (Var s) | s `elem` vs = [] | otherwise = [s] fv vs (Lam (s, _) f) = fv (s:vs) f fv vs (App x y) = fv vs x `union` fv vs y fv vs (Let _ x y) = fv vs x `union` fv vs y fv vs (TLam _ t) = fv vs t fv vs (TApp x _) = fv vs x newName x ys = head $ filter (`notElem` ys) $ (s ++) . show <$> [1..] where s = takeWhile (/= '_') x ++ "_" rename x x1 term = case term of Var s | s == x -> Var x1 | otherwise -> term Lam (s, t) b | s == x -> term | otherwise -> Lam (s, t) (rec b) App a b -> App (rec a) (rec b) Let a b c -> Let a (rec b) (rec c) TLam s t -> TLam s (rec t) TApp a b -> TApp (rec a) b where rec = rename x x1

The function `norm`

recurses to find the normal form:

norm env@(gamma, lets) term = case eval env term of Var v -> Var v -- Record abstraction variable to avoid clashing with let definitions. Lam (v, _) m -> Lam (v, TV "_") (norm (gamma, (v, Var v):lets) m) App m n -> App (rec m) (rec n) Let x y z -> Let x (rec y) (rec z) TApp m _ -> rec m TLam _ t -> rec t where rec = norm env

## User Interface

The less said the better.

#ifdef __HASTE__ main = withElems ["input", "output", "evalB", "resetB", "resetP", "pairB", "pairP", "surB", "surP"] $ \[iEl, oEl, evalB, resetB, resetP, pairB, pairP, surB, surP] -> do let reset = getProp resetP "value" >>= setProp iEl "value" >> setProp oEl "value" "" run (out, env) (Left err) = (out ++ "parse error: " ++ show err ++ "\n", env) run (out, env@(gamma, lets)) (Right m) = case m of None -> (out, env) Run term -> case typeOf gamma term of Left msg -> (out ++ "type error: " ++ msg ++ "\n", env) Right t -> (out ++ show (norm env term) ++ "\n", env) TopLet s term -> case typeOf gamma term of Left msg -> (out ++ "type error: " ++ msg ++ "\n", env) Right t -> (out ++ "[" ++ s ++ ":" ++ show t ++ "]\n", ((s, t):gamma, (s, term):lets)) reset resetB `onEvent` Click $ const reset pairB `onEvent` Click $ const $ getProp pairP "value" >>= setProp iEl "value" >> setProp oEl "value" "" surB `onEvent` Click $ const $ getProp surP "value" >>= setProp iEl "value" >> setProp oEl "value" "" evalB `onEvent` Click $ const $ do es <- map (parse line "") . lines <$> getProp iEl "value" setProp oEl "value" $ fst $ foldl' run ("", ([], [])) es #else repl env@(gamma, lets) = do let redo = repl env ms <- getInputLine "> " case ms of Nothing -> outputStrLn "" Just s -> do case parse line "" s of Left err -> do outputStrLn $ "parse error: " ++ show err redo Right None -> redo Right (Run term) -> case typeOf gamma term of Left msg -> outputStrLn ("type error: " ++ msg) >> redo Right t -> do outputStrLn $ "[type = " ++ show t ++ "]" outputStrLn $ show $ norm env term redo Right (TopLet s term) -> case typeOf gamma term of Left msg -> outputStrLn ("type error: " ++ msg) >> redo Right t -> do outputStrLn $ "[type = " ++ show t ++ "]" repl ((s, t):gamma, (s, term):lets) main = repl ([], []) #endif

## Booleans, Integers, Pairs, Lists

Hindley-Milner supports Church-encodings of booleans, integers, pairs, and lists. System F is more general, so of course supports them too. However, we must be explicit about types. With Hindley-Milner, globally scoped universal quantifiers for all type variables are implied. With System F, our terms must start with type abstractions or a term abstraction annotated with a universal type:

true = \X x:X y:X.x false = \X x:X y:X.y not = \b:forall X.X->X->X X t:X f:X.b [X] f t 0 = \X s:X->X z:X.z succ = \n:(forall X.(X->X)->X->X) X s:X->X z:X.s(n[X] s z) pair = \X Y x:X y:Y Z f:X->Y->Z.f x y fst = \X Y p:forall Z.(X->Y->Z)->Z.p [X] (\x:X y:Y.x) snd = \X Y p:forall Z.(X->Y->Z)->Z.p [Y] (\x:X y:Y.y) nil = \X.(\R.\c:X->R->R.\n:R.n) cons = \X h:X t:forall R.(X->R->R)->R->R.(\R c:X->R->R n:R.c h (t [R] c n))

## Apply yourself!

In our previous systems, the term `\x.x x`

has been untypable. No longer!
Self-application can be expressed in System F:

\x:forall X.X->X.x[forall X.X->X] x

Of course, self-application of self-application (`(\x.x x)(\x.x x)`

) remains
untypable, because it has no normal form.

## Information hiding

It turns out universal types can represent *existential types*.
These types can enforce information hiding. For example, we can give
the programmer access to an API but forbid access to the implementation
details.

Knowledge is power. Languages with simpler type systems still benefit if their designers know System F. For example, Haskell 98 is strictly Hindley-Milner, but researchers exploited existential types to design and prove theorems about a language extension enabling the ST monad.

## System F in System F

The polymorphic identity function is typable in System F, hence we can
construct the self-interpreter described in
*Breaking Through the
Normalization Barrier: A Self-Interpreter for F-omega* by Matt Brown and Jens
Palsberg.

E=\T q:(forall X.X->X)->T.q(\X x:X.x)

As we demonstrated for the shallow encoding of untyped lambda calculus terms, the trick is to block every application (of types or terms) by adding one more layer of abstraction. The evaluation proceeds once we instantiate the abstraction with the polymorphic identity function.

Since we must specify types in System F, computing even a shallow encoding involves type checking.

shallow gamma term = (Forall "_0" (TV "_0" :-> TV "_0") :-> t, Lam ("id", Forall "X" (TV "X" :-> TV "X")) q) where (t, q) = f gamma term where f gamma term = case term of Var s -> (ty, Var s) where Just ty = lookup s gamma App m n -> (tn, App (App (TApp (Var "id") tm) qm) qn) where (tm, qm) = f gamma m (tn, qn) = f gamma n Lam (s, ty) t -> (ty :-> tt, Lam (s, ty) qt) where (tt, qt) = f ((s, ty):gamma) t TLam s t -> (Forall s tt, TLam s qt) where (tt, qt) = f gamma t TApp x ty -> (beta t, TApp (App (TApp (Var "id") tx) q) ty) where (tx@(Forall s t), q) = f gamma x beta (TV v) | s == v = ty | otherwise = TV v beta (Forall u v) | s == u = Forall u v | u `elem` fvs = let u1 = newName u fvs in Forall u1 $ beta $ tRename u u1 v | otherwise = Forall u $ beta v beta (m :-> n) = beta m :-> beta n fvs = tfv [] ty Let s t u -> f ((s, fst $ f gamma t):gamma) $ beta (s, t) u

Why, then, do books and papers claim self-interpreters are impossible for a strongly normalizing language? It turns out the definition of "self-interpreter" varies.

*blynn@cs.stanford.edu*💡