Typechecking for Classical Linear Logic sequents

This post contains a type checker for classical linear logic sequents, written in Haskell.

Lets start by encoding types.

data Ty
    = Terminal | Initial | TensorUnit | ParUnit
    | Prod Ty Ty | Sum Ty Ty | Tensor Ty Ty | Par Ty Ty
    | OfCourse Ty | WhyNot Ty
    | Pos Int | Neg Int
    deriving (Show, Eq)

These types can be grouped into additives, multiplicatives and exponentials. The main property of this type system is that every type has a de-morgan dual.

dual :: Ty -> Ty
dual Terminal = Initial
dual TensorUnit = ParUnit
dual (Prod x y) = Sum (dual x) (dual y)
dual (Sum x y) = Prod (dual x) (dual y)
dual (Tensor x y) = Par (dual x) (dual y)
dual (Par x y) = Tensor (dual x) (dual y)
dual (OfCourse x) = WhyNot (dual x)
dual (WhyNot x) = OfCourse (dual x)
dual (Pos i) = (Neg i)
dual (Neg i) = (Pos i)

The duality extends to sequents as well. If you have a sequent that is a proof for some proposition, then it's a refutation for the dual proposition.

polarity :: Ty -> Bool
polarity Initial      = True
polarity TensorUnit   = True
polarity (Prod _ _)   = True
polarity (Tensor _ _) = True
polarity (OfCourse _) = True
polarity (Pos _)      = True
polarity Terminal     = False
polarity ParUnit      = False
polarity (Sum _ _)    = False
polarity (Par _ _)    = False
polarity (WhyNot _)   = False
polarity (Neg _)      = False

Polarity isn't too important for typechecking, but it appears to be useful for evaluating terms.

Now we'd have to encode the CLL sequents as terms. It can help if you notice that these sequents have lot of redundant structure which means that some of them can slide past each other. This allows dividing inference steps to "positive" and "negative".

data Tm
    = Cut Ty Tm Tm
    | Pair Tm Tm
    | Opt Tm Tm
    | Exp Tm
    | Tt
    | Ax
    | Absurd Int
    | Sr [Tn] Tm
    deriving (Show, Eq)

data Tn
    = Drop
    | Dup Tn Tn
    | Inst Tn
    | Var Int
    | Ff
    | Inl Tn
    | Inr Tn
    | Split Tn Tn
    deriving (Show, Eq)

Positive terms introduce some structure or "control flow" whereas negative terms behave like signals.

I'm going to explain what these structures mean when introducing typechecking. For now notice that even although if you removed the "Cut" this structure would not represent a normal form because some terms here can still slide past each other.

Type checking

Every "Tm" represents a sequent with a context. Therefore these structures have an arity.

arity :: Tm -> Int
arity (Sr ctx _)  = length ctx
arity (Cut _ a b) = arity a + arity b - 2
arity (Pair a b)  = arity a + arity b - 1
arity (Opt a b)   = arity a
arity (Exp a)     = arity a
arity Tt = 1
arity Ax = 2
arity (Absurd n) = n

Arity is either fixed, or then it's a sum of the composed sequents. In Cut two variables are eliminated so the arity decreases by 2. In Pair two variables are combined, so arity decreases by 1. Opt arity is measured from left side and the result of this function is only correct if the term is valid.

Type checking takes a type for every variable in the context and decides whether a term forms a valid proof for the proposition that the type stands for.

check :: [Ty] -> Tm -> Bool
check env (Sr ctx a)
    = case infer_env env ctx (init_ctx (arity a)) >>= full of
        Just env' -> check env' a
        Nothing   -> False
check env (Cut ty a b) = let
    (env1, env2) = splitAt (arity a-1) env
    in check (ty:env1) a && check (dual ty:env2) b
check (Tensor x y:env) (Pair a b) = let
    (env1, env2) = splitAt (arity a-1) env
    in check (x:env1) a && check (y:env2) b
check (Prod x y:env) (Opt a b)  = check (x:env) a && check (y:env) b
check (OfCourse ty:env) (Exp a) = all is_whynot env && check (ty:env) a
check [TensorUnit] Tt           = True
check [t,v]        Ax = polarity v && (dual t == v)
check env (Absurd n)  = any terminal_present env && (length env == n)
check _   _           = False

infer_env :: [Ty] -> [Tn] -> [Maybe Ty] -> Maybe [Maybe Ty]
infer_env []       []     ctx = Just ctx
infer_env (ty:tys) (x:xs) ctx = infer ty x ctx >>= infer_env tys xs
infer_env _        _      _   = Nothing

