<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    On 02/04/19 21:23, Jesper Cockx wrote:<br>
    <blockquote type="cite"
cite="mid:CAEm=boxOByinBT=Og8dXfGKfz5dPGkC2efdtUnBxx0f0rR2=0Q@mail.gmail.com">
      <div dir="ltr">
        <div>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</div>
      </div>
    </blockquote>
    <br>
    Right... the conjecture should be Delay(A) = Unit. I made a silly
    mistake before!<br>
    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.<br>
    <br>
    <blockquote type="cite"
cite="mid:CAEm=boxOByinBT=Og8dXfGKfz5dPGkC2efdtUnBxx0f0rR2=0Q@mail.gmail.com">
      <div dir="ltr">
        <div>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. </div>
      </div>
    </blockquote>
    <br>
    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).<br>
    <br>
    <blockquote type="cite"
cite="mid:CAEm=boxOByinBT=Og8dXfGKfz5dPGkC2efdtUnBxx0f0rR2=0Q@mail.gmail.com">
      <div dir="ltr">
        <div>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).</div>
        <div><br>
        </div>
        <div>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:</div>
        <div><br>
        </div>
        <div>- Pattern matching on an equality between two constructors
          with an absurd pattern () obviously doesn't work for higher
          inductive types.</div>
        <div>- 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).</div>
      </div>
    </blockquote>
    <br>
    `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?)<br>
    <br>
    <blockquote type="cite"
cite="mid:CAEm=boxOByinBT=Og8dXfGKfz5dPGkC2efdtUnBxx0f0rR2=0Q@mail.gmail.com">
      <div dir="ltr">
        <div>- 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).</div>
        <div><br>
        </div>
        <div>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.<br>
        </div>
      </div>
    </blockquote>
    <br>
    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.)<br>
    -- Nicolai<br>
    <br>
    <br>
    <blockquote type="cite"
cite="mid:CAEm=boxOByinBT=Og8dXfGKfz5dPGkC2efdtUnBxx0f0rR2=0Q@mail.gmail.com">
      <div dir="ltr">
        <div><br>
        </div>
        <div>-- Jesper<br>
        </div>
      </div>
      <br>
      <div class="gmail_quote">
        <div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at 10:06
          PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com"
            moz-do-not-send="true">nicolai.kraus@gmail.com</a>>
          wrote:<br>
        </div>
        <blockquote class="gmail_quote" style="margin:0px 0px 0px
          0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
          <div bgcolor="#FFFFFF"> 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?<br>
            (Maybe, at this point, we shouldn't call it "Delay" :)<br>
            -- Nicolai<br>
            <br>
            <br>
            <div class="gmail-m_-2314557868947509404moz-cite-prefix">On
              02/04/19 15:08, Jesper Cockx wrote:<br>
            </div>
            <blockquote type="cite">
              <div dir="ltr">
                <div>Hi Nicolai,</div>
                <div><br>
                </div>
                <div>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.</div>
                <div><br>
                </div>
                <div>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.</div>
                <div><br>
                </div>
                <div>-- Jesper<br>
                </div>
              </div>
              <br>
              <div class="gmail_quote">
                <div dir="ltr" class="gmail_attr">On Tue, Apr 2, 2019 at
                  3:15 PM Nicolai Kraus <<a
                    href="mailto:nicolai.kraus@gmail.com"
                    target="_blank" moz-do-not-send="true">nicolai.kraus@gmail.com</a>>
                  wrote:<br>
                </div>
                <blockquote class="gmail_quote" style="margin:0px 0px
                  0px 0.8ex;border-left:1px solid
                  rgb(204,204,204);padding-left:1ex">
                  <div bgcolor="#FFFFFF"> Hi Jesper,<br>
                    <br>
                    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. <br>
                    <br>
                    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).<br>
                    <br>
                    Thus, my guess is that Delay(Unit) could be
                    contractible. One could try to prove that every
                    element is equal to 'now'.<br>
                    <br>
                    Cheers,<br>
                    Nicolai<br>
                    <br>
                    <br>
                    <div
class="gmail-m_-2314557868947509404gmail-m_5865528187534997207moz-cite-prefix">On
                      29/03/19 18:40, Jesper Cockx wrote:<br>
                    </div>
                    <blockquote type="cite">
                      <div dir="ltr">
                        <div dir="ltr">
                          <div dir="ltr">
                            <div>Hi all,</div>
                            <div><br>
                            </div>
                            <div>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:</div>
                            <div><br>
                            </div>
                            <div>
                              <div style="margin-left:40px"><span
                                  style="font-family:monospace,monospace">data
                                  Delay (A : Set ℓ) : Set ℓ</span><br>
                                <span
                                  style="font-family:monospace,monospace"></span><br>
                                <span
                                  style="font-family:monospace,monospace">record
                                  Delay′ (A : Set ℓ) : Set ℓ where</span><br>
                                <span
                                  style="font-family:monospace,monospace"> 
                                  coinductive</span><br>
                                <span
                                  style="font-family:monospace,monospace"> 
                                  field</span><br>
                                <span
                                  style="font-family:monospace,monospace">   
                                  force : Delay A</span><br>
                                <span
                                  style="font-family:monospace,monospace"></span><br>
                                <span
                                  style="font-family:monospace,monospace">open
                                  Delay′ public</span><br>
                                <span
                                  style="font-family:monospace,monospace"></span><br>
                                <span
                                  style="font-family:monospace,monospace">data
                                  Delay A where</span><br>
                                <span
                                  style="font-family:monospace,monospace"> 
                                  now   : A → Delay A</span><br>
                                <span
                                  style="font-family:monospace,monospace"> 
                                  later : Delay′ A → Delay A</span><br>
                                <span
                                  style="font-family:monospace,monospace"> 
                                  step  : (x : Delay′ A) → later x ≡ x
                                  .force</span><br>
                              </div>
                              <br>
                            </div>
                            <div> 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: <a
href="https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9"
                                target="_blank" moz-do-not-send="true">https://github.com/jespercockx/cubical/commit/f1647a90c1b27aadd5da748f08e23630221cc3d9</a>
                              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.)<br>
                            </div>
                            <div><br>
                            </div>
                            <div>Cheers,</div>
                            <div>Jesper<br>
                            </div>
                          </div>
                        </div>
                      </div>
                      <br>
                      <fieldset
class="gmail-m_-2314557868947509404gmail-m_5865528187534997207mimeAttachmentHeader"></fieldset>
                      <br>
                      <pre>_______________________________________________
Agda mailing list
<a class="gmail-m_-2314557868947509404gmail-m_5865528187534997207moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="gmail-m_-2314557868947509404gmail-m_5865528187534997207moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
                    </blockquote>
                    <br>
                  </div>
                  _______________________________________________<br>
                  Agda mailing list<br>
                  <a href="mailto:Agda@lists.chalmers.se"
                    target="_blank" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
                  <a
                    href="https://lists.chalmers.se/mailman/listinfo/agda"
                    rel="noreferrer" target="_blank"
                    moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
                </blockquote>
              </div>
            </blockquote>
            <br>
          </div>
        </blockquote>
      </div>
    </blockquote>
    <br>
  </body>
</html>