[Agda] Defining the Delay monad as a HIT in cubical agda
Martin Escardo
m.escardo at cs.bham.ac.uk
Tue Apr 2 23:13:01 CEST 2019
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