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
Read the rest of this entry »