[Agda] Any examples of monad use in Agda?

[Andreas Abel]

Hello Jonathan,

your erasability monad has some similarity to bracket types (Awodey and 
Bauer) and the proof or Squash monad.  Here are some slides where I 
survey different approaches to irrelevance:

   http://www2.tcs.ifi.lmu.de/~abel/talkJFLA10.pdf

Currently, Agda's irrelevance is too weak to implement your monad 
directly as

   data Squash (A : Set) : Set where
     return : .A -> Squash A

.extract and extract\bot would work, but not extract== (btw. Alan 
Jeffrey also uses something equivalent to extract==: a version of subst 
with irrelevant equality proof).  Semantically, extract! is justified 
for the usual interpretation of the Squash monad (Squash A makes all 
elements of A equal).  So far, I think you are on the safe side.

I never thought about what Squash Set should be.  Your term setout 
suggest that Squash Set = Set.  That does not hold in the models I 
study.  However, you are looking for more than Squash, you are after 
erasure, and at runtime types are gone.

You might want to look at the work of Barras and Bernardo:  Here, 
irrelevant values can be used arbitrarily in types.  This corresponds to 
the intuition that types are computationally irrelevant.

Cheers,
Andreas

On 13.02.12 11:24 PM, jleivent at comcast.net wrote:
> 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

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