Less recursion in type defs
Date: Wed, 29 Mar 89 12:43:15 +0200
>Argument for less recursion in datatype definitions ...
>I'd love to know what camps exist on this. Are there other
>strong opinions out there on the pros and cons of defining data
>types directly by recursion vs. indirectly on simpler bases?
Any time I am teaching (initial) type recursion I am short of good
examples. All of them boil down to various kinds of finitely branching
trees defined by systems of mutually recursive type definitions using
Cartesian product and strong union. In other words, they are
translations of context-free grammars to type equations. Once the
students have seen that, there is little left in the subject to keep
them from yawning.
Here follows a non-standard definition of trees:
tree = empty
| CONTENTS x (ALPHABET --> tree)
They are infinitely branching if ALPHABET is infinite, still this
recursive equation can be expressed in existing applicative languages
(e.g. in ML). This is the only example I know, of a type equation that
does not directly correspond to a context-free grammar and still
may be considered of some practical value.
Are trees the only recursive types worth mentioning? If yes, then I
would whole-heartedly support
> ... the approach of defining data structures as functions on
>ordinals and other suitable structures such as graphs instead of
>directly by recursion.
ICS PAS, Gdansk, Poland
Temporarily: Universitaet Passau, Germany