[Agda] Any examples of monad use in Agda?

[jleivent at comcast.net]

Hello, Andreas.

> > 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!

I assure you that my monad has only the purest of intentions!  Not all
monads fire rockets.  The monad I'm trying to define is little more
than the Identity monad with a very restricted form of extract.

What I am doing is taking up the challenge Conor issued a month ago to
find a more general notion of erasability than the trick I was using
in the red-black tree code which I sent to the list last month.  My
idea for such a general notion of erasability is such a monad (see
attached ErasableMonad.agda).  It is basically the Identity monad (in
that bind and return don't do very much), but it stores its internal
value in a private field, and only allows extraction of irrelevant or
stateless values (such as inhabitants of a == b for some a, b).  It
would have to be coupled with assurances that the compiler would
always erase it (by which I mean that the programmer could not provoke
the erasure without assistance from the compiler, as was possible with
that trick I sent in last month) - but at least it seems always
erasable, and so feasible for a compiler to make such a guarantee.

With such a monad, consider that red-black tree code I sent in, and it
is easy to see cases like what I described above - where you want to
fmap a predicate/type constructor.  That case would be the "sorted"
predicate, which has the type F -> Set, where F is the "flattened"
list of elements in the tree.  The intention of the erasable monad
usage here is to be able to declare all mentions of that type F as
erasable M F, where M is the above erasable monad.  That's certainly
desirable, because carrying around inhabitants of F at runtime is a
huge waste, and would defeat the whole purpose of the tree algorithm.
So, the programmer might wish to make sure that they're all erasable
by declaration, not merely leave that decision up to the compiler.
The trick I was using prior to this erasable monad idea was to
axiomatize F such that it is indistinguishable from a stateless type
(such as top).  That trick worked - for the black-level Ns as well.
But, as you and Conor pointed out, that trick isn't a very general
technique.  Hence this idea for a monad, since monads are (usually)
general.

So, given M F, and predicate/type-constructor sorted : F -> Set, what
does one do?  That's why I think I need:

  setout : M Set -> Set

that either does

  setout (return S) == M S

or

  setout (return S) == S

which scares me a bit, because it looks too much like an extract that
would defeat the purpose of this monad - could someone extract a
stateful value out of the monad using either version of setout?

But there are other problems with types in monads as well, that I'm
trying to work through - it's hard to determine if they're actual
flaws in the monad or that I'm just having a hard time dealing with
these cases.

Anyway, I'm surprised that you're surprised that I'd put types in a
(pure) monad.  Types are values, too!  I guess your surprise implies
bad news for this effort - if it's really new territory, it's unlikely
that I'll get very far.

> > 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.

Yes - and for purposes similar to the inspect function.  Like the
inspect function, the resulting == can be used to convince the type
checker of one's good intentions, possibly by rewriting things.

Alan Jeffrey points out in his response that bind== might be
inconsistent for non-pure monads, but that's not my concern here.  I
am perfectly willing to concede that such proof-style computations
have no place in non-pure monads.  However, the erasable monad (if one
could be completely defined) would be pure - and hopefully would be
able to host any type of pure computation, including proofs and other
type constructions.

-- Jonathan Leivent
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ErasableMonad.agda
Type: application/octet-stream
Size: 4245 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120213/95888dcc/ErasableMonad.obj