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 (App t1 t2) = do
f <- eval t1
x <- malias (eval t2)
f x
Author: Nicholas Coltharp (mail@heraplem.xyz)
Last modified: 2026-05-18 Mon 17:22
Emacs 30.2 (Org mode 9.7.11)
Validate