[TYPES] Representing inductive types with W-types

[Kristina Sojakova]

Dear Russell,

I do not necessarily see anything ad-hoc about the particular encoding 
of tress as

Tree A ~ W (a,n):A*nat. Fin n

On the other hand, I find it very natural. After all, a tree is 
determined by
1) a term a : A, which is the value at the root
2) a term n : nat, which is the number of children
3) n subtrees
Each pair (a,n) will determine a separate constructor, thus the type of 
constructors will be A x nat. Since the arity of the constructor (a,n) 
is n, we need a dependent type
(a,n) : A x nat |- B(a,n) type
such that B(a,n) is inhabited by exactly n terms. As we see the value of 
a does not matter for this requirement, thus we need a type
n : nat |- B(n) type
which is inhabited by precisely n terms, which is the specification of 
Fin(n).

You are right that the types nat and Fin do not occur in the Coq 
definition of Tree A explicitly and have to be inferred at the 
meta-level. So if you are asking whether it is possible to derive a 
completely generic way to encode suitable data types (as in, a precise 
algorithm) then the answer is probably not. There has been some work 
done by Gambino&Hyland
in their paper "Wellfounded trees and Dependent Polynomial Functors":
http://www.math.unipa.it/~ngambino/Research/Papers/gambino-hyland.pdf
They show that certain class of inductive types corresponding to the 
dependent polynomial functors can be represented by W-types (which 
correspond to non-dependent polynomial functors). I am not sure if this 
is what you were looking for though.

Best,

Kristina