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

[Jesper Cockx]

Hi Nicolai,

Yes, Christian and I suspected the same thing (that this definition of the
delay monad is actually a unit type), but I haven't managed to prove that
either because of some mysterious termination checker problem.

I'm currently trying a different approach where I define the Delay type
mutually with the ⇓ type so I can quotient by the relation "normalize to
the same value in a finite number of steps". I'll let you know later if it
works.

-- Jesper

On Tue, Apr 2, 2019 at 3:15 PM Nicolai Kraus <nicolai.kraus at gmail.com>
wrote:

> Hi Jesper,
>
> I find this construction very interesting since it's the first "cubical
> higher co-inductive type" that I've seen! Unfortunately, I don't know how
> these "CHCIT's" behave in Agda.
>
> If I had to guess, I would expect that you *cannot* distinguish now and
> never, which would mean that your construction doesn't give you what you
> wanted. The difference to the quotiented delay monad (or, for what it's
> worth, the QIT/QIIT partiality monad) is that your construction inserts the
> equations "coinductively" (usually, only the later-steps are coinductive).
>
> Thus, my guess is that Delay(Unit) could be contractible. One could try to
> prove that every element is equal to 'now'.
>
> Cheers,
> Nicolai
>
>
> On 29/03/19 18: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/f1647a90c1b27aadd5da748f08e23630221cc3d9
> I looked at the problem together with Christian Sattler and we are not even
> 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 listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190402/f279ea40/attachment.html>