Linear abstract machine interpreter steps in Haskell

LAM.hs

-- The linear abstract machine
-- as described in the "The Linear Abstract Machine"

-- Environment is a representation of a canonical combinator
-- the canonical combinator u ⊗ v is represented by Ja, and 1 by Nil
-- the canonical combinator y ∘ v represented by Comb: y is piece of code.
--
-- Code is list of primitive instructions.
--
-- Sequential composition becomes concatenation (in opposite order),
-- but parallel composition has to be sequentialized.
-- y ∘ u becomes y ++ u (concatenation) and id becomes []
-- y ⊗ u   (=(id⊗y)∘(u⊗id)) becomes [Splitl] ++ u ++ [Consl;Splitr] ++ y [Consr]
-- 1       (=id)            becomes []
-- Splitl pushes the second component of the environment and gets to the first one,
-- whereas Consl reconstructs the pair.
-- Splitr and Consr are symmetric instructions.
-- Of course, the sequence [Consl;Splitr] can be abbreviated into a single instruction
-- Swap that exchanges the environment with the top of the stack.
--
-- For the other combinators, the translation is straightforward.

data Code =
    Split | Consl | Splitr | Consr
  | Assl | Assr | Insl | Dell | Exch
  | App | Fst | Snd
  | Inl | Inr
  | Alt [Code] [Code]
  | Pair [Code] [Code]
  | Cur [Code]
  | Input
  | Output
    deriving (Show)
data Value =
    Nil
  | And Value Value
  | Comp Code Value
  | InOut
    deriving (Show)
data Stack = Thunk [Code] | Obj Value   deriving (Show)
data State = State [Code] Value [Stack] deriving (Show)

step (State (Split  : c) (u `And` v)       (s)) = (State (c)   (u)         (Obj v:s))
step (State (Consl  : c) (u)         (Obj v:s)) = (State (c)   (u `And` v)       (s))
step (State (Splitr : c) (u `And` v)       (s)) = (State (c)   (v)         (Obj u:s))
step (State (Consr  : c) (v)         (Obj u:s)) = (State (c)   (u `And` v)       (s))

step (State (Assl : c) (u `And` (v `And` w)) (s)) = (State (c) ((u `And` v) `And` w) (s))
step (State (Assr : c) ((u `And` v) `And` w) (s)) = (State (c) (u `And` (v `And` w)) (s))
step (State (Insl : c) (u)                   (s)) = (State (c) (Nil `And` u)         (s))
step (State (Dell : c) (Nil `And` u)         (s)) = (State (c) (u)                   (s))
step (State (Exch : c) (u `And` v)           (s)) = (State (c) (v `And` u)           (s))

step (State (App : c) ((Cur a `Comp` u) `And` v) (s)) = (State (a) (u `And` v) (Thunk c:s))
step (State (Fst : c) (Pair a b `Comp` u)        (s)) = (State (a) (u)         (Thunk c:s))
step (State (Snd : c) (Pair a b `Comp` u)        (s)) = (State (b) (u)         (Thunk c:s))

step (State (Alt a b : c) (Inl `Comp` u) (s)) = (State (a) (u) (Thunk c:s))
step (State (Alt a b : c) (Inr `Comp` u) (s)) = (State (b) (u) (Thunk c:s))

step (State (yu : c) (u)         (s)) = (State (c) (yu `Comp` u) (s))
step (State []       (u) (Thunk c:s)) = (State (c) (u)           (s))

-- step (State (Input : c)  (InOut) (s))           = (State (b) (InOut `And` u)   (Thunk c:s))
-- step (State (Output : c) (InOut `And` u)   (s)) = (State (b) (InOut) (Thunk c:s))