Minimal Interaction Calculus implementation in Haskell

ic.hs

import Control.Monad (when)
import Data.Char (chr, ord)
import Data.IORef
import Data.Word
import Debug.Trace
import System.IO.Unsafe (unsafePerformIO)
import Text.Parsec hiding (State)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map as Map
import qualified Text.Parsec as Parsec
import Control.Monad.IO.Class (liftIO)

type Name = Word64

data Term
  = Var Name                     -- Name
  | Let Name Term Term           -- "! " Name " = " Term "; " Term
  | Era                          -- "*"
  | Sup Name Term Term           -- "&" Name "{" Term "," Term "}"
  | Dup Name Name Name Term Term -- "! &" Name "{" Name "," Name "}" "=" Term ";" Term
  | Lam Name Term                -- "λ" Name "." Term
  | App Term Term                -- "(" Term " " Term ")"

-- Globals
-- -------

{-# NOINLINE gSUBST #-}
gSUBST :: IORef (IntMap.IntMap Term)
gSUBST = unsafePerformIO $ newIORef IntMap.empty

{-# NOINLINE gFRESH #-}
gFRESH :: IORef Name
gFRESH = unsafePerformIO $ newIORef 0

{-# NOINLINE gINTERS #-}
gINTERS :: IORef Word64
gINTERS = unsafePerformIO $ newIORef 0

-- Evaluator
-- ---------

-- Helper functions for global substitution
set :: Name -> Term -> IO ()
set name term = do
  subMap <- readIORef gSUBST
  writeIORef gSUBST (IntMap.insert (fromIntegral name) term subMap)

get :: Name -> IO (Maybe Term)
get name = do
  subMap <- readIORef gSUBST
  return $ IntMap.lookup (fromIntegral name) subMap

fresh :: IO Name
fresh = do
  n <- readIORef gFRESH
  writeIORef gFRESH (n + 1)
  return n

incInters :: IO ()
incInters = do
  n <- readIORef gINTERS
  writeIORef gINTERS (n + 1)

app_era :: Term -> Term -> IO Term
app_era Era _ = do
  incInters
  return Era
app_era _ _ = error "app_era: expected Era as first argument"

app_lam :: Term -> Term -> IO Term
app_lam (Lam nam bod) arg = do
  incInters
  set nam arg
  whnf bod
app_lam _ _ = error "app_lam: expected Lam as first argument"

app_sup :: Term -> Term -> IO Term
app_sup (Sup lab lft rgt) arg = do
  incInters
  c0 <- fresh
  c1 <- fresh
  let a0 = App lft (Var c0)
  let a1 = App rgt (Var c1)
  whnf (Dup lab c0 c1 arg (Sup lab a0 a1))
app_sup _ _ = error "app_sup: expected Sup as first argument"

app_dup :: Term -> IO Term
app_dup (App f (Dup lab x y val bod)) = do
  incInters
  whnf (Dup lab x y val (App f bod))
app_dup term = error "app_dup: expected App with Dup"

dup_era :: Term -> Term -> IO Term
dup_era (Dup lab r s _ k) Era = do
  incInters
  set r Era
  set s Era
  whnf k
dup_era _ _ = error "dup_era: expected Dup and Era"

dup_lam :: Term -> Term -> IO Term
dup_lam (Dup lab r s _ k) (Lam x f) = do
  incInters
  x0 <- fresh
  x1 <- fresh
  f0 <- fresh
  f1 <- fresh
  set r (Lam x0 (Var f0))
  set s (Lam x1 (Var f1))
  set x (Sup lab (Var x0) (Var x1))
  whnf (Dup lab f0 f1 f k)
dup_lam _ _ = error "dup_lam: expected Dup and Lam"

dup_sup :: Term -> Term -> IO Term
dup_sup (Dup dupLab x y _ k) (Sup supLab a b) = do
  incInters
  if dupLab == supLab then do
    set x a
    set y b
    whnf k
  else do
    a0 <- fresh
    a1 <- fresh
    b0 <- fresh
    b1 <- fresh
    set x (Sup supLab (Var a0) (Var b0))
    set y (Sup supLab (Var a1) (Var b1))
    whnf (Dup dupLab a0 a1 a (Dup dupLab b0 b1 b k))
dup_sup _ _ = error "dup_sup: expected Dup and Sup"

dup_dup :: Term -> Term -> IO Term
dup_dup (Dup labL x0 x1 _ t) (Dup labR y0 y1 y x) = do
  -- incInters
  whnf (Dup labL x0 x1 x (Dup labL y0 y1 y t))
dup_dup _ _ = error "dup_dup: expected Dup with inner Dup"

whnf :: Term -> IO Term
whnf term = do
  case term of
    Var n -> do
      sub <- get n
      case sub of
        Just s  -> whnf s
        Nothing -> return (Var n)
    Let x v b -> do
      v' <- whnf v
      set x v'
      whnf b
    App f a -> do
      f' <- whnf f
      case f' of
        Lam _ _       -> app_lam f' a
        Sup _ _ _     -> app_sup f' a
        Era           -> app_era f' a
        Dup _ _ _ _ _ -> app_dup (App f' a)
        _             -> return (App f' a)
    Dup l x y v b -> do
      v' <- whnf v
      case v' of
        Lam _ _       -> dup_lam (Dup l x y v' b) v'
        Sup _ _ _     -> dup_sup (Dup l x y v' b) v'
        Era           -> dup_era (Dup l x y v' b) v'
        Dup _ _ _ _ _ -> dup_dup (Dup l x y v' b) v'
        _             -> return $ Dup l x y v' b
    _ -> return term

-- Normalization
-- -------------

normal :: Term -> IO Term
normal term = do
  term' <- whnf term
  case term' of
    Lam x b -> do
      b' <- normal b
      return $ Lam x b'
    App f a -> do
      f' <- normal f
      a' <- normal a
      return $ App f' a'
    Sup l a b -> do
      a' <- normal a
      b' <- normal b
      return $ Sup l a' b'
    Dup l x y v b -> do
      v' <- normal v
      b' <- normal b
      return $ Dup l x y v' b'
    _ -> return term'

-- Stringifier
-- -----------

name :: Name -> String
name k = all !! fromIntegral (k+1) where
  all :: [String]
  all = [""] ++ concatMap (\str -> map (: str) ['a'..'z']) all

instance Show Term where
  show (Var n)           = name n
  show (Let x t1 t2)     = "! " ++ name x ++ " = " ++ show t1 ++ "; " ++ show t2
  show Era               = "*"
  show (Sup l t1 t2)     = "&" ++ show (fromIntegral l :: Int) ++ "{" ++ show t1 ++ "," ++ show t2 ++ "}"
  show (Dup l x y t1 t2) = "! &" ++ show (fromIntegral l :: Int) ++ "{" ++ name x ++ "," ++ name y ++ "} = " ++ show t1 ++ "; " ++ show t2
  show (Lam x t)         = "λ" ++ name x ++ "." ++ show t
  show (App t1 t2)       = "(" ++ show t1 ++ " " ++ show t2 ++ ")"

-- Parser
-- ------

type ParserST = Map.Map String Name
type LocalCtx = Map.Map String Name
type Parser a = ParsecT String ParserST IO a

whiteSpace :: Parser ()
whiteSpace = skipMany (space <|> comment) where
  comment = do 
    try (string "//")
    skipMany (noneOf "\n\r")
    (newline <|> (eof >> return '\n'))

lexeme :: Parser a -> Parser a
lexeme p = p <* whiteSpace

symbol :: String -> Parser String
symbol s = lexeme (string s)

parseNatural :: Parser Integer
parseNatural = lexeme $ read <$> many1 digit

isGlobal :: String -> Bool
isGlobal name = take 1 name == "$"

getGlobalName :: String -> Parser Name
getGlobalName gname = do
  globalMap <- getState
  case Map.lookup gname globalMap of
    Just n  -> return n
    Nothing -> do
      n <- liftIO fresh
      putState (Map.insert gname n globalMap)
      return n

bindVar :: String -> LocalCtx -> Parser (Name, LocalCtx)
bindVar name ctx
  | isGlobal name = do
      n <- getGlobalName name
      return (n, ctx)
  | otherwise = do
      n <- liftIO fresh
      let ctx' = Map.insert name n ctx
      return (n, ctx')

getVar :: String -> LocalCtx -> Parser Name
getVar name ctx
  | isGlobal name = getGlobalName name
  | otherwise = case Map.lookup name ctx of
      Just n  -> return n
      Nothing -> fail $ "Unbound local variable: " ++ name

parseVarName :: Parser String
parseVarName = lexeme $ try (do
  char '$'
  name <- many1 (alphaNum <|> char '_')
  return ("$" ++ name)
 ) <|> many1 (alphaNum <|> char '_')

-- Term parsers
parseTerm :: LocalCtx -> Parser Term
parseTerm ctx
  =   try (parseApp ctx)
  <|> try (parseLet ctx)
  <|> try (parseLam ctx)
  <|> try (parseSup ctx)
  <|> try (parseDup ctx)
  <|> parseSimpleTerm ctx

parseSimpleTerm :: LocalCtx -> Parser Term
parseSimpleTerm ctx
  = parseVar ctx
  <|> parseEra
  <|> between (symbol "(") (symbol ")") (parseTerm ctx)

parseVar :: LocalCtx -> Parser Term
parseVar ctx = do
  name <- parseVarName
  n    <- getVar name ctx
  return $ Var n

parseLam :: LocalCtx -> Parser Term
parseLam ctx = do
  symbol "λ"
  name      <- parseVarName
  (n, ctx') <- bindVar name ctx
  symbol "."
  body      <- parseTerm ctx'
  return $ Lam n body

parseApp :: LocalCtx -> Parser Term
parseApp ctx = between (symbol "(") (symbol ")") $ do
  f <- parseTerm ctx
  whiteSpace
  a <- parseTerm ctx
  return $ App f a

parseSup :: LocalCtx -> Parser Term
parseSup ctx = do
  symbol "&"
  l <- fromIntegral <$> parseNatural
  (a, b) <- between (symbol "{") (symbol "}") $ do
    a <- parseTerm ctx
    symbol ","
    b <- parseTerm ctx
    return (a, b)
  return $ Sup l a b

parseDup :: LocalCtx -> Parser Term
parseDup ctx = do
  symbol "!"
  symbol "&"
  l <- fromIntegral <$> parseNatural
  (name1, name2) <- between (symbol "{") (symbol "}") $ do
    a <- parseVarName
    symbol ","
    b <- parseVarName
    return (a, b)
  symbol "="
  val <- parseTerm ctx
  symbol ";"
  (n1, ctx') <- bindVar name1 ctx
  (n2, ctx'') <- bindVar name2 ctx'
  body <- parseTerm ctx''
  return $ Dup l n1 n2 val body

parseLet :: LocalCtx -> Parser Term
parseLet ctx = do
  symbol "!"
  name      <- parseVarName
  symbol "="
  t1        <- parseTerm ctx
  symbol ";"
  (n, ctx') <- bindVar name ctx
  t2        <- parseTerm ctx'
  return $ Let n t1 t2

parseEra :: Parser Term
parseEra = do
  symbol "*"
  return Era

parseIC :: String -> IO (Either ParseError (Term, Map.Map String Name))
parseIC input = runParserT parser Map.empty "" input where
  parser = do
    whiteSpace
    term <- parseTerm Map.empty
    state <- getState
    return (term, state)

doParseIC :: String -> IO Term
doParseIC input = do
  result <- parseIC input
  case result of
    Left err        -> error $ show err
    Right (term, _) -> return term

-- Tests
-- -----

test :: String -> IO ()
test input = do
  term <- doParseIC input
  norm <- normal term
  print term
  print norm

main :: IO ()
main = do
  test $ unlines
    [ "!F = λf."
    , "  !&0{f0,f1} = f;"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  !&0{f0,f1} = λx.(f0 (f1 x));"
    , "  λx.(f0 (f1 x));"
    , "((F λnx.((nx λt0.λf0.f0) λt1.λf1.t1)) λT.λF.T)"
    ]
  inters <- readIORef gINTERS
  putStrLn $ "- WORK: " ++ show inters

Interaction Calculus

The Interaction Calculus is a minimal term rewriting system inspired by the
Lambda Calculus (λC), but with some key differences:

1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
3. There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

Term ::=
  | VAR: Name
  | ERA: "*"
  | LAM: "λ" Name "." Term
  | APP: "(" Term " " Term ")"
  | SUP: "&" Label "{" Term "," Term "}"
  | DUP: "!" "&" Label "{" Name "," Name "}" "=" Term ";" Term
  | NUM: Number
  | SUC: "+" Term
  | SWI: "?" Term "{" "0" ":" Term ";" "+" ":" Term ";" "}"

Where:

• VAR represents a variable.
• ERA represents an erasure.
• LAM represents a lambda.
• APP represents a application.
• SUP represents a superposition.
• DUP represents a duplication.
• NUM represents a number.
• SUC represents a successor
• SWI represents a switch.

Lambdas are curried, and work like their λC counterpart, except with a relaxed
scope, and with affine usage. Applications eliminate lambdas, like in λC,
through the beta-reduce (APP-LAM) interaction.

Superpositions work like pairs. Duplications eliminate superpositions through
the DUP-SUP interaction, which works exactly like a pair projection.

What makes SUPs and DUPs unique is how they interact with LAMs and APPs. When a
SUP is applied to an argument, it reduces through the APP-SUP interaction, and
when a LAM is projected, it reduces through the DUP-LAM interaction. This gives
a computational behavior for every possible interaction: there are no runtime
errors on the Interaction Calculus.

NUM, SUC and SWI aren't essential to the theory, but are added for convenience.

The 'Label' is just a numeric value. It affects the DUP-SUP interaction.

The core interaction rules are listed below:

(* a)
----- APP-ERA
*

(λx.f a)
-------- APP-LAM
x <- a
f

(&L{a,b} c)
----------------- APP-SUP
! &L{c0,c1} = c;
&L{(a c0),(b c1)}

! &L{r,s} = *;
K
-------------- DUP-ERA
r <- *
s <- *
K

! &L{r,s} = λx.f;
K
----------------- DUP-LAM
r <- λx0.f0
s <- λx1.f1
x <- &L{x0,x1}
! &L{f0,f1} = f;
K

! &L{x,y} = &L{a,b};
K
-------------------- DUP-SUP (if equal labels)
x <- a
y <- b
K

! &L{x,y} = &R{a,b};
K
-------------------- DUP-SUP (if different labels)
x <- &R{a0,b0} 
y <- &R{a1,b1}
! &L{a0,a1} = a;
! &L{b0,b1} = b;
K

The numeric interaction rules are listed below:

+N
--- SUC-NUM
N+1

+*
-- SUC-ERA
*

+&L{x,y}
--------- SUC-SUP
&L{+x,+y}

?N{0:z;+:s;}
------------ SWI-NUM (if N==0)
z

?N{0:z;+:s;}
------------ SWI-NUM (if N>0)
(s N-1)

?*{0:z;+:s;}
------------ SWI-ERA
*

?&L{x,y}{0:z;+:s;}
--------------------------------- SWI-SUP
!&L{z0,z1} = z;
!&L{s0,s1} = s;
&L{?x{0:z0;+:s0;},?y{0:z1;+:s1;}}

! &L{x,y} = N;
K
-------------- DUP-NUM
x <- N
y <- N
K

Where x <- t stands for a global substitution of x by t.

Since variables are affine, substitutions can be implemented efficiently by just
inserting an entry in a global substitution map (sub[var] = value). There is
no need to traverse the target term, or to handle name capture, as long as fresh
variable names are globally unique. It can also be implemented in a concurrent
setup with a single atomic-swap.

Below is a pseudocode implementation of these interaction rules:

def app_lam(app, lam):
  sub[lam.nam] = app.arg
  return lam.bod

def app_sup(app, sup):
  x0 = fresh()
  x1 = fresh()
  a0 = App(sup.lft, Var(x0))
  a1 = App(sup.rgt, Var(x1))
  return Dup(sup.lab, x0, x1, app.arg, Sup(a0, a1))

def dup_lam(dup, lam):
  x0 = fresh()
  x1 = fresh()
  f0 = fresh()
  f1 = fresh()
  sub[dup.lft] = Lam(x0, Var(f0))
  sub[dup.rgt] = Lam(x1, Var(f1))
  sub[lam.nam] = Sup(dup.lab, Var(x0), Var(x1))
  return Dup(dup.lab, f0, f1, lam.bod, dup.bod)

def dup_sup(dup, sup):
  if dup.lab == sup.lab:
    sub[dup.lft] = sup.lft
    sub[dup.rgt] = sup.rgt
    return dup.bod

Terms can be reduced to weak head normal form, which means reducing until the
outermost constructor is a value (LAM, SUP, etc.), or until no more reductions
are possible. Example:

def whnf(term):
  while True:
    match term:
      case Var(nam):
        if nam in sub:
          term = sub[nam]
        else:
          return term
      case App(fun, arg):
        fun = whnf(fun)
        match fun:
          case Lam(_, _):
            term = app_lam(term, fun)
          case Sup(_, _):
            term = app_sup(term, fun)
          case _:
            return App(fun, arg)
      case Dup(lft, rgt, val, bod):
        val = whnf(val)
        match val:
          case Lam(_, _):
            term = dup_lam(term, val)
          case Sup(_, _):
            term = dup_sup(term, val)
          case _:
            return Dup(lft, rgt, val, bod)
      case _:
        return term

Terms can be reduced to full normal form by recursively taking the whnf:

def normal(term):
  term = whnf(term)
  match term:
    case Lam(nam, bod):
      bod_nf = normal(bod)
      return Lam(nam, bod_nf)
    case App(fun, arg):
      fun_nf = normal(fun)
      arg_nf = normal(arg)
      return App(fun_nf, arg_nf)
    case Sup(lft, rgt):
      lft_nf = normal(lft)
      rgt_nf = normal(rgt)
      return Sup(lft_nf, rgt_nf)
    case Dup(lft, rgt, val, bod):
      val_nf = normal(val)
      bod_nf = normal(bod)
      return Dup(lft, rgt, val_nf, bod_nf)
    case _:
      return term

Below are some normalization examples.

Example 0: (simple λ-term)

(λx.λt.(t x) λy.y)
------------------ APP-LAM
λt.(t λy.y)

Example 1: (larger λ-term)

(λb.λt.λf.((b f) t) λT.λF.T)
---------------------------- APP-LAM
λt.λf.((λT.λF.T f) t)
----------------------- APP-LAM
λt.λf.(λF.t f)
-------------- APP-LAM
λt.λf.t

Example 2: (global scopes)

{x,(λx.λy.y λk.k)}
------------------ APP-LAM
{λk.k,λy.y}

Example 3: (superposition)

!{a,b} = {λx.x,λy.y}; (a b)
--------------------------- DUP-SUP
(λx.x λy.y)
----------- APP-LAM
λy.y

Example 4: (overlap)

({λx.x,λy.y} λz.z)
------------------ APP-SUP  
! {x0,x1} = λz.z; {(λx.x x0),(λy.y x1)}  
--------------------------------------- DUP-LAM  
! {f0,f1} = {r,s}; {(λx.x λr.f0),(λy.y λs.f1)}  
---------------------------------------------- DUP-SUP  
{(λx.x λr.r),(λy.y λs.s)}  
------------------------- APP-LAM  
{λr.r,(λy.y λs.s)}  
------------------ APP-LAM  
{λr.r,λs.s}  

Example 5: (default test term)

The following term can be used to test all interactions:

((λf.λx.!{f0,f1}=f;(f0 (f1 x)) λB.λT.λF.((B F) T)) λa.λb.a)
----------------------------------------------------------- 16 interactions
λa.λb.a

DUP Permutations

These interactions move a nested DUP out of a redex position.

(!&L{k0,k1}=k;f x)
------------------ APP-DUP
!&L{k0,k1}=k;(f x)

?!&L{k0,k1}=k;n{0:z;+:s;}
------------------------- SWI-DUP
!&L{k0,k1}=k;?n{0:z;+:s;}

! &L{x0,x1} = (!$R{y0,y1}=Y;X); T
------------------------------------- DUP-DUP
! &L{x0,x1} = X; ! &L{y0,y1} = Y; T