Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)

[jleivent at comcast.net]

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