Properties of patterns and copatterns:
| Patterns | Copatterns |
|---|---|
| Finite data | Infinite data |
| Initial objects | Final objects |
| Inductive types | Coinductive types |
| Positive types | Negative types |
| Sums | Products |
| Least fixpoints | Greatest fixpoints |
| Lists | Streams |
| Natural numbers | Function spaces |
| Constructors | Observations |
| Pattern matching | Copattern matching |
| case...of | merge |
| Checking | Synthesis |
| Introduction forms | Elimination forms |
Tuples are inductive or coinductive?
In his blog post, The Point of Laziness, Bob Harper lashes out at laziness once again. In this post, positive and negative types show up in a very interesting point, namely, that lazy languages have products, but not sums, and eager languages have sums, but not products. A question remains whether this applies to inductive and coinductive types in general, or just these two types in particular.
In Codatatypes in ML, tuples are defined as coinductive types, thus making them negative types. In fact, they are defined through observations, namely, "fst" and "snd".
However, in Copatterns, for bidirectional typechecking, tuples have checking rules, thus making them positive types. Bob Harper's blog post Polarity in Type Theory shows (if I understand correctly) that we can either define, in this particular case, tuples either as an inductive or coinductive type.
Finally, in Section 6 of Copatterns, there is a coinductive definition of tuples. This definition, however, makes bidirectional typechecking incomplete.
Tags: type theory