Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)
jleivent at comcast.net
jleivent at comcast.net
Fri Feb 17 19:08:42 CET 2012
Andreas,
The function "smap" used in the example is a combination of setout and fmap (smap f ma == setout (fmap f ma)). Without setout, there would be no way to legally declare the type signature of MEven+, because fmap isEven ma produces an inhabitant of M Set, which isn't usable as a type outside the monad, and so could not be an argument type to or return type of MEven+:
MEven+ : {ma mb : M N} -> fmap isEven ma -> fmap isEven mb -> fmap isEven (ma +M mb) -- isn't legal Agda
Also note that Axs is the axiomatization of the definition of setout as a rewrite rule, and that >>== used in the example is the operator equivalent of bind==, just as >>= is to bind.
I opted for a setout (return A) == A instead of == M A since it is the more general purpose of the two possibilities, and both seem safe.
-- Jonathan Leivent
----- Original Message -----
From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: jleivent at comcast.net
Cc: Agda mailing list <agda at lists.chalmers.se>
Sent: Fri, 17 Feb 2012 09:34:33 -0000 (UTC)
Subject: Re: Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)
Hello Jonathan,
I briefly looked at your example, but there was no appliation of setout.
It would be instructive to see an example use of it.
Cheers,
Andreas
More information about the Agda
mailing list