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 t⁴). 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 definedness⁵.
Alternatives:

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.