On 11/21/07, apfelmus <apfelmus@quantentunnel.de> 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.

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.

That said, the generalization to monad transformers and the metaprogramming techniques demonstrated look pretty cool.

   -- ryan