[Agda] Tentative guidelines for working with coinductive types
Anton Setzer
A.G.Setzer at swansea.ac.uk
Thu Jan 15 21:05:52 CET 2009
Here are some first thoughts concerning Nisses new approach of dealing
with codata:
- I think this gives a very easy way of interpreting codata in an approach
using coalgebras, which avoids the problem we always had that
when using coalg, many codata types become much longer.
If we look for instance at colist, which now reads
data Colist (A : Set) : Set where
[] : Colist A
_?_ : A ? ? (Colist A) ? Colist A
rename Colist to ColistShape and
define ? (Colist A) as Colist and expand that definition
we obtain
coalg Colist (A : Set) : Set where
? : Colist A -> ColistShape A
data ColistShape (A : Set) : Set where
[] : ColistShape A
_?_ : A ? Colist A ? ColistShape A
which is the way I originally was translating codata types into
coalg types.
So Nisses translation is very elegant, and reduces the overhead.
My impression however is that having coalg and having
Nisses definition as the most important part of the library
would be more appropriate.
The reasons are
- I have the feeling it is conceptionally clearer to add the
general case rather than only one instance.
- I believe that coalgebras in its general form will be used more
generally in the future.
We can see lots of coalgebras when we look at a (quite restricted however)
form of a class as in object oriented programming.
A class
class A
method1 : B -> C
method2 : D -> E
where B, C, D, E don't refer to A can be translated into
coalg A : Set where
method1 : A -> B -> C x A
method2 : A -> D -> E x A
or better
coalg A : Set where
method1result : A -> B -> C
method1effect : A -> B -> A
method2result : A -> D -> E
method2effect : A -> D -> A
If one looks with this point of view one sees that in object oriented
programming there are lots of occurrences of coalg.
One can argue of course that coalgebras can always be translated
into the simple form used by Nisse
For instance, if we have
coalg A : Set where
f1 : A -> B -> C
f2 : A -> D -> A
then this can be translated into (I am using here [] for box not for nil)
data A : Set where
[] : (B -> C) -> (D -> ? A) -> A
which translates back into my coalg
data Ashape : Set where
[] : (B -> C) -> (D -> A) -> Ashape
coalg A : Set where
? : A -> Ashape
This seems to work as well in the indexed case:
coalg A : I -> Set where
f1 : A i -> (b : B) -> C (g i b)
f2 : A i -> (d : D) -> A (h i d)
translates into
data A : Set where
[] : (i : I) -> ( (b: B) -> C (g i b) ) -> ( (d : D) -> ? (A (h i
d)) -> A i
But I have the feeling that this translation is slightly artificial,
the original coalg defintion is more neat.
When looking at streams one can see the advantages:
coalg Stream : Set where
head : Stream -> Nat
tail : Stream -> Stream
seems to me quite attractive and (depending on the taste or
the point of view one wants to make) for some applications
better than
data Stream : Set where
_::_ : Nat -> ? Stream -> Stream
What I like really about coalg is that it is completely symmetric
to data, and that it is categorically exactly the dual to data,
which I expect will result in lots of very clean code.
Nisses approach solves the problem of how to get the benefits
of codata without loosing the conceptual clarity of coalg.
In some sense I feel that coalg generalises record types:
record is just the degenerated case of a coalg with no recursive
occurrence of the type defined.
But these are just my first thoughts about it. I think a broad discussion
and lots of experiments are needed in order to clarify this issue.
Anton
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.
> >
>
-- --------------------------------------- Anton Setzer Department of
Computer Science Swansea University Singleton Park Swansea SA2 8PP UK
Telephone: (national) (01792) 513368 (international) +44 1792 513368
Fax: (national) (01792) 295708 (international) +44 1792 295708 Visiting
address: Faraday Building, Computer Science Dept. 2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk WWW: http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
--
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK
Telephone:
(national) (01792) 513368
(international) +44 1792 513368
Fax:
(national) (01792) 295708
(international) +44 1792 295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090115/08b62bfd/attachment-0001.html
More information about the Agda
mailing list