[Agda] Tentative guidelines for working with coinductive types

[Noam Zeilberger]

This is a nice design pattern.  I was having trouble getting Agda to
accept some proofs about an equality relation ≡ for a little
coinductively defined language, and following these principles almost
all of the proofs went through easily.  The remaining problem seems to
be the weakness of Agda's definitional equality.  For example, I
define a cyclic term Ω in the syntax of the language, and then want to
prove that Ω ≡ Ω.  Well, I can prove reflexivity in general by
recursion on terms, but I'm having trouble proving Ω ≡ Ω directly.
(If this doesn't make any sense, I can try to come up with a small
example.)

My one thought about the proposed changes to Agda is that, while
they do make good sense, it might end up being easier and less
bug-prone to adopt the more general, destructor-based view of
coinductive types.

Noam

On Tue, Jan 13, 2009 at 03:26:48PM +0000, Nils Anders Danielsson wrote:
> Hi,
> 
> I think I have found a reasonably nice way to work with coinductive
> types in Agda. The method does not address productivity, which is a
> separate problem, but only evaluation, equality and similar things. It
> does seem to solve the problem with subject reduction.
> 
> This method works today with the current implementation of codata in
> Agda. In this message I do not consider the wider issue of whether we
> should switch to a destructor-based view of coinductive types, but I
> note that the method is inspired by Anton Setzer's ideas about
> destructor-based approaches, as presented in messages to this list.
> 
> Subject reduction
> -----------------
> 
> As observed by Anton the problem with subject reduction does not occur
> if a destructor-based view of coinductive types is used. Thierry
> Coquand observed in a privately circulated note that when the
> destructor-based view is used there is only one evaluation mechanism;
> there is no separate mechanism to "delay" an expression.
> 
> In the case of Agda it is the unfortunate combination of a delay
> mechanism (~) and dependent pattern matching which causes subject
> reduction to fail; codata per se does not have anything to do with it.
> (There may be other reasons for why subject reduction fails, I have not
> proved that Agda is always well-behaved; I only consider problems like
> the one raised by Nicolas Oury last year.)
> 
> Consider the following code:
> 
>   data D : Set where
>     d : D
> 
>   e : D
>   e ~ d
> 
> Here e is delayed, so Agda's definitional equality does not treat e and
> d as being equal. One can force delayed expressions by using pattern
> matching:
> 
>   force : D → D
>   force d = d
> 
> This appears to be unproblematic, but by using /dependent/ pattern
> matching one can prove that an unforced expression coincides with the
> forced one, because dependent pattern matching makes Agda "remember"
> the result of the pattern match, and hence also the result of forcing
> the delayed expression:
> 
>   force-eq : (x : D) → x ≡ force x
>   force-eq d = ≡-refl
> 
>   p : e ≡ d
>   p = force-eq e
> 
> Now we have a closed proof of e ≡ d, which means that p evaluates to
> ≡-refl. Unfortunately the term
> 
>   q : e ≡ d
>   q = ≡-refl
> 
> does not type check, though, so we have lost subject reduction.
> 
> To summarise: This particular problem with subject reduction can be
> avoided by never using dependent pattern matching to force delayed
> expressions.
> 
> Coinductive types
> -----------------
> 
> Let us now move on to coinductive types. Inspired by Anton's ideas
> about destructor-based approaches to coinductive types I suggest that
> there should only be a single "codata" type (plus variants for Set1,
> Set2 etc.):
> 
>   codata ∞ (T : Set) : Set where
>     ♯_ : T → ∞ T
> 
> This type comes with a destructor, which is the only function which is
> allowed to pattern match on ♯_:
> 
>   ♭ : ∀ {T} → ∞ T → T
>   ♭ (♯ x) = x
> 
> Coinductive types are then defined using /data/, but with ∞ annotating
> coinductive arguments (this was suggested by Thorsten Altenkirch):
> 
>   data Colist (A : Set) : Set where
>     []  : Colist A
>     _∷_ : A → ∞ (Colist A) → Colist A
> 
> This makes it easy to choose which arguments should be inductive and
> which should be coinductive, so we can for instance define stream
> processors in a nice way:
> 
>   data Stream (A : Set) : Set where
>     _∷_ : A → ∞ (Stream A) → Stream A
> 
>   data SP (A B : Set) : Set where
>     get : (A → SP A B) → SP A B
>     put : B → ∞ (SP A B) → SP A B
> 
> Note also that the use of data plus ∞ corresponds quite closely to
> Anton's explanation of codata in terms of mutual coalg and data. The
> data part is put on the outside, though, so the destructor ♭ is
> applied in the (co)recursive calls instead of before pattern matching
> can take place, which means that we can avoid Anton's use of with:
> 
>   map : ∀ {A B} → (A → B) → Colist A → Colist B
>   map f []       = []
>   map f (x ∷ xs) = f x ∷ rec
>     where rec ~ ♯ map f (♭ xs)
> 
>   eat : {A B : Set} → SP A B → Stream A → Stream B
>   eat (get f)    (a ∷ as) = eat (f a) (♭ as)
>   eat (put b sp) as       = b ∷ rec
>     where rec ~ ♯ eat (♭ sp) as
> 
> Note above that ~ is only used right before ♯_. This ensures that the
> delayed expression can always be forced using ♭. If ~ is never used
> anywhere else this also ensures that we do not get the subject
> reduction problem discussed above, because dependent pattern matching
> on ♯_ is not allowed.
> 
> Proofs
> ------
> 
> Let us now see how one can state and prove properties about
> coinductive values. Indexing on coinductive values seems to be fine,
> but just as it is sometimes a bad idea to use functions in a
> constructor's index expressions, it can also be a bad idea to use ♯_.
> I suggest using destructors instead, as in the following definition of
> colist equality:
> 
>   data _≈_ {A} : (xs ys : Colist A) → Set where
>     []  : [] ≈ []
>     _∷_ : ∀ {x y xs ys} → x ≡ y → ∞ (♭ xs ≈ ♭ ys) → x 
>     ∷ xs ≈ y ∷ ys
> 
> Because the destructors are applied exactly where they are needed it
> is often straight-forward to prove things:
> 
>   map-cong : ∀ {A B} (f : A -> B) {xs ys : Colist A} ->
>              xs ≈ ys -> map f xs ≈ map f ys
>   map-cong f []         = []
>   map-cong f (x≡ ∷ xs≈) = ≡-cong f x≡ ∷ rec
>     where rec ~ ♯ map-cong f (♭ xs≈)
> 
> Equality
> --------
> 
> When comparing this approach to coinduction with others it should be
> noted that Agda's definitional equality is perhaps a bit weaker than
> one might want, because delayed expressions are compared by name.
> Given the definitions
> 
>   x ~ ♯ z
> 
> and
> 
>   y ~ ♯ z
> 
> x is not definitionally equal to y. In ΠΣ, Thorsten and Nicolas' core
> language, the (equivalent) expressions are definitionally equal
> because in ΠΣ boxes (expressions headed by ♯_) are compared for some
> notion of α-equality. As discussed by Thorsten this can lead to
> another problem with subject reduction
> (http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104), so if Agda's
> definitional equality were strengthened one would have to take care to
> avoid this issue.
> 
> Possible changes to Agda
> ------------------------
> 
> You may have noticed that there are some rough edges to the approach
> outlined above. Some small changes to the way Agda handles coinduction
> would make it nicer. Specifically:
> 
> • Remove codata and ~ from the language.
> 
> • Make ∞, ♯_ and ♭ builtin (with rebindable notation, like sizes 
> have
>   now). Perhaps it is necessary to have one instance of this triple
>   for every universe level, but it would be nice if this could be
>   avoided.
> 
> • Do not allow pattern matching on ♯_.
> 
> • Treat ♯_ as a constructor when checking guardedness.
> 
> • Insert a virtual ~ in front of every use of ♯_.
> 
>   If ~ could be used in let one could translate C [♯ e] to
>   C [let r ~ ♯ e in r]. It would be nice if the user did not have to
>   see the fresh variable r, though. This translation would also imply
>   that the user has no direct way to refer to the delayed expression,
>   which can be annoying.
> 
>   The first problem can perhaps be solved by writing out the
>   right-hand side of the expression, instead of some fresh variable.
>   However, this could be confusing to the user, because one could
>   easily end up in a situation where Agda prints out the goal type as
>   "e ≡ e", but the goal is nevertheless not provable. With a stronger
>   equality between delayed expressions this situation could perhaps be
>   avoided, though.
> 
> These changes seem to be pretty easy to implement, unless we decide to
> switch to a different equality.
> 
> -- 
> /NAD
> 
> 
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses, which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>