infer :: Ty -> Tn -> [Maybe Ty] -> Maybe [Maybe Ty]
infer ty            (Var n)     ctx = edit_ctx n ty ctx
infer (WhyNot _)    Drop        ctx = Just ctx
infer ty@(WhyNot _) (Dup x y)   ctx = infer ty x ctx >>= infer ty y
infer (WhyNot ty)   (Inst x)    ctx = infer ty x ctx
infer ParUnit       Ff          ctx = Just ctx
infer (Sum a _)     (Inl x)     ctx = infer a x ctx
infer (Sum _ b)     (Inr y)     ctx = infer b y ctx
infer (Par a b)     (Split x y) ctx = infer a x ctx >>= infer b y
infer _             _           _   = Nothing

I threw that all out at once since it ended up being fairly short. Now explaining these structures.

Sr restructures the context and constructs terms corresponding to negative types.
Cut eliminates two variables that are dual to each other. The variables must appear in opposite contexts that are then merged.
Pair constructs a tensor by pairing two variables.
Opt constructs an option that's resolved by a suitable sum type.
Exp constructs anything that can be duplicated and erased.
Tt constructs a tensor unit.
Ax eliminates two variables but in an another direction.
Absurd can be used when there's a structure in context that cannot be constructed.

The Drop,Dup,Inst provide counterparts for the Exp, Likewise Inl,Inr counterpart the Opt. Ff forms a par unit to counterpart the tensor unit. Likewise Split is counterpart for the Pair.

The context-handling ensures that variables are used up exactly once.

init_ctx :: Int -> [Maybe Ty]
init_ctx n = replicate n Nothing

edit_ctx :: Int -> Ty -> [Maybe Ty] -> Maybe [Maybe Ty]
edit_ctx 0 ty (Nothing:xs) = Just (Just ty:xs)
edit_ctx n ty (x:xs) = (x:) `fmap` edit_ctx (n-1) ty xs
edit_ctx _ _ _ = Nothing

full :: [Maybe a] -> Maybe [a]
full []          = Just []
full (Just x:xs) = (x:) `fmap` full xs
full _           = Nothing

The Absurd and Exp requires that the context is constrained in a certain way.

is_whynot :: Ty -> Bool
is_whynot (WhyNot _) = True
is_whynot _ = False

terminal_present :: Ty -> Bool
terminal_present Terminal = True
terminal_present (Opt a b) = terminal_present a || terminal_present b
terminal_present (Par a b) = terminal_present a || terminal_present b
terminal_present (WhyNot a) = terminal_present a
terminal_present _ = False

Now we should be able to typecheck some sequents. Lets try the SKI combinators.

i_type = [Par (OfCourse (Neg 0)) (WhyNot (Pos 0))]
i_prog = [Split (Var 0) (Var 1)] `Sr` Exp ([Var 0, Inst (Var 1)] `Sr` Ax)

k_type = [Par (Par (OfCourse (Neg 0)) (WhyNot (Pos 1))) (WhyNot (Pos 0))]
k_prog = [Split (Split (Var 0) (Var 1)) (Var 2)] `Sr` Exp
    ([Var 0, Drop, Inst (Var 1)] `Sr` Ax)

s_type = [Par (Par (Par (OfCourse (Neg 2))
    (WhyNot (Pos 0)))
    (WhyNot (Tensor (Pos 1) (Neg 0))))
    (WhyNot (Tensor (Tensor (Pos 2) (Neg 1)) (Neg 0)))]
s_prog = [Split (Split (Split (Var 0) (Var 1)) (Var 2)) (Var 3)] `Sr` Exp
    ([Var 1, Dup (Inst (Var 3)) (Inst (Var 4)), Inst (Var 2), Inst (Var 0)] `Sr` 
        Pair 
            (Pair ([Var 1, Var 0] `Sr` Ax)
                  ([Var 1, Var 0, Var 2] `Sr` Pair
                      ([Var 1, Var 0] `Sr` Ax)
                      Ax))
            Ax)

Next it'd be time to consider how to normalise these structures.

Evaluation with MVars

There's a paper that implements interaction nets with haskell's MVars.

The evaluation involves translating from types into semantic values. We are building this kind of a communication "protocol" that passes mutable variables around and labels them.

data Sem = Nil | Cons (MVar Sem) (MVar Sem) | X (MVar Sem) | Y (MVar Sem)

We pick sequences of empty variables and treat them as the execution environment.

blank_env :: Int -> IO [MVar Sem]
blank_env n = mapM id (replicate n newEmptyMVar)

Evaluation takes a term and interprets it in the given environment. Positive terms become "actors" that interface through mutable variables. They are activated through eval.

eval :: Tm -> [MVar Sem] -> IO ()

Ax is like a schoolboy, what goes from one ear in goes out from another.

eval Ax [dst,src] = do
    forkIO (readMVar src >>= putMVar dst)
    pure ()

Tt is also like a schoolboy, well, in an another way. It's doing nothing.

eval Tt [src] = do
    forkIO (readMVar src >>= const (pure ()))
    pure ()

Sr sends negative terms as "messages".

