[Agda] Any examples of monad use in Agda?

[Alan Jeffrey]

I'm quite concerned about the use of:

> bind== : {A : Set} ->  (ma : M A) ->  (f : (a : A) ->  ma == return a ->  MB) ->  MB

For example, taking M to be the monad of mutable state, consider:

   bind (ref 0) (\ x ->
   bind== (set x (get x + 1)) (\one incx==one ->
   bind== (set x (get x + 1)) (\two incx==two ->
   ...

It looks like a bit of simple equational reasoning gives an inhabitant 
at run-time for the type (1 == 2) oh dear. The inhabitant is wrapped 
inside M, so you can't use it to get a compile-time contradiction, but 
it looks like it violates run-time safety.

A.

On 02/12/2012 02: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.
>
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda