[Agda] Changes to coinduction

[Nils Anders Danielsson]

Hi,

I have changed the way Agda handles coinduction and corecursion. The
changes are as follows:

* Dependent pattern matching on coinductive constructors is not
  allowed.

* ~ has been removed. All coinductive constructors are now "lazy". The
  semantics is similar to what we had before: Every coinductive
  constructor application c args is translated into an application
  fresh tel, where tel is a list of variables corresponding to the
  current telescope and fresh is defined by fresh tel = c args. The
  application in the body of fresh is not translated again (of course),
  and the definition of fresh is delayed as if it had been defined
  using ~.

The reason for the second change is that I got tired of writing things
like

  map : ∀ {A B} → (A → B) → Stream A → Stream B
  map f (x ∷ xs) = f x ∷ map′
    where map′ ~ ♯ map f (♭ xs).

Now you can write

  map : ∀ {A B} → (A → B) → Stream A → Stream B
  map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

instead.

There are some problems with this approach:

* Two delayed applications of a coinductive constructor are not
  definitionally equal unless they come from the same location in
  the source code. This problem is a bit worse than when ~ was used,
  because now /every/ application is delayed.

* The name "fresh" is automatically generated and cannot be used in
  the source code. (I use a name derived from the name of the
  constructor.)

* The only way to delay evaluation is to use a coinductive
  constructor, so there is less scope for abstraction: definitions
  which need to be delayed /must/ use coinductive constructors, even
  if the termination checker has been turned off.

There is also a limitation which I hope will soon be lifted (by someone
more knowledgeable in the internals of Agda):

* Coinductive constructors may not occur in the scope of let-bound
  variables.

Note that the support for coinduction and corecursion in Agda is still
experimental, and subject to change.

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