[Agda] Defining the Delay monad as a HIT in cubical agda
Andrea Vezzosi
sanzhiyan at gmail.com
Thu Apr 11 15:35:22 CEST 2019
This sounded like an interesting variation, however one can build this
proof which is terminating, even if agda does not recognize it so.
delay-never : delay {A = A} never ≡ never′
delay-never i .force = never
mutual
never′≡ : ∀ (x : Delay′ A) → never′ ≡ x
never′≡ x i .force = never≡ (x .force) i
{-# TERMINATING #-}
never≡ : ∀ (x : Delay A) → never ≡ x
never≡ x i = hcomp
(\ { k (i = i0) → later (delay-never k) ; k (i =
i1) → step x k })
(step (later (never′≡ (delay x) i)) i)
Would be interesting to see what happens in the model.
On Thu, Apr 11, 2019 at 2:03 PM Dan Doel <dan.doel at gmail.com> wrote:
>
> So, I thought about this a while longer.
>
> One thing to note is that you can avoid the coinductive proof working
> (I think) by making the argument to step inductive like so:
>
> data Delay A where
> now : A -> Delay A
> later : Delay' A -> Delay A
> step : ∀ d -> later (delay d) ≡ d -- delay d .force = d
>
> This still implies `later ≡ force`, but not the infinite path (you need a different
> one that I couldn't come up with to pass the termination checker, at least).
> Possibly sized types would let it still go through? I don't really know those
> well enough to say.
>
> -- Dan
>
> On Wed, Apr 10, 2019 at 7:16 PM Jon Sterling <jon at jonmsterling.com> wrote:
>>
>> It is not too surprising to me that this example turned out to be degenerate, considering that we do not yet know exactly what higher coinductive types are ;-) and whether they have anything to do with quotients of coinductive types....
>>
>> I'm optimistic that we can find ways to use (and constrain!) these tools which do not have such surprising results :)
>>
>> Best,
>> Jon
>>
>>
>> On Wed, Apr 10, 2019, at 7:05 PM, Dan Doel wrote:
>> > Actually, perhaps it isn't fair to say that it's an oddity in this case,
>> > because νμ is actually what we want for the lowest level, but not
>> > what we want for the path level, and it would be more odd for the
>> > fixed points to be swapped between levels.
>> >
>> > -- Dan
>> >
>> > On Wed, Apr 10, 2019 at 6:47 PM Dan Doel <dan.doel at gmail.com> wrote:
>> > > It seems like what's going on here is kind of related to the somewhat
>> > > odd behavior of coinduction in Agda in general, where every set of
>> > > definitions involving coinduction is always νμ. This means that there
>> > > is a never _path_ that chains arbitrarily many `steps` together. But
>> > > what you really want for things to work out is for the paths to be well
>> > > founded, so that an `== now x` has to eventually reach the now.
>> > >
>> > > Is this fixed by first defining the coinductive Delay, and then inductively
>> > > defining a HIT like:
>> > >
>> > > data Part (A : Set) : Set where
>> > > include : Delay A -> Part A
>> > > step : ∀ d -> include (later d) == include (force d)
>> > >
>> > > since the steps no longer tie through a coinductive type?
>> > >
>> > > On Tue, Apr 9, 2019 at 4:09 AM Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>> > >> On Mon, Apr 8, 2019 at 8:38 PM Nicolai Kraus <nicolai.kraus at gmail.com> wrote:
>> > >> >
>> > >> > Great!! :)
>> > >> > That means we know what this type is: Delay(A) = 1.
>> > >> > It's not so clear (to me) though how we can justify these higher
>> > >> > coinductive types.
>> > >>
>> > >> It seems that this example should make sense as a cubical set in the
>> > >> same style as the construction of HITs in CTT ?
>> > >> Just defined as a mixed inductive-coinductive type rather than purely inductive.
>> > >>
>> > >> https://arxiv.org/abs/1802.01170
>> > >>
>> > >> >
>> > >> > On 08/04/19 19:34, Andrea Vezzosi wrote:
>> > >> > > Oh, yeah, I hadn't thought about it, but indeed there's nothing
>> > >> > > special about "now" here.
>> > >> > >
>> > >> > > mutual
>> > >> > > never′≡ : ∀ (x : Delay′ A) → never′ ≡ x
>> > >> > > never′≡ x i .force = never≡ (x .force) i
>> > >> > >
>> > >> > > never≡ : ∀ (x : Delay A) → never ≡ x
>> > >> > > never≡ x i = step (never′≡ (delay x) i) i
>> > >> > >
>> > >> > >
>> > >> > >
>> > >> > > On Mon, Apr 8, 2019 at 8:11 PM Nicolai Kraus <nicolai.kraus at gmail.com> wrote:
>> > >> > >> Wow, thanks, Andrea!
>> > >> > >> Can this proof be extended to show that Delay(A) is contractible?
>> > >> > >> -- Nicolai
>> > >> > >>
>> > >> > >> On 08/04/19 19:01, Andrea Vezzosi wrote:
>> > >> > >>> Here is a proof that "never" is equal to "now x", making use of path
>> > >> > >>> abstraction and copatterns.
>> > >> > >>>
>> > >> > >>> mutual
>> > >> > >>> never′ : Delay′ A
>> > >> > >>> never′ .force = never
>> > >> > >>>
>> > >> > >>> never : Delay A
>> > >> > >>> never = later never′
>> > >> > >>>
>> > >> > >>> mutual
>> > >> > >>> never≡now′ : ∀ (x : A) → never′ ≡ delay (now x)
>> > >> > >>> never≡now′ x i .force = never≡now x i
>> > >> > >>>
>> > >> > >>> never≡now : ∀ (x : A) → never ≡ now x
>> > >> > >>> never≡now x i = step (never≡now′ x i) i
>> > >> > >>>
>> > >> > >>> Of course one still wonders what Delay really is.
>> > >> > >>>
>> > >> > >>> This definition is accepted because the corecursion goes through the
>> > >> > >>> coinductive projection ".force" and both "step" and application to"i"
>> > >> > >>> are considered guardedness preserving.
>> > >> > >>>
>> > >> > >>> On Tue, Apr 2, 2019 at 11:11 PM Nicolai Kraus <nicolai.kraus at gmail.com> wrote:
>> > >> > >>>> 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> 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 list
>> > >> > >>>>>> Agda at lists.chalmers.se
>> > >> > >>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> > >> > >>>>>>
>> > >> > >>>>>>
>> > >> > >>>>>> _______________________________________________
>> > >> > >>>>>> Agda mailing list
>> > >> > >>>>>> Agda at lists.chalmers.se
>> > >> > >>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> > >> > >>>> _______________________________________________
>> > >> > >>>> Agda mailing list
>> > >> > >>>> Agda at lists.chalmers.se
>> > >> > >>>> https://lists.chalmers.se/mailman/listinfo/agda
>> > >> >
>> > >> _______________________________________________
>> > >> Agda mailing list
>> > >> Agda at lists.chalmers.se
>> > >> https://lists.chalmers.se/mailman/listinfo/agda
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> >
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list