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

Nicolai Kraus nicolai.kraus at gmail.com
Tue Apr 2 23:11:13 CEST 2019


On 02/04/19 21:23, Jesper Cockx wrote:
> Well, if `never` is equal to `now x`, then by transitivity `now x` is 
> equal to `now y` for any `x` and `y`, which would mean I found a very 
> complicated way to define the constant unit type :P

Right... the conjecture should be Delay(A) = Unit. I made a silly 
mistake before!
It's possible that the theory doesn't allow us to prove Delay(A) = 1, 
but I don't expect that we can show the negation of this.

> About terminology: Nisse informed me that `Delay` is used for the 
> (non-truncated) coinductive type with two constructors `now` and 
> `later`, while the properly truncated variant where `later^n x` = `now 
> x` for any finite `n` is called the partiality monad.

This is also the terminology that I know. In addition, probably one 
would want to call something "partiality monad" only if it actually is a 
monad. The definition for this that I find most elegant is the one by 
Tarmo and Niccolò (iirc, this definition ends up being equivalent to our 
suggestion in the "Partiality revisited" paper).

> So my question is actually whether the partiality monad is definable 
> as a higher coinductive type with two point constructors `now` and 
> `later` plus some path constructor(s).
>
> The problem with defining such a higher coinductive type `D` is that 
> all attempts at proving two of its elements are *not* equal seem to fail:
>
> - Pattern matching on an equality between two constructors with an 
> absurd pattern () obviously doesn't work for higher inductive types.
> - Defining a function `f : D -> Bool` or `D -> Set` which 
> distinguishes the two elements doesn't work either because both `Bool` 
> and `Set` are inductively defined, so `f` can only depend on a finite 
> prefix of its input (i.e. f must be continuous).

`f : D -> Bool` shouldn't work even with a correct partiality monad, 
because it shouldn't be decidable whether an element is `never`. One 
could replace `Bool` by the Sierpinski space, which is by definition  
Partiality(1). (btw, `Set` is not inductively defined?)

> - Defining an indexed datatype `data P : D -> Set` that is empty at 
> one index but not at another seems to work, but then we get into 
> trouble when we actually want to prove that it is empty for that 
> particular index (this is not really surprising because indexed 
> datatypes can be explained with normal datatypes + the equality type, 
> so this is essentially the same as the first option).
>
> This exhausts my bag of tricks when it comes to proving two 
> constructor forms are not equal. This seems to be an essential problem 
> that would pop up any time one tries to mix coinduction with higher 
> constructors. It would be an interesting research topic to try and 
> define a suitable notion of "higher coinductive type" which does not 
> have this problem.

Right, but I think we current have no idea what cubical Agda's "higher 
coinductive types" are. It's interesting that Agda allows these, but 
they could as well be inconsistent. (That's why I asked about models 
before.)
-- Nicolai


>
> -- Jesper
>
> On Tue, Apr 2, 2019 at 10: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
>
>
>     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/4a3c73ff/attachment.html>


More information about the Agda mailing list