[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

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.