Epilogue

I thought I’d just collect together some disparate observations about W-types, and their use in encoding other recursive datatypes. My motivation, bluntly, is to point out the inevitable unsuitability of W-types as the basis for recursive datatypes in an implementation of decidable type theories. I don’t want to downplay the conceptual importance of W-types as a uniform basis for recursive structures in an extensional setting. I’m just saying that computers aren’t clever enough to cope all that well with W-type encodings: if we want to make our understanding go, we need to refine it. This is a long post, so if you want the bad news first, skip to the end.

What are W-types?

Martin-Löf identified a general notion of well-ordering — data with a well-founded notion of ‘structurally smaller’. The power of dependent types enabled him to express this parametrically, once for all, rather than by fiddling about with syntactic criteria for acceptable recursive definitions. Here goes (informal notation)

W (S : Set) (P : S → Set) : Set
(s : S) ⊲ (f : P s → W S P) : W S P
(more…)

I’ve had an enquiry for more details on quotients in the new Epigram setup, so I’ll take that as a cue to blog a bit.

First, I’d better sketch some basics about propositions and equality. It’s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible thus far in a decidable type theory. The headlines:

• quotients given by a ‘carrier’ set, equivalence relation
• definitional equality on equivalence classes inherited from carrier on representatives
• propositional equality on equivalence classes is equivalence of representatives
• propositional equality is substitutive

The tabloid headline is STUFF YOUR SETOIDS.
(more…)