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 -> "∀" ++ 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 -> "λ" ++ 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) = "λ" ++ 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) = "λ" ++ 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 ((\(a,b) -> (b,a)) <$> 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 type-level function.
We introduce simply-typed lambda calculus at the level of types. We
have operator abstractions and operator applications. We say kind for
the type of a type-level lambda expression, and define the base kind *
for proper types that is, the types of (term-level) 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
simply-typed 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 type-level let expression.
jsEval "curl_module('../compiler/Charser.ob')"
import Charser
data FOmegaLine = Blank | Typo String Type
| TopLet String Term | Run Term deriving Show
line = between ws eof $ typo <|>
TopLet <$> v <*> (str "=" *> term) <|> Run <$> term <|> pure Blank 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 "λ"
lam1 = str "."
lam = flip (foldr ($)) <$> between lam0 lam1 (some bind) <*> term where
bind = (&) <$> v <*>
( str "::" *> ((\k s -> TLam (s, k)) <$> kin)
<|> str ":" *> ((\t s -> Lam (s, t)) <$> typ)
<|> pure (\s -> TLam (s, Star))
)
typ = olam <|> fun
olam = flip (foldr OLam) <$> between lam0 lam1 (some vk) <*> typ
fun = oapp `chainr1` (const (:->) <$> str "->")
oapp = foldl1 OApp <$> some (forallt <|> (TV <$> v)
<|> between (str "(") (str ")") typ)
forallt = flip (foldr Forall) <$> between fa0 fa1 (some vk) <*> typ where
fa0 = str "forall" <|> str "∀"
fa1 = str "."
vk = (,) <$> v <*> (str "::" *> kin <|> pure Star)
kin = ((str "*" *> pure Star) <|> between (str "(") (str ")") kin)
`chainr1` (const (:=>) <$> str "->")
app = termArg >>= moreArg
termArg = (Var <$> v) <|> between (str "(") (str ")") term
moreArg t = ((App t <$> termArg
<|> TApp t <$> between (str "[") (str "]") typ) >>= moreArg) <|> pure t
v = do
s <- some alphaNumChar
when (s `elem` words "let in forall typo") $ Charser $ const $ Left $ "unexpected " ++ s
ws
pure s
str = (<* ws) . string
ws = space *> (string "--" *> many (sat $ const True) *> pure () <|> pure ())
chainr1 p op = go id where
go d = do
x <- p
(op >>= \f -> go (d . (f x:))) <|> pure (foldr ($) x $ d [])
Type-level lambda calculus
In System F, for type-checking, we needed a beta-reduction which substitued a given type variable with a given type value.
This time, this routine is used to build a type-level 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 (\c -> '0' <= c && c <= '9') 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 well-kinded 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.
eval = do
es <- map (parse line "") . lines <$> jsEval "input.value;"
jsEval $ "output.value = `" ++ run [] [] [] es "" ++ "`;"
where
run lets types kinds = \case
[] -> id
h:t -> let next = run lets types kinds t in case h of
Left err -> ("parse error: "++) . shows err . ("\n"++) . next
Right m -> case m of
Blank -> next
Run term -> case typeOf (types, kinds) term of
Left m -> ("type error: "++) . shows term . (": "++) .
(m++) . ("\n"++) . next
Right _ -> shows (norm (lets, types) term) . ("\n"++) . next
Typo s typo -> case kindOf (types, kinds) typo of
Left m -> ("kind error: "++) . shows typo . (": "++) .
(m++) . ("\n"++) . next
Right k -> ("["++) . (s++) . (":"++) .
shows (tNorm (types, kinds) typo) . ("]\n"++) .
run lets ((s, typo):types) ((s, k):kinds) t
TopLet s term -> case typeOf (types, kinds) term of
Left m -> ("type error: "++) . shows term . (": "++) .
(m++) . ("\n"++) . next
Right x -> ("["++) . (s++) . (":"++) . shows x . ("]\n"++) .
run ((s, term):lets) ((s, x):types) kinds t
jsEval [r|
evalB.addEventListener("click", (ev) => { repl.run("chat", ["Main"], "eval"); });
|]
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 self-interpreter and more, though still stops short of a self-reducer.
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.