(in)finite binary trees

Stream: Is there code for X?

[Patrick Johnson]

What is the conventional way to define a type of binary trees that may be infinite? A naive way produces only finite trees:

inductive Tree
| nil : Tree
| pair : Tree → Tree → Tree

The following should work:

structure Tree
(f : list bool → bool)
(h : ∀ (l : list bool) (b : bool), f (l ++ [b]) → f l)

It essentially says: given a path (list of bools - left/right choices) in the tree, function f returns tt iff the node at the given path is a pair. Proof h asserts that nil has no child nodes.

The problem is that this definition is hard to work with and nontrivial to come up with for more complicated data structures.

[Yaël Dillies]

A coinductive definition would work I suppose. Can you use a W type in your application?

[Reid Barton]

docs#pfunctor.M

[Patrick Johnson]

Ok, seems like I need to study M-types and polynomial functors to better understand how they work.