"Optimal reduction" implemented with ST monad

INet.hs

module INet where

import Data.STRef
import Control.Monad.ST

-- This kind of implementation of optimal reduction 
-- accumulates control nodes (Croissants and brackets)
--
-- I'd guess the reason for that is that it's lacking essential structure.
-- Adding a "box" around the exponential solves the problem, but also removes the optimality.
--
-- I suppose that's not a problem for normalising linear logic,
-- but it's tricky to implement the "box" around exponential as well.

data (Tm a)
    = Link a
    | Drop
    | Fan Int (Tm a) (Tm a)
    | Crois Int (Tm a)
    | Brack Int (Tm a)
    deriving (Show, Eq)

newtype Box s = Box (STRef s (Either Int (Tm (Box s))))

eval :: [Box s] -> Tm Int -> Tm (Box s)
eval env (Link i) = Link (env !! i)
eval env Drop = Drop
eval env (Fan n x y) = Fan n (eval env x) (eval env y)
eval env (Crois n x) = Crois n (eval env x)
eval env (Brack n x) = Brack n (eval env x)

blank :: ST s (Box s)
blank = Box `fmap` newSTRef (Left (-1))

fresh :: Int -> ST s [Box s]
fresh n = sequence (replicate n blank)

type Cuts s = [(Tm (Box s), Tm (Box s))]

cut :: Tm (Box s) -> Tm (Box s) -> ST s (Cuts s)
cut x y = if depth x <= depth y
    then slice x y
    else slice y x

slice :: Tm (Box s) -> Tm (Box s) -> ST s (Cuts s)
slice (Link (Box ref)) y = do
    state <- readSTRef ref
    case state of
        Left _ -> writeSTRef ref (Right y) >> pure []
        Right x -> pure [(x,y)]
slice Drop (Fan _ x y) = pure [(Drop,x), (Drop,y)]
slice Drop (Crois _ x) = pure [(Drop,x)]
slice Drop (Brack _ x) = pure [(Drop,x)]
slice (Fan n x y) (Fan m z w) | (n == m) = pure [(x,z), (y,w)]
slice (Fan n x y) (Fan m z w) = do
    a <- fmap Link blank
    b <- fmap Link blank
    c <- fmap Link blank
    d <- fmap Link blank
    pure [(x,Fan m a b),
          (y,Fan m c d),
          (Fan n a c,z),
          (Fan n b d,w)]
slice (Fan n x y) (Crois m z) = do
    a <- fmap Link blank
    b <- fmap Link blank
    pure [(x,Crois m a),
          (y,Crois m b),
          (Fan n a b,z)]
slice (Fan n x y) (Brack m z) = do
    a <- fmap Link blank
    b <- fmap Link blank
    pure [(x,Brack m a),
          (y,Brack m b),
          (Fan n a b,z)]
slice (Crois n x) (Crois m y) | (n == m) = pure [(x,y)]
slice (Crois n x) p = commute x (\a -> (a-1)) (Crois n) p
slice (Brack n x) (Brack m y) | (n == m) = pure [(x,y)]
slice (Brack n x) p = commute x (+1) (Brack n) p

commute :: Tm (Box s)
     -> (Int -> Int)
     -> (Tm (Box s) -> Tm (Box s))
     -> Tm (Box s)
     -> ST s [(Tm (Box s), Tm (Box s))]
commute x f g (Fan m z w) = do
    a <- fmap Link blank
    b <- fmap Link blank
    pure [(x,Fan (f m) a b), (g a,z), (g b,w)]
commute x f g (Crois m y) = do
    a <- fmap Link blank
    pure [(x,Crois (f m) a), (g a,y)]
commute x f g (Brack m y) = do
    a <- fmap Link blank
    pure [(x,Brack (f m) a), (g a,y)]

depth :: Tm a -> Int
depth (Link _) = -2
depth Drop     = -1
depth (Fan n _ _) = n
depth (Crois n _) = n
depth (Brack n _) = n

readback :: Tm (Box s) -> Int -> ST s (Tm Int, Int)
readback (Link (Box ref)) n = do
    state <- readSTRef ref
    case state of
        (Left (-1)) -> writeSTRef ref (Left n) >> pure (Link n, n+1)
        (Left i)    -> pure (Link i, n)
        (Right x)   -> readback x n
readback Drop m = pure (Drop, m)
readback (Fan n x y) m0 = do
    (x', m1) <- readback x m0
    (y', m2) <- readback y m1
    pure (Fan n x' y', m2)
readback (Crois n x) m0 = do
    (x', m1) <- readback x m0
    pure (Crois n x', m1)
readback (Brack n x) m0 = do
    (x', m1) <- readback x m0
    pure (Brack n x', m1)