[Agda] Defining the Delay monad as a HIT in cubical agda
Jesper Cockx
Jesper at sikanda.be
Thu Apr 11 18:17:10 CEST 2019
Hi,
Thanks for all the interesting replies, in particular to Andrea for proving
that my definition of Delay is contractible (which I was already beginning
to suspect but was unable to prove).
I have a new proposal for the definition of Delay as a mixed
inductive-(higher inductive)-coinductive type:
```agda
open import Agda.Builtin.Size
open import Cubical.Core.Prelude
variable
ℓ : Level
A : Set ℓ
x : A
data Delay (A : Set ℓ) (i : Size) : Set ℓ
data Delay↘ (A : Set ℓ) (i : Size) (i′ : Size) : Delay A i → A → Set ℓ
record Delay′ (A : Set ℓ) (i : Size) : Set ℓ where
coinductive
field
force : {j : Size< i} → Delay A j
open Delay′ public
data Delay A i where
now : A → Delay A i
later : Delay′ A i → Delay A i
norm : {d : Delay′ A i} {j : Size< i}
→ Delay↘ A j i (d .force) x → later d ≡ now x
data Delay↘ A i i′ where
now↘ : ∀ x → Delay↘ A i i′ (now x) x
later↘ : {d : Delay′ A i} {j : Size< i}
→ Delay↘ A j i′ (d .force) x → Delay↘ A i i′ (later d) x
_↘_ : {A : Set ℓ} {i i′ : Size} → Delay A i → A → Set ℓ
_↘_ {A = A} {i} {i′} = Delay↘ A i i′
```
The main difference with the previous proposal (apart from the Sizes) is
that Delay is defined mutually with an *inductive* relation `Delay↘ d x`
expressing that `d` terminates with value `x`, and the higher constructor
of Delay takes an argument of this type. In particular, the higher
constructor no longer takes a recursive argument so it's no longer possible
to construct the infinite sequence of `step`s in Andrea's proof.
I wonder whether we can prove for this definition that:
1. it is a monad
2. `now x` is not equal to `never`
I suspect 2 is currently not provable in Agda, but it seems to be a
technical limitation rather than a real problem with this definition.
-- Jesper
On Thu, Apr 11, 2019 at 3:36 PM Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> 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
> _______________________________________________
> 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/4e963a42/attachment.html>
More information about the Agda
mailing list