Erasable Monad (was Re: [Agda] Any examples of monad use in Agda?)
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Feb 17 10:34:33 CET 2012
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
On 17.02.12 5:40 AM, jleivent at comcast.net wrote:
> Hello Andreas,
>
> Thank you for the references. They have helped me continue to clarify
> my thinking. However, there was much in them that I do not
> understand, an so I could not determine if the properties discussed
> cover the erasure property I am after. In particular, I would like to
> declare an arbitrary amount of a program to be erasable, not just
> irrelevant aspects (proof inhabitants) and types and their parameters
> - and have the type checker prevent any non-erasable usage.
>
> Attached is an updated version of the erasable monad I am working on,
> and a simple example of its (rather inelegant) use.
>
> The following is probably obvious to you, but I will state it just to
> make sure we are in agreement:
>
> I think the difference between the erasability I am looking for and
> irrelevance studied in some of the references you posted can be stated
> as follows. Consider an arbitrary type T that has some version of a
> discrimination axiom like:
>
> ((a b : T) -> a == b) -> \bot
>
> We can make two types Ti (irrelevant) and Te (erasable) from T as
> follows. For Ti, we replace the discrimination axiom with the
> uniqueness axiom:
>
> (a b : Ti) -> a == b
>
> For Te, we just delete the discrimination axiom without replacing it,
> such that neither one of:
>
> (a b : Te) -> a == b
> ((a b : Te) -> a == b) -> \bot
>
> is provable.
>
> The three types are otherwise as similar as they can be (obviously,
> consequences of discrimination have been removed from Ti and Te), and
> we can allow the coercions: T -> Te, T -> Ti, and Te -> Ti.
>
> One can think of Ti as the set containing just one arbitrary and
> anonymous inhabitant from T. One can think of Te as being either T or
> Ti, but which one is not known. We can make Te be erasable by
> requiring that the type checker respect the possibility that Te could
> be T, but have the compiler (after type checking has finished) replace
> Te with Ti - since the consistency of such a replacement is guaranteed
> by the above similarity.
>
> Ti is most useful when T either already does not have provable
> discrimination, or that it has discrimination that is not of any use
> to the program (and is perhaps a burden) - such as is the case with
> the proposition-like types. As some of the references you sent
> explore.
>
> Te is most useful when T isn't a proposition-like type. For example,
> all proofs involving Te terms as arguments to predicates would apply
> to T as well. Proving in Te would be a bit less powerful (fewer
> things provable), because of the absence of discrimination.
>
> The use of a monad to create Te (Te = M T) is interesting because it
> allows the programmer to declare erasable parts of a program
> explicitly. Also, T's discrimination axiom is still available within
> the monad, even though it is rendered unprovable outside (by virtue of
> the erasable monad's limited extraction - which prevents any stateful
> extraction that could "encode" discrimination). As long as one can
> marshal proofs into and through the monad and be satisfied with
> stateless extraction, it should be just as powerful as T. But, that
> marshaling might need some help from strange functions like bind== and
> setout, and multiple rewrites using the monad axioms. It is
> unfortunately not very pretty, even for what should be simple cases,
> as can be seen in the attached example.
>
> Thanks again
> 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: Wed, 15 Feb 2012 08:42:48 -0000 (UTC)
> Subject: Re: [Agda] Any examples of monad use in Agda?
>
> 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
--
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