Example of an interpreter with recursive types using compdata

Eval.hs

-- You need DeepSubsumption enabled in order for the example to compile.
{-# LANGUAGE DeepSubsumption #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

module Eval where

import Control.Monad.State.Strict (StateT, evalStateT, gets, liftIO, modify', void)
import Data.Comp.Multi
import Data.Comp.Multi.Derive
import Data.Comp.Multi.Equality ()
import Data.Comp.Multi.Ordering ()
import Data.Comp.Multi.Show ()
import Data.Foldable (traverse_)
import Data.Maybe (fromJust)

type Id = String

data Exp'
data Stm'

data Value e l where
  Id :: Id -> Value e Exp'
  Num :: Int -> Value e Exp'

data Op e l where
  Plus :: e Exp' -> e Exp' -> Op e Exp'
  Minus :: e Exp' -> e Exp' -> Op e Exp'
  Times :: e Exp' -> e Exp' -> Op e Exp'
  Div :: e Exp' -> e Exp' -> Op e Exp'

data Comb e l where
  ESeq :: e Stm' -> e Exp' -> Comb e Exp'

data StmUnit e l where
  Stm :: StmUnit e Stm'

data StmValue e l where
  Compound :: e Stm' -> e Stm' -> StmValue e Stm'
  Assign :: Id -> e Exp' -> StmValue e Stm'
  Print :: [e Exp'] -> StmValue e Stm'

type Exp = Value :+: Op :+: Comb
type Stm = StmUnit :+: StmValue
type Sig = Exp :+: Stm

$(derive [makeHFunctor, makeHTraversable, makeHFoldable] [''Value, ''Op, ''Comb, ''StmValue, ''StmUnit])
$(derive [smartConstructors] [''Value, ''Op, ''Comb, ''StmValue])

-- `smartConstructors` doesn't work with StmUnit, so write iStm manually.
iStm :: (StmUnit :<: f) => Term f Stm'
iStm = inject Stm

type Env = [(Id, Int)]

class EvalM f v where
  evalAlgM :: AlgM (StateT Env IO) f (Term v)

-- You need this to print anything!
$(derive [liftSum] [''EvalM])

evalM :: (HTraversable f, EvalM f v) => Env -> Term f i -> IO (Term v i)
evalM env = flip evalStateT env . cataM evalAlgM

instance {-# OVERLAPPABLE #-} (f :<: v) => EvalM f v where
  evalAlgM = pure . inject

instance {-# OVERLAPPING #-} (Value :<: v) => EvalM Value v where
  evalAlgM (Id i) = iNum . fromJust <$> gets (lookup i)
  evalAlgM v = pure $ inject v

instance {-# OVERLAPPING #-} (Value :<: v) => EvalM Op v where
  evalAlgM (Plus a b) = pure $ iNum $ pNum a + pNum b
  evalAlgM (Minus a b) = pure $ iNum $ pNum a - pNum b
  evalAlgM (Times a b) = pure $ iNum $ pNum a * pNum b
  evalAlgM (Div a b) = pure $ iNum $ pNum a `quot` pNum b

instance {-# OVERLAPPING #-} (Value :<: v) => EvalM Comb v where
  evalAlgM (ESeq _ e) = pure e

instance {-# OVERLAPPING #-} (Value :<: v, StmUnit :<: v) => EvalM StmValue v where
  evalAlgM (Compound _ s2) = pure s2
  evalAlgM (Assign i e) = iStm <$ modify' ((i, pNum e) :)
  evalAlgM (Print es) = iStm <$ traverse_ (liftIO . print . pNum) es

pNum :: (Value :<: v) => Term v Exp' -> Int
pNum v = case project v of Just (Num n) -> n

prog :: Term Sig Stm'
prog =
  iCompound
    (iAssign "a" (iPlus (iNum 5) (iNum 3)))
    ( iCompound
        ( iAssign
            "b"
            ( iESeq
                (iPrint [iId "a", iMinus (iId "a") (iNum 1)])
                (iTimes (iNum 10) (iId "a"))
            )
        )
        (iPrint [iId "b"])
    )

main :: IO ()
main = do
  putStrLn "Evaluating program:"
  void $ evalM @_ @Sig [] prog