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

[Thorsten Altenkirch]

Our presentation using chains as functions from Nat isn’t really so different to the coinductive definition. The delay monad can be equivalently described as functions f : Nat -> Maybe(A) with the property that if f n = just a -> f(n+1) = just a. Hence the definition in our paper corresponds to the delay monad of they are flat, i.e. if we don’t iterate the lub constructor and use only bottom or eta a. Hence if you want to model the partiality monad using a coninductive type you should allow to iterate it that is use something like Delay^n(A) and quotient this e.g. by collapsing layers. Our definition of the partiality monad seems quite natural because it is simply the free omega-CPO over a given set. However, maybe one can define this coniductively instead of using functions to describe chains.

Thorsten

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Nicolai Kraus <nicolai.kraus at gmail.com>
Date: Tuesday, 2 April 2019 at 22:17
To: Tom Jack <tom at tomjack.co>
Cc: agda list <agda at lists.chalmers.se>
Subject: Re: [Agda] Defining the Delay monad as a HIT in cubical agda

On 02/04/19 22:10, Tom Jack wrote:

Normally, I'd expect to be able to 'do path induction' on (later, step), winding up with just `now`, so that Delay A = A. But this is absurd.

I think this is what would happen if we were talking about induction instead of coinduction. My intuition is that coinduction causes all the "chains" to be "one-point-compactified" with the same point `never`.
By "chain", I mean
now(a) = later(now(a)) = later(later(now(a))) = ...

-- Nicolai



Are there examples like this which don't involve a mutual coinductive type?

On Tue, Apr 2, 2019 at 1:06 PM Nicolai Kraus <nicolai.kraus at gmail.com<mailto:nicolai.kraus at gmail.com>> wrote:
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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190402/700c7b82/attachment.html>