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

{-# LANGUAGE CPP #-}
#ifdef __HASTE__
import Haste.DOM
import Haste.Events
#else
#endif
import Control.Arrow
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  ## Parsing With 3 different abstractions, we must tread carefully. Different conventions exist for denoting them:  Term -> Term $$\lambda x:T$$ $$\lambda x:T$$ Type -> Term $$\lambda X::K$$ $$\Lambda t:K$$ Type -> Type $$\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. 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)  ## 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 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 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.

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

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.

Ben Lynn blynn@cs.stanford.edu 💡