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