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

[Nicolai Kraus]

Interesting! So, in case Delay(Unit) does turn out to be contractible, 
we might also expect that Delay(A) = A. This doesn't seem intuitive to 
me, but it could still be true. Do you see a way to construct Delay(A) 
-> A? If there is such a function, it should be quite canonical, and 
maybe it's easier to write this function than to prove the 
contractibility. But if we can't do this, and we also can't distinguish 
'now' and 'never', then I have no idea what Delay(A) actually is. Does 
any of the cubical models capture such constructions?
(Maybe, at this point, we shouldn't call it "Delay" :)
-- Nicolai


On 02/04/19 15:08, Jesper Cockx wrote:
> 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 
> <mailto: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 list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto: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/35609ec7/attachment.html>