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

Nicolai Kraus nicolai.kraus at gmail.com
Wed Apr 3 00:58:07 CEST 2019


Hi Martin, thanks for the pointers! Of course, we should keep all of 
this great work in mind.
Best wishes,
Nicolai

On 02/04/19 22:13, Martin Escardo wrote:
>
> I want to make some comments about the delay monad and partial
> functions in Agda, in Coq, and more generally in Martin-Loef type
> theory and dependent type theory.
>
>  1. Once you you quotient the delay monad, you are entering the realm
>     of "lifting monads with respect to a dominance", which were
>     studied extensively in 1980-2000.
>
>     This is work by lots of people, including Pino Rosolini
>     (supervised by Dana Scott), Martin Hyland, Paul Taylor, Alex
>     Simpson, John Longley, and many more people. I think this work
>     should not be neglected, not only because of credit reasons, but
>     also because it has many interesting things to say that we don't
>     need to invent again.
>
>  2. An attempt to bring the above work (1) to the realm of dependent
>     type theory, and in particular to to univalent foundations, is
>     developed by Cory Knapp and myself (CSL'2017).
>
> https://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf
>
>  3. A practical test of (1) and (2) is given by Tom de Jong
>     https://github.com/tomdjong/UniMath/blob/paper/paper.pdf
>
>     What this does it to implement old ideas of Scott in the realm of
>     dependent type theory, using the UniMath system, to (a) give an
>     operational semantics to a programming language, called PCF, with
>     non-terminating programs, (b) use a lifting monad in the good old
>     sense of (1) above to give a denotational semantics for the
>     language, and (c) prove in type theory that the operational and
>     denotational semantics of the language coincide at ground types
>     (which is known as "computational adequacy", since the 1970's,
>     with the work of Gordon Plotkin).
>
> I read the above and hear myself preaching. I don't like
> preaching. But while I love the new ideas that are the result of
> dependent type theory, HoTT, univalent mathematics, cubical type
> theory, cubical Agda, and so on, I still think we should pay attention
> to the great things that were done not that long ago (even if it was
> in the previous millennium). We should not reinvent the wheel
> (although it may be fun to rediscover things on our own, I must say).
>
> Best,
> Martin
>
>
>
> On 02/04/2019 21:23, Jesper at sikanda.be 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
>>
>> 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. 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).
>> - 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.
>>
>> -- 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
>>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> -- 
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe



More information about the Agda mailing list