[Agda] Defining the Delay monad as a HIT in cubical agda
Nicolai Kraus
nicolai.kraus at gmail.com
Tue Apr 2 23:11:13 CEST 2019
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
> <mailto: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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto: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/4a3c73ff/attachment.html>
More information about the Agda
mailing list