17 Nov 2011 23:50

## [TYPES] Representing inductive types with W-types

```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Russell,

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
```