A symmetric effect system inspired by game semantics.

EffeGS.hs

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, LambdaCase, DeriveFunctor, DataKinds, GADTs, StandaloneDeriving, NoStarIsType, TypeFamilies, StandaloneKindSignatures, PolyKinds #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module EffeGS where

-- TODO:
--   * Answer-type modification
--   * Higher order effects
--   * Cas: the sum/product duality is still asymmetric
--     solution: session types?

import GHC.TypeLits (Symbol)
import Data.Kind ( Type )
import Control.Monad (ap)

-- Trees (Free Monad)

data Tree f a
  = Pure a
  | Move (f (Tree f a))

instance Functor f => Functor (Tree f) where
  fmap f (Pure x) = Pure (f x)
  fmap f (Move m) = Move (fmap (fmap f) m)

instance Functor f => Applicative (Tree f) where
  pure = Pure
  (<*>) = ap

instance Functor f => Monad (Tree f) where
  Pure x >>= k = k x
  Move m >>= k = Move (fmap (>>= k) m)


-- Operations

type Op :: Symbol -> Type -> Type -> Type
data Op l a b

-- Player

type P :: Type -> Type -> Type
data P sig k where
  P :: forall l a b k. (b -> (a, k)) -> P (Op l a b) k
deriving instance Functor (P sig)

-- Opponent

type O :: Type -> Type -> Type
data O sig k where
  O :: (a -> (b, k)) -> O (Op l a b) k
deriving instance Functor (O sig)

-- Sum of signatures (Player)

data PSum sig a where
  Hd :: P f a -> PSum (f : sig) a
  Tl :: PSum sig a -> PSum (f : sig) a
deriving instance Functor (PSum sig)

-- Row membership

class f < g where
  inj :: f x -> g x

instance {-# OVERLAPPING #-} P f < PSum (f : sig) where
  inj = Hd

instance P f < PSum sig => P f < PSum (f' : sig) where
  inj = Tl . inj

-- Product of signatures (Opponent)

data OProd sig a where
  Cons :: O f a -> OProd sig a -> OProd (f : sig) a
  Nil :: OProd '[] a

deriving instance Functor (OProd sig)

-- Run one opponent move against a player move
runOne :: O sig ko -> P sig kp -> (ko, kp)
runOne (O f) (P g) =
  let ~(y, ko) = f x
      ~(x, kp) = g y
  in (ko, kp)

-- Run a tree of opponent moves against a tree of player moves
runAll :: forall sig a. Tree (OProd sig) a -> Tree (PSum sig) a -> a
runAll (Pure x) _ = x
runAll _ (Pure x) = x
runAll (Move o) (Move p) = go o p where
  go :: OProd sig' (Tree (OProd sig) a) -> PSum sig' (Tree (PSum sig) a) -> a
  go (Cons o _) (Hd p) = uncurry runAll (runOne o p)
  go (Cons _ o) (Tl p) = go o p

-- Get and Put operations
type Get = Op "get" () Int
type Put = Op "put" Int ()

-- hstate opponent which models state
hstate :: Int -> Tree (OProd [Get, Put]) a
hstate s = Move (Cons (O (\() -> (s, hstate s))) (Cons (O (\s' -> ((), hstate s'))) Nil))

-- Parallel composition of two opponent trees

type family Append xs ys where
  Append '[] ys = ys
  Append (x : xs) ys = x : Append xs ys

oappend :: OProd sig1 a -> OProd sig2 a -> OProd (Append sig1 sig2) a
oappend Nil ys = ys
oappend (Cons x xs) ys = Cons x (oappend xs ys)

pcompose :: Tree (OProd sig1) a -> Tree (OProd sig2) a -> Tree (OProd (Append sig1 sig2)) a
pcompose (Pure x) _ = Pure x
pcompose _ (Pure x) = Pure x
pcompose x0@(Move x) y0@(Move y) = Move $
  oappend (fmap (`pcompose` y0) x) (fmap (pcompose x0) y)

-- get and put player moves

get :: (P Get) < sig => Tree sig Int
get = Move (inj (P @"get" (\s -> ((), Pure s))))

put :: (P Put) < sig => Int -> Tree sig ()
put s = Move (inj (P @"put" (\() -> (s, Pure ()))))

-- program that uses get and put player moves

prog :: Tree (PSum [Get, Put]) (Int, Int)
prog = do
  put 1
  x <- get
  put 2
  y <- get
  pure (x, y)

-- >>> runAll (hstate 0) prog
-- (1,2)