I have 2 questions motivated by modular interpreters, as done by
S. Liang, P. Hudak and M.P. Jones.
1. In POPL'95 paper the lifting of inEnv through ContT (continuation
transfomer) is given. I think I managed to prove this lifting natural,
but I needed another environment axiom:
do {o <- rdEnv; inEnv o m} = m
It indeed holds when EnvT is introduced, but I did not verify that it is
preserved through the other transformers. It would be nice if this
property could be derived from the other environment axioms from Liang's
PhD thesis, but I didn't manage.
What confuses me is that Liang in the thesis (written 3 years after POPL'95)
says ``We do not know of a desirable way to lift inEnv through ContT''.
Why is the lifting from POPL'95 paper undesirable? Is something more than
naturalness needed to make it desirable, or is it just that the
additional axiom I mention does not hold in general (which would mean it
breaks after applying some monad transformer)?
2. The second question is simpler. The mentioned lifting of
inEnv through ContT with my class and instance declarations
becomes
newtype ContT c m a = Cont {unCont :: (a -> m c) -> m c}
instance EnvMonad e m => EnvMonad e (ContT c m) where
rdEnv = lift rdEnv
inEnv e ma = Cont (\k ->
do old <- rdEnv
inEnv e (unCont ma (inEnv old . k)))
which does not type check in Hugs98. The problem seems to be with
the first argument of inEnv, when I use
type Enviro = Int
instance EnvMonad Enviro m => EnvMonad Enviro (ContT c m) where
rdEnv = lift rdEnv
inEnv e ma = Cont (\k ->
do old <- rdEnv
inEnv e (unCont ma (inEnv (old::Enviro) . k )))
all is fine. But it suffices to constrain the 2 occurences of rdEnv to
have the same type in the given expression. I managed to do it using
lambda abstraction:
instance EnvMonad e m => EnvMonad e (ContT c m) where
rdEnv = lift rdEnv
inEnv e ma = Cont (\k ->
(\ie -> -- a trick to make inEnv monomorphic
do old <- rdEnv
ie e (unCont ma (ie old . k))) inEnv)
Is there a better way to do it?
Viktor Kuncak, University of Novi Sad
