![]() |
Subject: Changes to coinduction Newsgroups: gmane.comp.lang.agda Date: Tuesday 17th March 2009 00:49:08 UTC (over 9 years ago) 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. |
||