[Agda] Partiality/delay monad

[Nils Anders Danielsson]

On 2018-03-08 14:20, Guillaume Allais wrote:
> I have pushed a first few modules to the codata branch to start the
> discussion one of which is Codata.Delay:
> https://github.com/agda/agda-stdlib/blob/codata/src/Codata/Delay.agda

Feel free to port parts of my library (git clone
http://www.cse.chalmers.se/~nad/repos/delay-monad/).

Note that an important feature of/problem with the delay monad is that
transitivity is not fully size-preserving for weak bisimilarity and
expansion. I have proved that a number of variants of transitivity
cannot be implemented:

   http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.Negative.html

However, some variants can be implemented:

   http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.html

The standard library's equational reasoning framework was not designed
to handle "heterogeneous" forms of transitivity. I have experimented
with a more general framework:

   http://www.cse.chalmers.se/~nad/listings/up-to/Equational-reasoning.html

However, I am not entirely happy with it. Too much overloading can make
code harder to read and harder for Agda to type-check. In the
delay-monad library I defined a set of combinators that is used only for
strong and weak bisimilarity and expansion.

-- 
/NAD