The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

roconnor AT theorem.ca
 wrote:
> On Sat, 7 Jun 2008, 
> roconnor AT theorem.ca
>  wrote:
> 
>> But I worry that there are (as you say) more snakes.  CoInductive
>> types are very strange.  They are the only objects where computation
>> "simplfies" the introduction rule (cofix) rather than simplifying the
>> elimination rule.
> 
> I think I'm wrong about this point.  match is the eliminator and cofix
> is the introducution (with cons being a sort of degenerate cofix).  This
> makes match (cofix ...) ... a redex, which indeed seems to be what Coq
> does.
> 
> My reference on CoInductive types is just one section from "Type Theory
> and Functional Programming" (where his "computation rule" operated on
> the cofix).  What is the reference that details the rules for
> coinductive types in Coq?
> 

Hi,

Regarding Coq, the main reference is Eduardo Gimenez' thesis, available
at ftp://ftp.inria.fr/INRIA/LogiCal/Eduardo.Gimenez/thesis.ps.gz
(maybe at some point the LogiCal will become TypiCal, that sweet INRIA
habit to rename everything every 4 or 8 years)

He mentions the problem about subject-reduction (and that's the reason
why coinductive types were not formalized in "Coq in Coq"), so this not
quite new, although it is not so well known.

In fact, a weaker form of subject reduction holds: if M:T and M->M' then
M':T' for some T' convertible to T if we allow free expansion of cofix
(i.e. not only in the context of a match). But if we have free
expansion, then conversion becomes undecidable (hint: we can think of
potentially infinite lists as execution traces of Turing machines, and
we can probably encode the halting problem as a conversion problem).

So, there is a trade-off to make between subject-reduction and
decidability of type-checking (at least in the current setup). Eduardo
argued that in practice decidablility is more useful than
subject-reduction. This will probably sound weird to theorists, but
notice that the lack of SR is hardly noticed after more than 15 years of
use of Coq, while I bet non-termination would have been spotted quickly,
regardless of how clever the conversion strategy would be.

Put it in another way, there is a system that enjoys SR but not
decidability (the one with free expansion), and Coq implements a
(decidable) sub-system that does not enjoy SR.

Personally, I'm not fully satisfied by the current situation. If we are
going in the direction of invalidating forall x, x = out x (by forbiding
dependent elimination of streams), Leibniz equality on coinductive types
will become even more useless, and setoid rewrite is your life jacket.
The OTT approach seems highly desirable then.

Bruno.