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

[Henning Basold]

-----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
>
> 
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-----