[Agda] Defining the Delay monad as a HIT in cubical agda

[Jesper Cockx]

Hi Henning,

Thanks for your mail. Maybe I misunderstand, but isn't this just the Delay
monad as defined in the standard library (
https://github.com/agda/agda-stdlib/blob/master/src/Codata/Delay.agda)? 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.

-- Jesper

On Tue, Apr 2, 2019 at 11:14 AM Henning Basold <henning at basold.eu> wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA512
>
> Hi Jesper,
>
> When I experimented with the delay monad, I used the code below. Note
> that this uses vanilla Agda and no cubical/HITs. I suppose, however,
> that the same should work with cubical, as the first property proceeds
> by induction on the termination proof, which in turns does not use any
> HITs. The second property is merely unfolding bisimilarity one step.
>
> I hope this helps.
>
> Cheers,
> Henning
>
> - -- Preliminaries
> open import Function
> open import Data.Empty
> open import Data.Sum as Sum
> open import Data.Sum.Properties
> open import Relation.Nullary
> open import Relation.Binary.PropositionalEquality
>
> open import Relation.Binary renaming (Rel to RelP)
>
> Rel : Set → Set₁
> Rel A = RelP A _
>
> inj₁≠inj₂ : {A B : Set} {a : A} {b : B} → inj₁ a ≡ inj₂ b →
>             {C : Set} → C
> inj₁≠inj₂ ()
>
> - -- Delay monad
> record D (A : Set) : Set where
>   coinductive
>   field step : A ⊎ D A
> open D public
>
> ∞ : {A : Set} → D A
> ∞ .step = inj₂ ∞
>
> - -- Bisimilarity via relation lifting
> data Delay-Ext {A B : Set} (R : Rel A) (S : Rel B) : Rel (A ⊎ B) where
>   now    : {x y : A} → R x y → Delay-Ext R S (inj₁ x) (inj₁ y)
>   later  : {x y : B} → S x y → Delay-Ext R S (inj₂ x) (inj₂ y)
>
> record DRel {A : Set} (R : Rel A) (x y : D A) : Set where
>   coinductive
>   field step : Delay-Ext R (DRel R) (x .step) (y .step)
> open DRel public
>
> _~_ : {A : Set} (x y : D A) → Set
> _~_ {A} = DRel _≡_
>
> data _↓′ {A : Set} (d : D A) : Set where
>   now    : (a : A)              → d .step ≡ inj₁ a  → d ↓′
>   later  : {d' : D A}  → d' ↓′  → d .step ≡ inj₂ d' → d ↓′
>
> - -- And then you get the desired results with the following,
> - -- rather crude, proofs:
>
> ∞-non-terminating : ∀ {A} → ¬ (∞ {A} ↓′)
> ∞-non-terminating (now a e)  = inj₁≠inj₂ (sym e)
> ∞-non-terminating (later p e) with inj₂-injective e
> ∞-non-terminating (later p e) | refl = ∞-non-terminating p
>
> ∞-not-now : ∀ {A} x → ¬ (∞ {A} ~ return x)
> ∞-not-now x p with p .step
> ∞-not-now x p | ()
>
>
> On 29/03/2019 19:40, Jesper Cockx wrote:
> > Hi all,
> >
> > As an experiment with cubical agda, I was trying to define a
> > quotiented version of the Delay monad as a higher inductive type.
> > I'm using this definition:
> >
> > data Delay (A : Set ℓ) : Set ℓ
> >
> > record Delay′ (A : Set ℓ) : Set ℓ where coinductive field force :
> > Delay A
> >
> > open Delay′ public
> >
> > data Delay A where now   : A → Delay A later : Delay′ A → Delay A
> > step  : (x : Delay′ A) → later x ≡ x .force
> >
> > I managed to implement some basic functions on it but I got stuck
> > on trying to prove the looping computation 'never' does not in fact
> > evaluate to any value. My code is available here:
> > https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f
> 08e23630221cc3d9
> <https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9>
> >
> >
> I looked at the problem together with Christian Sattler and we are not e
> ven
> > sure it is actually provable. Does anyone have an idea how to
> > proceed? Or has someone already experimented with coinductive types
> > in cubical and encountered similar problems? (I looked at the paper
> > "Partiality revisited" by Thorsten, Nisse and Nicolai but they use
> > a very different definition of the partiality monad.)
> >
> > Cheers, Jesper
> >
> >
> > _______________________________________________ Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> -----BEGIN PGP SIGNATURE-----
>
> iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlyjJ+UACgkQatBsEc2x
> Mm7ssRAApnhxYylfbxU0f6vQKm0y1MSL1kZ6jleKdpGDcYQObaACGVoIQ3BBoOw1
> XqEiInf+uegeNIsWU9D0xOhTFrpn9b4eaDWgeZYuivc4KcUr4QjtrFlT4D/3wLHq
> UlApjDmrcIrIgF4IR1lqn7gblAd8JES4uIwb5nGfbQXnp/sT0Ewv39Ap+0hIKMsf
> S5g1rrzARzsPWkQC8Rx3pUZTUCMA7TB7MPDm9AiKYf70QC3vrmQPIAOt1EfMdwQW
> cJfxgCV6Ayo0nmhAXXLq92+JZCjavdaeS0/o56MWCvLn3tS+/U0mUzBfGXG6Cevg
> gsbFWdtmpPLXvt79wC93wB+h/uZ5vcKkdmsVKNKnlA46xOigv3nbWYkWymJ6/Xnf
> jI7jhWMZxCQZEvzWVC9IgYA17M/uUIBe6tx3F4WP3o49OMxX9qMVdBhIwRsJ4nIn
> LkSQPAbTob0XNYEDFfaow9h2usOqXC1rj5TJtBYr7aiK1qgmpeXWYw6L5P/vSN7i
> bGYl3PqtjPHIgtL14Xin2bvihSuMcYwd3pfoTHZ5Eb1ORJ2BipUIhlj+jBfsEmU5
> YGRZB7bovnHldYAY4iiX5SvafgJUoTySieVcYiuHxc4tQs1NZSLOUNok88B5HnK1
> KEzghZe+tGi2weP7JyuUuQ9iBH7NPlyswbPLQSHkklULk3pq7Ps=
> =r8V9
> -----END PGP SIGNATURE-----
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190402/e6499bd8/attachment.html>