Ryan Ingram wrote:
apfelmus wrote:
A slightly different point of view is that you use a term implementation for your monad, at least for the interesting primitive effects
That's a really interesting point of view, which had struck me slightly, but putting it quite clearly like that definitely helps me understand what is going on.
In fact, it seems like I can implement the original "list" and "state" examples from the Unimo paper in terms of Prompt as well, using a specialized observation function. For example:
data StateP s a where Get :: StateP s s Put :: s -> StateP s ()
runStateP :: Prompt (StateP s) a -> s -> (a,s) runStateP (PromptDone a) s = (a,s) runStateP (Prompt Get k) s = runStateP (k s) s runStateP (Prompt (Put s) k) _ = runStateP (k ()) s
instance MonadState s (Prompt (StatePrompt s)) where get = prompt Get put = prompt . Put
Strangely, this makes me less happy about Prompt rather than more; if it's capable of representing any reasonable computation, it means it's not really the "targeted silver bullet" I was hoping for. On the other hand, it still seems useful for what I am doing.
It appears that your prompt data type is basically Unimo with Bind and Effect fused, i.e. data Prompt p a where Return :: a -> Prompt p a BindEffect :: p b -> (b -> Prompt p a) -> Prompt p a I think that an explicit Bind isn't needed at all, the whole Unimo "framework" can be recast in terms of this type. This simplifies it considerably: the helper function observe_monad can be dropped and observation functions like run_list or run_state can be implemented by directly pattern matching on Prompt. ( unit_op and bind_op are nothing else than the two cases of this match) (The other minor difference is that effects p does not explicitly contain monadic actions, but it's easy to introduce the recursion afterwards: data EffectPlus a where Mplus :: Prompt EffectPlus a -> Prompt EffectPlus a -> EffectPlus a Mzero :: EffectPlus a In Unimo, the effect can be parametrized on the monad, whereas it's fixed here. But this is straightforward to rectify.)
I definitely feel like the full term implementation (like the Unimo paper describes) is overkill; unless I'm misunderstanding what's going on there, you're basically destroying any ability for the compiler to reason about your computations by reifying them into data. As long as (>>=) and return are functions that get inlined, lots of extraneous computation can be eliminated as the compiler "discovers" the monad laws through compile-time beta-reduction; once you turn them into data constructors that ability basically goes away.
I don't know what the compiler does, so I wouldn't recommend unlimited enthusiasm :) But there's an efficiency issue with your implementation that the full term implementation doesn't have (contrary to what I believed in a previous post about the state moand): just like with lists and ++, using
= left-recursively runs in quadratic instead of linear time. Here's a demonstration:
data Effect a = Foo a -- example effect Bef m := BindEffect Foo -- shorthand for the lengthy constructor x = BindEffect Foo Return -- just the example effect = z Return m >> n = m >>= \_ -> n -- we use >> for simplicity Now, consider evaluation to WHNF: (x >> x) => Bef f >> x -- reduce x to WHNF => Bef f (\b -> f b >> x) -- definition of >> (x >> x) >> x => .. => (Bef f (\b -> f b >> x)) >> x -- reduce (x >> x) => Bef f (\b -> (\b2 -> f b2 >> x) b >> x) = Bef f (\b -> (f b >> x) >> x) -- shorthand We see that in the general case, the evaluation of (..(((x >> x) >> x) >> x) ... ) = foldl1 (>>) (replicate n x) will produce the expression Bef f (\b -> (..(((f b >> x) >> x) >> x)..)) in O(n) time. The problem is that this contains another left-recursive chain of (>>) which will take O(n-1) time to evaluate and produce another such chain when the monad is executed. Thus, the whole thing will run in O(n^2). A context passing implementation (yielding the ContT monad transformer) will remedy this. See also John Hughes. The Design of a Pretty-printing Library. http://citeseer.ist.psu.edu/hughes95design.html Regards, apfelmus