The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 04/09/2014 16:27, Thorsten Altenkirch a écrit :

Is there any use of positive inductive types? I lack any intuition about such types. They seem to be a formalist invention.

Hi Thorsten.

Note that formalist inventions can have unexpected applications. The history of mathematics offers many examples. ;-)

Here is an application in algorithmic due to Martin Hofmann (unpublished 5-pages note "Approaches to recursive data types - a case study", 1995; cited in Ralph Matthes' lecture notes on "Lambda calculus: a case study for inductive definitions", 2000). See pages 61-63 of Ralph's lectures notes (http://www.irit.fr/~Ralph.Matthes/papers/esslli.pdf). One defines the type of continuations as follows:

cont = D | C of (cont -> list) -> list

and use it to compute the list of labels of a labeled tree in breadth-first order.

Best regards,

Frédéric.