{# 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.