eval (Sr ctx a) env = do
    env' <- plug_ctx ctx env (init_box (arity a))
    eval a env'

Put two schoolboys ear-to-ear and you can route information around. Thats what Cut is for.

eval (Cut _ a b) env = do
    let (env1, env2) = splitAt (arity a) env
    k <- newEmptyMVar
    eval a (k:env1)
    eval b (k:env2)

Pair splits a cake.

eval (Pair a b) (p:env) = do
    let (env1, env2) = splitAt (arity a) env
    forkIO $ do
        Cons p1 p2 <- readMVar p
        eval a (p1:env1)
        eval b (p2:env2)
    pure ()

Option selects a branch.

eval (Opt a b) (p:env) = do
    forkIO $ do
        i <- readMVar p
        case i of
            X x -> eval a (x:env)
            Y y -> eval b (y:env)
    pure ()

Exponents are things that are cheap to copy around.

eval (Exp a) (p:env) = do
    forkIO (exponent_impl p env)
    pure ()
    where
        n = arity a
        exponent_impl q e = do
            i <- readMVar q
            case i of
                X x -> eval a (x:env)
                Cons x y -> do
                    e1 <- blank_env n
                    e2 <- blank_env n
                    mapM_ id (zipWith putMVar e (zipWith Cons e1 e2))
                    exponent_impl x e1
                    exponent_impl y e2
                Nil -> mapM_ (\m -> putMVar m Nil) e

Finally we have things that aren't activated because valid environment cannot be built for them.

eval (Absurd _) env = undefined

Negative types manifest as different kind of messages that are sent around. The Drop becomes Nil, Inst n becomes X n. Likewise Inl x and Inr y become X x and Y y. Split x y can be thought of as a way to "open" a pair.

plug_ctx :: [Tn] -> [MVar Sem] -> [MVar Sem] -> IO [MVar Sem]
plug_ctx []     []     box = pure box
plug_ctx (x:xs) (v:vs) box = plug x v box >>= plug_ctx xs vs

plug :: Tn -> MVar Sem -> [MVar Sem] -> IO [MVar Sem]
plug (Var n)   v box = pure (edit_box n v box)
plug Drop      v box = putMVar v Nil >> pure box
plug (Dup x y) v box = do
    a <- newEmptyMVar
    b <- newEmptyMVar
    putMVar v (Cons a b)
    plug x a box >>= plug y b
plug (Inst x)  v box = do
    a <- newEmptyMVar
    putMVar v (X a)
    plug x a box
plug Ff v box      = putMVar v Nil >> pure box
plug (Inl x) v box = do
    a <- newEmptyMVar
    putMVar v (X a)
    plug x a box
plug (Inr y) v box = do
    b <- newEmptyMVar
    putMVar v (Y b)
    plug y b box
plug (Split x y) v box = do
    a <- newEmptyMVar
    b <- newEmptyMVar
    putMVar v (Cons a b) 
    plug x a box >>= plug y b

When "plugging" values into a context, we construct a structure that isn't filled and would cause the program to crash if it was accessed before it was filled.

init_box :: Int -> [a]
init_box n = replicate n undefined

edit_box :: Int -> a -> [a] -> [a]
edit_box 0 v (_:xs) = (v:xs)
edit_box n v (x:xs) = (x:edit_box (n-1) v xs)
edit_box n v []     = [v]

So that's an evaluator.

I think it'd be possible to turn this evaluator into a normalizer, but it'd be fairly unappealing and would correspond to running the program with every variation of input it can react to.

Serving suggestion

Another thing I didn't do, I didn't try this out. But I think it can be a fun thing. It's like a functional programming environment but you can give types for interactions.

For example, echo -program would be:

echo :: Stream `Par` ~Stream

You can model the communication by stacking up interactions. Eg. the Stream would be:

Stream = Sum TensorUnit (Opt TensorUnit (TextBlock `Tensor` Stream))

To implement a "Stream", you'd send signal of whether you're closed or not, then prepare for either closing or then continue producing results.

Note that such notion of a stream could be entirely denotational. The type isn't saying which stream it is, and if you get something to implement the type, you can treat it as a stream.

I'd think you can implement the evaluator in Javascript. Build the "communication protocol" from promises.

Also it's a fairly fun program representation and you don't need to leave traditional functional programming style behind, typed lambda calculus translates in several ways into classical linear logic.

Download link

You can download CLL.hs and try it out. It's embedded in this blogpost.

The type checker is about 130 lines.

Concluding remarks

Optimal reduction could be a nice algorithm for evaluating and normalizing classical linear logic sequents but it has the problem of accumulating control operators, Garbage nodes, croissants and brackets, that eventually clog up the reduction. The algorithm likely removes something it should keep along during the reduction.

Building models like these maybe reveals what optimal reduction would need in order to collect its garbage nodes.