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