[Agda] Any examples of monad use in Agda?

jleivent at comcast.net jleivent at comcast.net
Sun Feb 12 21:07:43 CET 2012

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.

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)

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.

But, I'm not sure if or why I should need either setout or bind==.  Certainly neither is definable from return and normal bind alone.  And the apparent need for them is independent of the computation in the monad.

More information about the Agda mailing list