{# LANGUAGE CPP #} #ifdef __HASTE__ import Haste.DOM import Haste.Events #else import System.Console.Haskeline #endif import Control.Arrow import Control.Monad import Data.Char import Data.Function import Data.List import Data.Tuple import Text.Parsec data Kind = Star  Kind :=> Kind deriving Eq data Type = TV String  Forall (String, Kind) Type  Type :> Type  OLam (String, Kind) Type  OApp Type Type data Term = Var String  App Term Term  Lam (String, Type) Term  Let String Term Term  TLam (String, Kind) Term  TApp Term Type instance Show Kind where show Star = "*" show (a :=> b) = showA ++ ">" ++ show b where showA = case a of _ :=> _ > "(" ++ show a ++ ")" _ > show a showK Star = "" showK k = "::" ++ show k instance Show Type where show ty = case ty of TV s > s Forall (s, k) t > '\8704':s ++ showK k ++ "." ++ show t t :> u > showL ++ " > " ++ showR where showL = case t of Forall _ _ > "(" ++ show t ++ ")" _ :> _ > "(" ++ show t ++ ")" _ > show t showR = case u of Forall _ _ > "(" ++ show u ++ ")" _ > show u OLam (s, k) t > '\0955':s ++ showK k ++ "." ++ show t OApp t u > showL ++ showR where showL = case t of TV _ > show t OApp _ _ > show t _ > "(" ++ show t ++ ")" showR = case u of TV _ > ' ':show u _ > "(" ++ 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, k) t) = "\0955" ++ s ++ showK k ++ showB t where showB (TLam (s, k) t) = " " ++ s ++ showK k ++ 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 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, ks) x) (Forall (t, kt) y)  ks /= kt = False  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
Type operators
In Haskell, Map Integer String
describes a map of integers to strings.
Thus Map
is an example of a type operator, because it takes 2 types and
returns a type.
GHC has an syntax sugar extension called "type operators". We use the term differently; for us, a type operator is a typelevel function.
We introduce simplytyped lambda calculus at the level of types. We
have operator abstractions and operator applications. We say kind for
the type of a typelevel lambda expression, and define the base kind *
for proper types that is, the types of (termlevel) lambda expressions.
For example, the Map
type constructor has kind * > * > *
. No term
has type Map
. The Integer
and String
types both have kind *
, so
Map Integer String
has kind *
and it is therefore a proper type.
Another example of a proper type is (String > Int) > String
.
When type operators are added to System F, we obtain System F_{ω}.
Definitions
Our Type
and Term
data types both have their own variables, abstractions,
and applications. The new Kind
data type holds typing information for
Type
values, and as before, Type
holds typing information for Term
values.
Because we’re extending System F, we also have Forall
, TLam
, and TApp
for functions that take types and return terms; without these, we obtain a
system known as \(\lambda\underline{\omega}\). [I don’t know much about
\(\lambda\underline{\omega}\), but because types and terms undergo beta
reduction in their own separate worlds, I sense it’s only a minor upgrade for
simplytyped lambda calculus.]
The kinding ::*
is common, so we elide it.
Parsing
With 3 different abstractions, we must tread carefully. Different conventions exist for denoting them:

\(\lambda x:T\) 
\(\lambda x:T\) 

\(\lambda X::K\) 
\(\Lambda t:K\) 

\(\lambda X::K\) 
\(\lambda t:K\) 
We use the notation in first column to avoid the uppercase lambda.
Writing \x:X y.
was previously equivalent to \x:X.\y.
but now X y
is
parsed as an operator application. One solution is write more lambdas.
We add the typo
expression, which is a typelevel let expression.
data FOmegaLine = Blank  Typo String Type  TopLet String Term  Run Term deriving Show line :: Parsec String () FOmegaLine line = between ws eof $ option Blank $ typo <> (try $ TopLet <$> v <*> (str "=" >> term)) <> (Run <$> term) where typo = Typo <$> between (str "typo") (str "=") v <*> typ term = letx <> lam <> app letx = Let <$> (str "let" >> v) <*> (str "=" >> term) <*> (str "in" >> term) lam0 = str "\\" <> str "\0955" lam1 = str "." lam = flip (foldr ($)) <$> between lam0 lam1 (many1 bind) <*> term where bind = (&) <$> v <*> option (\s > TLam (s, Star)) ( (str "::" >> (\k s > TLam (s, k)) <$> kin) <> (str ":" >> (\t s > Lam (s, t)) <$> typ)) typ = olam <> fun olam = flip (foldr OLam) <$> between lam0 lam1 (many1 vk) <*> typ fun = oapp `chainr1` (const (:>) <$> str ">") oapp = foldl1' OApp <$> many1 (forallt <> (TV <$> v) <> between (str "(") (str ")") typ) forallt = flip (foldr Forall) <$> between fa0 fa1 (many1 vk) <*> typ where fa0 = str "forall" <> str "\8704" fa1 = str "." vk = (,) <$> v <*> option Star (str "::" >> kin) kin = ((str "*" >> pure Star) <> between (str "(") (str ")") kin) `chainr1` (const (:=>) <$> str ">") 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 typo") $ fail "unexpected keyword" ws pure s str = try . (>> ws) . string ws = spaces >> optional (try $ string "" >> many anyChar)
Typelevel lambda calculus
In System F, for typechecking, we needed a betareduction which substitued a given type variable with a given type value.
This time, this routine is used to build a typelevel evaluation function that returns the weak head normal form of a type expression, which in turn is used to compute its normal form.
newName x ys = head $ filter (`notElem` ys) $ (s ++) . show <$> [1..] where s = dropWhileEnd isDigit x tBeta (s, a) t = rec t where rec (TV v)  s == v = a  otherwise = TV v rec (Forall (u, k) v)  s == u = Forall (u, k) v  u `elem` fvs = let u1 = newName u fvs in Forall (u1, k) $ rec $ tRename u u1 v  otherwise = Forall (u, k) $ rec v rec (m :> n) = rec m :> rec n rec (OLam (u, ku) v)  s == u = OLam (u, ku) v  u `elem` fvs = let u1 = newName u fvs in OLam (u1, ku) $ rec $ tRename u u1 v  otherwise = OLam (u, ku) $ rec v rec (OApp m n) = OApp (rec m) (rec n) fvs = tfv [] a tEval env (OApp m a) = let m' = tEval env m in case m' of OLam (s, _) f > tEval env $ tBeta (s, a) f where _ > OApp m' a tEval env term@(TV v)  Just x < lookup v (fst env) = case x of TV _ > x _ > tEval env x tEval _ ty = ty tNorm env ty = case tEval env ty of TV _ > ty m :> n > rec m :> rec n Forall sk t > Forall sk (rec t) OApp m n > OApp (rec m) (rec n) OLam sk t > OLam sk (rec t) where rec = tNorm env 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 tfv vs (OLam (s, _) t) = tfv (s:vs) t tfv vs (OApp x y) = tfv vs x `union` tfv vs y tRename x x1 ty = case ty of TV s  s == x > TV x1  otherwise > ty Forall (s, k) t  s == x > ty  otherwise > Forall (s, k) (rec t) OLam (s, k) t  s == x > ty  otherwise > OLam (s, k) (rec t) a :> b > rec a :> rec b OApp a b > OApp (rec a) (rec b) where rec = tRename x x1
Kind checking
We require type lambda expressions to be wellkinded to guarantee strong
normalization. Much of the code is similar to type checking for simply typed
lambda calculus. A few checks verify that proper types have base type *
.
kindOf :: ([(String, Type)], [(String, Kind)]) > Type > Either String Kind kindOf gamma t = case t of TV s  Just k < lookup s (snd gamma) > pure k  otherwise > Left $ "undefined " ++ s t :> u > do kt < kindOf gamma t when (kt /= Star) $ Left $ "Arr left: " ++ show t ku < kindOf gamma u when (ku /= Star) $ Left $ "Arr right: " ++ show u pure Star Forall (s, k) t > do k' < kindOf (second ((s, k):) gamma) t when (k' /= Star) $ Left $ "Forall: " ++ show k' pure Star OApp t u > do kt < kindOf gamma t ku < kindOf gamma u case kt of kx :=> ky > if ku /= kx then Left ("OApp " ++ show ku ++ " /= " ++ show kx) else pure ky _ > Left $ "OApp left " ++ show t OLam (s, k) t > (k :=>) <$> kindOf (second ((s, k):) gamma) t
Type checking
For App
and TApp
, we find the weak head normal form of the first argument
to check it is a suitable abstraction. In the case of App
, we compare the
normal form of the type of the abstraction binding against the normal form
of the type of the second argument to check that the application can proceed.
typeOf :: ([(String, Type)], [(String, Kind)]) > Term > Either String Type typeOf gamma t = case t of Var s  Just t < lookup s (fst gamma) > pure t  otherwise > Left $ "undefined " ++ s App x y > do tx < rec x ty < rec y case tEval gamma tx of ty' :> tz  tNorm gamma ty == tNorm gamma ty' > pure tz _ > Left $ "App: " ++ show tx ++ " to " ++ show ty Lam (x, t) y > do k < kindOf gamma t if k == Star then (t :>) <$> typeOf (first ((x, t):) gamma) y else Left $ "Lam: " ++ show t ++ " has kind " ++ show k TLam (s, k) t > Forall (s, k) <$> typeOf (second ((s, k):) gamma) t TApp x y > do tx < tEval gamma <$> rec x case tx of Forall (s, k) t > do k' < kindOf gamma y when (k /= k') $ Left $ "TApp: " ++ show k ++ " /= " ++ show k' pure $ tBeta (s, y) t _ > Left $ "TApp " ++ show tx Let s t u > do tt < rec t typeOf (first ((s, tt):) gamma) u where rec = typeOf gamma
Evaluation
We again erase types as we lazily evaluate a given term.
Because this system is getting complex, it may be better to treat type substitutions as part of the computation to verify our code works as intended. For now, we leave this as an exercise.
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 (fst 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 fvs 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 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 norm env@(lets, gamma) 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 ((v, Var v):lets, gamma) 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
Our user interface code grows uglier still, because to support let expressions, we now must maintain three association lists in the environment: one for terms, one for types, and one for kinds.
#ifdef __HASTE__ main = withElems ["input", "output", "evalB", "resetB", "resetP", "churchB", "churchP"] $ \[iEl, oEl, evalB, resetB, resetP, churchB, churchP] > 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@(lets, types, kinds)) (Right m) = case m of Blank > (out, env) Run term > case typeOf (types, kinds) term of Left msg > (out ++ "type error: " ++ msg ++ "\n", env) Right t > (out ++ show (norm (lets, types) term) ++ "\n", env) Typo s typo > case kindOf (types, kinds) typo of Left msg > (out ++ "kind error: " ++ msg ++ "\n", env) Right k > (out ++ "[" ++ show (tNorm (types, kinds) typo) ++ " : " ++ show k ++ "]\n", (lets, (s, typo):types, (s, k):kinds)) TopLet s term > case typeOf (types, kinds) term of Left msg > (out ++ "type error: " ++ msg ++ "\n", env) Right t > (out ++ "[" ++ s ++ ":" ++ show t ++ "]\n", ((s, term):lets, (s, t):types, kinds)) reset resetB `onEvent` Click $ const reset churchB `onEvent` Click $ const $ getProp churchP "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@(lets, types, kinds) = 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 Blank > redo Right (Run term) > case typeOf (types, kinds) term of Left msg > outputStrLn ("type error: " ++ msg) >> redo Right ty > do outputStrLn $ "[type = " ++ show ty ++ "]" outputStrLn $ show $ norm (lets, types) term redo Right (Typo s typo) > case kindOf (types, kinds) typo of Right k > do outputStrLn $ "[" ++ show (tNorm (types, kinds) typo) ++ " : " ++ show k ++ "]" repl (lets, (s, typo):types, (s, k):kinds) Left m > do outputStrLn m redo Right (TopLet s term) > case typeOf (types, kinds) term of Left msg > outputStrLn ("type error: " ++ msg) >> redo Right t > do outputStrLn $ "[type = " ++ show t ++ "]" repl ((s, term):lets, (s, t):types, kinds) main = runInputT defaultSettings $ repl ([], [], []) #endif
Applications
Type operators make System F less unbearable, though in our example the savings
are miniscule. We do get to write List X
once, which is nice.
Brown and Palsberg describe a representation of System F_{ω} terms which powers a selfinterpreter and more, though still stops short of a selfreducer.
Haskell’s type constructors are a restricted form of type operators. In practice, the full power of type operators is rarely needed, so we limit them to simplify type checking.
Above, we saw 3 sorts of abstraction. We’re only missing a way of feeding a term to a function and getting a type, namely dependent types. We can add these while still preserving decidable type checking and strong normalization.
However, real programming languages often support unrestricted recursion and hence it is undecidable whether a term normalizes. Adding dependent types to such a language would lead to undecidable type checking. System F_{ω} is about as far as we can go if we want unrestricted recursion and decidable type checking.