So we can model state of IO through embedding of the RealWorld# token. Still, we can actually escape this with unsafePerformIO. At that point, we don't have access to state anymore even though in the real evaluation we would actually have some global state. The solution would be to also carry around some global state in the evaluator. The type initial state (and its type) can be decided by the user and should likely be part of the annotation.
So we can model state of IO through embedding of the
RealWorld#token. Still, we can actually escape this withunsafePerformIO. At that point, we don't have access to state anymore even though in the real evaluation we would actually have some global state. The solution would be to also carry around some global state in the evaluator. The type initial state (and its type) can be decided by the user and should likely be part of the annotation.