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

[Andreas Abel]

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/