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

[jleivent at comcast.net]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ErasableMonadTest.agda
Type: application/octet-stream
Size: 1892 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120217/82edf98e/ErasableMonadTest.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ErasableMonad.agda
Type: application/octet-stream
Size: 3928 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120217/82edf98e/ErasableMonad.obj