6 - • Type Presuppositions in TCL

Summary

Having motivated and studied the properties and semantics of • types, I now turn to the way they influence the TCL rules for composition and presupposition justification. So in addition to the types we defined in chapter 4, I add to the TCL set of types a finite set of types of the form α • β, where α and β are well defined types. From the perspective of the λ calculus rules of application, • types behave pretty much like simple types; while they affect the subtyping relation in the way discussed in the last section, the effects of the internal structure of the complex type on the basic rules of the λ calculus are otherwise nil. The role of • types in type presupposition justification, however, is much more involved; the rules of • type presupposition justification exploit the internal structure of the • and introduce terms for its aspects. I turn to this now.

How to justify complex type presuppositions

The reader may have wondered why I bothered with the system of type presuppositions. Everything done up to now in TCL could be done in a slight extension of the λ calculus to take account of Simple Type Accommodation. However, • types present another way of justifying a type presupposition; and to make this sort of justification clear and cogent, we need the flexibility of TCL. Suppose, for instance, that a predicate passes a presupposition to its argument that it needs something of type p.