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

[Jesper Cockx]

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

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

-- Jesper

On Tue, Apr 2, 2019 at 10:06 PM Nicolai Kraus <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>
> 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/c8045668/attachment.html>