Evaluation strategies for monadic computations

class Monad m => MonadAlias m where
  malias :: m a -> m (m a)
data Ty = Fn Ty Ty

data Tm rep a where
  Var :: rep a -> Tm rep a
  Abs :: (rep a -> Tm rep b) -> Tm rep (Fn a b)
  App :: Tm rep (Fn a b) -> Tm rep a -> Tm rep a

type family Val

eval :: MonadAlias m => Tm m a -> m (rep a)
eval (Var x) = x
-- eval (Abs f) = return (\x -> f (eval )
eval (App t1 t2) = do
  f <- eval t1
  x <- malias (eval t2)
  f x

Author: Nicholas Coltharp

Created: 2026-05-04 Mon 00:00

Validate