Prev Up Next
Go backward to 4 Product types and arities of functions
Go up to Top
Go forward to 6 Predicate types

5 Partial function spaces and partial types

Design proposal: Allow total and partial function spaces and, moreover, the type constructor "?", where for a type t, ?t > t is the type that extends t by an "undefined" element. The semantics of ?t is t united with a new "undefined" element (this is isomorphic to, but not necessarily equal to the partial function space [() -> ? t] from the empty product to t4). Homomorphisms have to reflect (but not necessarily preserve) the undefined element. This is different from what one might expect, but fits well the CASL approach to partiality and in particular the intuition that initial models are those with no junk, no confusion and minimal definedness5.

  1. Allow just total and partial function spaces. This does not restrict expressiveness, but is no extension of first-order CASL, where we have partial constants of type ?t.
  2. Allow total function spaces and the type constructor "?". Then a partial function from t to u can be obtained through a total function from t to ?u. This can be considered to be a kernel language for the current proposal.

CoFI Note: L-8 ---- 7 January 1998.
Comments to

Prev Up Next