[Agda] Partiality/delay monad [was: proofs for (NON)TERMINATING]

[Sandro Stucki]

I have a follow-up question about the partiality/delay monad.

A while ago, I wrote some code using the Partiality monad from the
standard library (Category.Monad.Partiality). But that module uses old
coinduction, which seems deprecated now:

https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html#old-coinduction

If I want to future-proof my code, what is the recommended way to go?

NAD says

The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.

So that is definitely an alternative, but as NAD points out, it adds
some extra dependencies, which I'd like to avoid. Are there any plans
to "upgrade" Category.Monad.Partiality to use coinductive records
and/or sized types?

Here's an example of how one can implement an interpreter for the
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

I get a 404 error following that link.

/Sandro

Please, where it is described the delay monad ?

Venanzio Capretta
General Recursion via Coinductive Types
https://doi.org/10.2168/LMCS-1(2:1)2005
The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.
Here's an example of how one can implement an interpreter for the
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Sandro Stucki

Here's an example of how one can implement an interpreter for the
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

I get a 404 error following that link.

I had rearranged my code, but I decided to undo this rearrangement, so
the link should work again now.

[Guillaume Allais]

Hi Sandro,

This pushed me to finally start the "codata" project on agda-stdlib
to make use of copattern-based sized codatatypes:
https://github.com/agda/agda-stdlib/projects/1

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

There is no guarantee whatsoever that this is the version that will
eventually land in the stdlib but it should hopefully give you an
idea of how these things work.

Best,
--
gallais

Post by Sandro Stucki
I have a follow-up question about the partiality/delay monad.
A while ago, I wrote some code using the Partiality monad from the
standard library (Category.Monad.Partiality). But that module uses old
https://agda.readthedocs.io/en/v2.5.3/language/coinduction.html#old-coinduction
If I want to future-proof my code, what is the recommended way to go?
NAD says

The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.

So that is definitely an alternative, but as NAD points out, it adds
some extra dependencies, which I'd like to avoid. Are there any plans
to "upgrade" Category.Monad.Partiality to use coinductive records
and/or sized types?

Here's an example of how one can implement an interpreter for the
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

I get a 404 error following that link.
/Sandro

Please, where it is described the delay monad ?

Venanzio Capretta
General Recursion via Coinductive Types
https://doi.org/10.2168/LMCS-1(2:1)2005
The standard library contains an implementation in
Category.Monad.Partiality. I would not recommend that you use this
implementation. I have another implementation that uses sized types, and
which is therefore in my opinion easier to use (the delay-monad library,
available from http://www.cse.chalmers.se/~nad/software.html). However,
this implementation depends on a different library, which is set up in a
somewhat roundabout way in order to cater to a certain experiment. I
believe others have also implemented the delay monad using sized types.
Here's an example of how one can implement an interpreter for the
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
--
/NAD
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Guillaume Allais
I have pushed a first few modules to the codata branch to start the
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.

[Guillaume Allais]

Thanks! That's a lot of content!

I haven't implemented anything regarding weak bisimilarity yet because
it's notoriously hard. One thing I'm wondering as a complete newcomer
is whether it'd make sense to have a stricter notion of proofs of weak
bisimilarity and then recover some of the current constructor's types
as lemmas.

E.g. (reusing your notations, forgetting about the very general setting
for the moment) would it make sense to have:

  data [_]_≈_ (i : Size) :
           Delay A ∞ → Delay A ∞ → Set a where
      now    : ∀ {k x} → [ i ] now x ≈ now x
      later  : ∀ {k x y} →
               [ i ] force x ≈′ force y →
               [ i ] later x ≈ later y
      later-now : ∀ {k x y} →
               [ i ] force x ≈ now y →
               [ i ] later x ≈ now y
      now-later : ∀ {x y} →
               [ i ] now x ≈ force y →
               [ i ] now x ≈ later y

? Have you experimented with such a definition in the past?

Cheers,
--
gallais

Post by Nils Anders Danielsson

Post by Guillaume Allais
I have pushed a first few modules to the codata branch to start the
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
 
http://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.Bisimilarity.Negative.html
 
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
 
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.

[Nils Anders Danielsson]

Post by Guillaume Allais
E.g. (reusing your notations, forgetting about the very general setting
Delay A ∞ → Delay A ∞ → Set a where
now : ∀ {k x} → [ i ] now x ≈ now x
later : ∀ {k x y} →
[ i ] force x ≈′ force y →
[ i ] later x ≈ later y
later-now : ∀ {k x y} →
[ i ] force x ≈ now y →
[ i ] later x ≈ now y
now-later : ∀ {x y} →
[ i ] now x ≈ force y →
[ i ] now x ≈ later y
? Have you experimented with such a definition in the past?

This definition reminds me of Venanzio Capretta's definition of weak
bisimilarity. I have proved that his definition (defined using sized
types) is pointwise logically equivalent to the one that I use, in a
size-preserving way:

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

I guess that this also holds for your definition. I have no strong
argument for preferring one definition over the others.

There is another definition (also discussed by Venanzio) that has the
advantage of being propositional in the HoTT sense, assuming
extensionality, when the carrier type is a set (this observation is
possibly due to Thorsten Altenkirch):

∀ v → x ⇓ v ⇔ y ⇓ v

Here "x ⇓ v" means that x terminates with the value v; _⇓_ is defined
inductively.

This relation is also pointwise logically equivalent to the others.
However, it is not defined using sized types, so the translations are
not size-preserving, and I suspect (without any hard evidence) that it
would be tiresome to work directly with this type.