[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