Concurrently running linearly typed experiment.

LC.hs

{-# LANGUAGE FlexibleInstances #-}
module LC where

import Control.Monad.Cont
import Control.Monad (guard)
import Control.Concurrent
import Data.Bifunctor (bimap)

-- Interface to retrieve a boolean and then produce a boolean.
interface1 :: FT
interface1 = Sum interface2 interface2

interface2 :: FT
interface2 = prod Unit Unit
interface2_id = Cur (Ap Counit (Sum (Exp Counit Unit) (Exp Counit Unit)))

console_impl :: Cont (IO ()) (Sem (IO ()))
console_impl = do
    state <- plug_io getLine
    case state of
        "False" -> pure (X (Fun (>>=printout_impl)))
        "True"  -> pure (Y (Fun (>>=printout_impl)))
        _       -> error "no parse"
    where printout_impl :: Sem (IO ()) -> Cont (IO ()) (Sem (IO ()))
          printout_impl (X (Fun f)) = do
              plug_io (putStrLn "» False")
              f (pure Nil)
          printout_impl (Y (Fun f)) = do
              plug_io (putStrLn "» True")
              f (pure Nil)

plug_io :: IO a -> Cont (IO b) a
plug_io iofn = cont (iofn >>=)

-- Test program that should validate against the IO interface.
test_program1 :: NT
test_program1 = Alt
    (choice Inl)
    (choice Inr)
test_program1_valid = fmap snd (is_valid test_program1) == Just interface1

test_program2 :: NT
test_program2 = Alt
    (choice Inr)
    (choice Inl)
test_program2_valid = fmap snd (is_valid test_program2) == Just interface1

other_nop :: NT
other_nop = Delr Unit `Comp` Exch Unit Unit `Comp` Insr Unit

test1 = runCont (console_impl >>= eval test_program1) (const (pure ()))
test2 = runCont (console_impl >>= eval test_program2) (const (pure ()))
test3 = runCont (console_impl >>= eval test_program2 >>= eval other_nop) (const (pure ()))
test4 = runCont
    (pure (Cons console_impl console_impl) >>= eval (Delr Unit `Comp` Split test_program1 test_program2))
    (const (pure ()))

choice fn = CallCC Unit
              `Comp` Cur (Ap Counit (Sum (Exp Counit Unit) (Exp Counit Unit))
                          `Comp` Split
                             interface2_id
                             (fn (Exp Counit Unit) (Exp Counit Unit)))

data Sem r
    = Nil
    | Box (Cont r (Sem r))
    | Cons (Cont r (Sem r)) (Cont r (Sem r))
    | Fun (Cont r (Sem r) -> Cont r (Sem r))
    | X (Sem r)
    | Y (Sem r)

class Eval r where
    delr :: Cont r (Sem r) -> Cont r (Sem r) -> Cont r (Sem r)

instance Eval (IO ()) where
    delr x y = plug_io (forkIO (runCont y (const (pure ())))) >> x

eval :: Eval r => NT -> Sem r -> Cont r (Sem r)
eval (Id _)       x = pure x
eval (Nop)        Nil = pure Nil
eval (Insr _)     x = pure (Cons (pure x) (pure Nil))
eval (Delr _)     (Cons x y) = delr x y
eval (Exch _ _)   (Cons x y) = pure (Cons y x)
eval (Assl _ _ _) (Cons x w) = do
    Cons y z <- w
    pure (Cons (pure (Cons x y)) z)
eval (Split f g)  (Cons x y) = pure (Cons (x >>= eval f) (y >>= eval g))
eval (Cur f)      x = pure (Fun (\y -> eval f (Cons (pure x) y)))
eval (Ap _ _)     (Cons x y) = do
    Fun f <- x
    f y
eval (Alt f g)    (X x) = eval f x
eval (Alt f g)    (Y x) = eval g x
eval (Inl _ _)    x = pure (X x)
eval (Inr _ _)    x = pure (Y x)
eval (Dupl f)     x = pure (Box (eval f x))
eval (Extr _)     (Box x) = x
eval (Copy _)     x = pure (Cons (pure x) (pure x))
eval (Drop _)     x = pure Nil
eval (Comp f g)   x = eval g x >>= eval f
eval (CallCC _)   (Fun f) = callCC (\g -> f (pure (Fun (\x -> x >>= g))))
eval foo          Nil        = error (show foo ++ ": NIL dunno")
eval foo          (Cons _ _) = error (show foo ++ ": CONS dunno")
eval foo          (Fun _)    = error (show foo ++ ": FUN dunno")
eval foo          (X _)      = error (show foo ++ ": X dunno")
eval foo          (Y _)      = error (show foo ++ ": Y dunno")

data FT
    = Var Int
    | Unit
    | Counit       -- Dualizing object, not certain if counit
    | Tensor FT FT
    | Exp FT FT
    | Sum FT FT
    | Ofc FT
    deriving (Show, Eq)

par :: FT -> FT -> FT
par x y = Exp Counit (Tensor (Exp Counit x) (Exp Counit y))

prod :: FT -> FT -> FT
prod x y = Exp Counit (Sum (Exp Counit x) (Exp Counit y))

whynot :: FT -> FT
whynot x = Exp Counit (Ofc (Exp Counit x))

data NT
    = Id Int          -- a → a
    | Nop             -- I → I
    | Insr FT         -- A → A ⊗ I
    | Delr FT         -- A ⊗ I → A
    | Exch FT FT      -- A ⊗ B → B ⊗ A
    | Assl FT FT FT   -- A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C
    | Split NT NT     -- a ⊗ b
    | Cur NT          -- a → (a ⊗ b) ^ b
    | Ap FT FT        -- (a ^ b) ⊗ b → a
    | Alt NT NT       -- a+a → a
    | Inl FT FT       -- a → a+b
    | Inr FT FT       -- b → a+b
    | Dupl NT         -- a → !a where 'a' is compat.
    | Extr FT         -- !a → a
    | Copy FT         -- !a → !a ⊗ !a
    | Drop FT         -- !a → I
    | Comp NT NT      -- x.y
    | CallCC FT       -- U^(U^A) → A
    deriving (Show, Eq)

is_valid :: NT -> Maybe (FT, FT)
is_valid (Id i) = pure (Var i, Var i)
is_valid (Nop)  = pure (Unit, Unit)
is_valid (Insr x) = pure (Tensor x Unit, x)
is_valid (Delr x) = pure (x, Tensor x Unit)
is_valid (Exch x y) = pure (Tensor y x, Tensor x y)
is_valid (Assl x y z) = pure (Tensor (Tensor x y) z, Tensor x (Tensor y z))
is_valid (Split f g) = do
    (x',x) <- is_valid f
    (y',y) <- is_valid g
    pure (Tensor x' y', Tensor x y)
is_valid (Cur f) = do
    (x',x) <- is_valid f
    case x of
        Tensor y z -> pure (Exp x' z, y)
        _          -> Nothing
is_valid (Ap x y) = do
    pure (x, Tensor (Exp x y) y)
is_valid (Alt f g) = do
    (x',x) <- is_valid f
    (y',y) <- is_valid g
    guard (x' == y')
    pure (x', Sum x y)
is_valid (Inl x y) = do
    pure (Sum x y, x)
is_valid (Inr x y) = do
    pure (Sum x y, y)
is_valid (Dupl f) = do
    (x',x) <- is_valid f
    guard (is_dupl x)
    pure (Ofc x', x)
is_valid (Extr x) = do
    pure (x, Ofc x)
is_valid (Copy x) = do
    guard (is_dupl x)
    pure (Tensor x x, x)
is_valid (Drop x) = do
    guard (is_dupl x)
    pure (Unit, x)
is_valid (Comp f g) = do
    (x',x) <- is_valid f
    (y',y) <- is_valid g
    guard (x == y')
    pure (x', y)
is_valid (CallCC x) = do
    pure (x, Exp Counit (Exp Counit x))

is_dupl :: FT -> Bool
is_dupl Unit = True
is_dupl (Tensor x y) = is_dupl x && is_dupl y
is_dupl (Sum x y) = is_dupl x && is_dupl y
is_dupl (Ofc _) = True
is_dupl _ = False