[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-14 20:36, Noam Zeilberger wrote:
> 
> 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.

I think that the simplest implementation of the destructor-based view
would be almost identical to what I suggested.

In the simplest case we can settle for a single "corecord" type,
analogously to the codata type which I suggested, and almost identical
to the "coalg" type which Anton suggested in "Getting codata right":

   corecord ∞ (A : Set) : Set where
     ♭ : A

We can then define the "constructor" ♯_:

   ♯_ : ∀ {A} → A → ∞ A
   ♭ (♯ x) = x

Streams and stream equality can be defined as follows, just as in the
constructor-based approach:

   data Stream (A : Set) : Set where
     _∷_ : A → ∞ (Stream A) → Stream A

   data _≈_ {A} : Stream A → Stream A → Set where
     _∷_ : ∀ x {xs ys} → ∞ (♭ xs ≈ ♭ ys) → x ∷ xs ≈ x ∷ ys

We can also define an infinite stream of ones:

   mutual

     ones : Stream ℕ
     ones = 1 ∷ ones′

     ones′ : ∞ (Stream ℕ)
     ♭ ones′ = ones

Let us now see if we can prove that ones is equal to its own unfolding
(almost) with the simple corecursive proof that did not work for "inf"
in another message in this thread:

   eq : ones ≈ 1 ∷ ♯ ones
   eq = 1 ∷ eq′
     where
     eq′ : ∞ (♭ rec ≈ ♭ (♯ones))
     ♭ eq′ = ?

With the simplest implementation of evaluation and equality (i.e. more
or less the one which is already implemented) the goal type evaluates to

   1 ∷ ones′ ≈ 1 ∷ ones′,

which can be proved using reflexivity, but not using a corecursive call
to eq:

   eq : 1 ∷ ones′ ≈ 1 ∷ ♯ (1 ∷ ones′).

This mirrors the current situation exactly.

By generalising wildly from this simple example it seems to me as if the
destructor-based view is completely equivalent to the constructor-based
one, as long as the ∞-approach is used. In this setting the issueof
definitional equality seems to be orthogonal to the issue of
constructor vs. destructor.

I should perhaps mention that you can have something very similar to the
destructor-based view already now (I had not realised that before):

   record Stream (A : Set) : Set where
     field
       head : A
       tail : ∞ (Stream A)

   open Stream

   map : ∀ {A B} → (A → B) → Stream A → Stream B
   map f xs = record { head = f (head xs)
                     ; tail = map′
                     }
    where map′ ~ ♯ map f (♭ (tail xs))

This is accepted by Agda now. With my suggested changes to Agda the code
would be nicer:

   map : ∀ {A B} → (A → B) → Stream A → Stream B
   map f xs = record { head = f (head xs)
                     ; tail = ♯ map f (♭ (tail xs))
                     }

-- 
/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.