[Agda] Any examples of monad use in Agda?

[Andreas Abel]

On 2/12/12 9:07 PM, jleivent at comcast.net wrote:
> Does anyone know where I can find some examples of monad usage in
> Agda, not just monad definitions?
>
> I am having some difficulty with a monad I defined, especially when I
> fmap a function that produces a type: given f : A ->  Set, and ma : M
> A, do fmap f ma, and get a useable result, meaning a type that can be
> used to declare things.

Aeh, a type in a monad?  That sounds strange!  Should not types be 
pure??  Why would you need something that launches a rocket while 
returning a type?  Types are gone at runtime, so they should not have 
effects!

> It seems like I need a strange monadic function like this: setout : M
> Set ->  Set, such that forall (A : Set) ->  setout (return A) == M A.
> With this I can do the following:
>
> q : setout (fmap f ma)

Would you post some code that leads us to the point where you require 
such a thing?

> Also, I have found a particular dependent variety of bind to be
> helpful:
>
> bind== : {A : Set} ->  (ma : M A) ->  (f : (a : A) ->  ma == return a
> ->  MB) ->  MB
>
> meaning that the function f gets both the value in the monad and an
> equality proof tying that value back to the monadic input.

bind== could very well be useful if you want to prove stuff about your 
monadic programs.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/