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

[Dan Doel]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190411/ecf5a171/attachment.html>