next up previous contents index
Next: Details of the Up: Inductive Types Previous: Inductive Types

Expressiveness and Elegance

The transfinite W--type of well--founded   trees, , used to represent Brouwer  ordinals is inexpressible in the Nuprl logic discussed in the earlier chapters but can be represented in the logic extended by rec types as rec(w. x:A#(B->w)). The data type for programs given in chapter 11,

     d:N#ind(d; x,y.void; void; x,T. Atomic_Stmt | (T#T) | 
                                     (expr#T) | expr#T#T),
can be written more elegantly as
     rec(T. Atomic_Stmt | (T#T) | (expr#T) | expr#T#T).
The list type constructor is now redundant because A list can be expressed as rec(l. NIL | A#l).

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995