[Agda] Any examples of monad use in Agda?
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Feb 13 15:51:41 CET 2012
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/
More information about the Agda
mailing list