<div dir="ltr"><div dir="ltr"><div>Hi Henning,</div><div><br></div><div>Thanks for your mail. Maybe I misunderstand, but isn't this just the Delay monad as defined in the standard library (<a href="https://github.com/agda/agda-stdlib/blob/master/src/Codata/Delay.agda">https://github.com/agda/agda-stdlib/blob/master/src/Codata/Delay.agda</a>)? My goal was to define a version of the Delay monad where `now x` is definitionally equal to `x .force`. Supposedly this should be possible to define as a higher inductive type in cubical Agda, but I'm suspecting now that my definition is not the right one. The paper "Partiality, revisited" does achieve the goal of defining the proper 'quotiented' Delay monad but it uses a very different definition of the Delay monad and needs to introduce quite some infrastructure to make it work. <br></div><div><br></div><div>-- Jesper<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at 11:14 AM Henning Basold <<a href="mailto:henning@basold.eu">henning@basold.eu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">-----BEGIN PGP SIGNED MESSAGE-----<br>
Hash: SHA512<br>
<br>
Hi Jesper,<br>
<br>
When I experimented with the delay monad, I used the code below. Note<br>
that this uses vanilla Agda and no cubical/HITs. I suppose, however,<br>
that the same should work with cubical, as the first property proceeds<br>
by induction on the termination proof, which in turns does not use any<br>
HITs. The second property is merely unfolding bisimilarity one step.<br>
<br>
I hope this helps.<br>
<br>
Cheers,<br>
Henning<br>
<br>
- -- Preliminaries<br>
open import Function<br>
open import Data.Empty<br>
open import Data.Sum as Sum<br>
open import Data.Sum.Properties<br>
open import Relation.Nullary<br>
open import Relation.Binary.PropositionalEquality<br>
<br>
open import Relation.Binary renaming (Rel to RelP)<br>
<br>
Rel : Set → Set₁<br>
Rel A = RelP A _<br>
<br>
inj₁≠inj₂ : {A B : Set} {a : A} {b : B} → inj₁ a ≡ inj₂ b →<br>
{C : Set} → C<br>
inj₁≠inj₂ ()<br>
<br>
- -- Delay monad<br>
record D (A : Set) : Set where<br>
coinductive<br>
field step : A ⊎ D A<br>
open D public<br>
<br>
∞ : {A : Set} → D A<br>
∞ .step = inj₂ ∞<br>
<br>
- -- Bisimilarity via relation lifting<br>
data Delay-Ext {A B : Set} (R : Rel A) (S : Rel B) : Rel (A ⊎ B) where<br>
now : {x y : A} → R x y → Delay-Ext R S (inj₁ x) (inj₁ y)<br>
later : {x y : B} → S x y → Delay-Ext R S (inj₂ x) (inj₂ y)<br>
<br>
record DRel {A : Set} (R : Rel A) (x y : D A) : Set where<br>
coinductive<br>
field step : Delay-Ext R (DRel R) (x .step) (y .step)<br>
open DRel public<br>
<br>
_~_ : {A : Set} (x y : D A) → Set<br>
_~_ {A} = DRel _≡_<br>
<br>
data _↓′ {A : Set} (d : D A) : Set where<br>
now : (a : A) → d .step ≡ inj₁ a → d ↓′<br>
later : {d' : D A} → d' ↓′ → d .step ≡ inj₂ d' → d ↓′<br>
<br>
- -- And then you get the desired results with the following,<br>
- -- rather crude, proofs:<br>
<br>
∞-non-terminating : ∀ {A} → ¬ (∞ {A} ↓′)<br>
∞-non-terminating (now a e) = inj₁≠inj₂ (sym e)<br>
∞-non-terminating (later p e) with inj₂-injective e<br>
∞-non-terminating (later p e) | refl = ∞-non-terminating p<br>
<br>
∞-not-now : ∀ {A} x → ¬ (∞ {A} ~ return x)<br>
∞-not-now x p with p .step<br>
∞-not-now x p | ()<br>
<br>
<br>
On 29/03/2019 19:40, Jesper Cockx wrote:<br>
> Hi all,<br>
> <br>
> As an experiment with cubical agda, I was trying to define a<br>
> quotiented version of the Delay monad as a higher inductive type.<br>
> I'm using this definition:<br>
> <br>
> data Delay (A : Set ℓ) : Set ℓ<br>
> <br>
> record Delay′ (A : Set ℓ) : Set ℓ where coinductive field force :<br>
> Delay A<br>
> <br>
> open Delay′ public<br>
> <br>
> data Delay A where now : A → Delay A later : Delay′ A → Delay A <br>
> step : (x : Delay′ A) → later x ≡ x .force<br>
> <br>
> I managed to implement some basic functions on it but I got stuck<br>
> on trying to prove the looping computation 'never' does not in fact<br>
> evaluate to any value. My code is available here: <br>
> <a href="https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9" rel="noreferrer" target="_blank">https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f<br>
08e23630221cc3d9</a><br>
><br>
> <br>
I looked at the problem together with Christian Sattler and we are not e<br>
ven<br>
> sure it is actually provable. Does anyone have an idea how to<br>
> proceed? Or has someone already experimented with coinductive types<br>
> in cubical and encountered similar problems? (I looked at the paper<br>
> "Partiality revisited" by Thorsten, Nisse and Nicolai but they use<br>
> a very different definition of the partiality monad.)<br>
> <br>
> Cheers, Jesper<br>
> <br>
> <br>
> _______________________________________________ Agda mailing list <br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
-----BEGIN PGP SIGNATURE-----<br>
<br>
iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlyjJ+UACgkQatBsEc2x<br>
Mm7ssRAApnhxYylfbxU0f6vQKm0y1MSL1kZ6jleKdpGDcYQObaACGVoIQ3BBoOw1<br>
XqEiInf+uegeNIsWU9D0xOhTFrpn9b4eaDWgeZYuivc4KcUr4QjtrFlT4D/3wLHq<br>
UlApjDmrcIrIgF4IR1lqn7gblAd8JES4uIwb5nGfbQXnp/sT0Ewv39Ap+0hIKMsf<br>
S5g1rrzARzsPWkQC8Rx3pUZTUCMA7TB7MPDm9AiKYf70QC3vrmQPIAOt1EfMdwQW<br>
cJfxgCV6Ayo0nmhAXXLq92+JZCjavdaeS0/o56MWCvLn3tS+/U0mUzBfGXG6Cevg<br>
gsbFWdtmpPLXvt79wC93wB+h/uZ5vcKkdmsVKNKnlA46xOigv3nbWYkWymJ6/Xnf<br>
jI7jhWMZxCQZEvzWVC9IgYA17M/uUIBe6tx3F4WP3o49OMxX9qMVdBhIwRsJ4nIn<br>
LkSQPAbTob0XNYEDFfaow9h2usOqXC1rj5TJtBYr7aiK1qgmpeXWYw6L5P/vSN7i<br>
bGYl3PqtjPHIgtL14Xin2bvihSuMcYwd3pfoTHZ5Eb1ORJ2BipUIhlj+jBfsEmU5<br>
YGRZB7bovnHldYAY4iiX5SvafgJUoTySieVcYiuHxc4tQs1NZSLOUNok88B5HnK1<br>
KEzghZe+tGi2weP7JyuUuQ9iBH7NPlyswbPLQSHkklULk3pq7Ps=<br>
=r8V9<br>
-----END PGP SIGNATURE-----<br>
</blockquote></div>