5
$\begingroup$

In the Foundations chapter of Elements of Programming (Stepanov and McJones, 2009), this paragraph appears:

A value type is properly partial if its values represent a proper subset of the abstract entities in the corresponding species; otherwise it is total. For example, the type int is properly partial, while the type bool is total.

I have a hard time understanding what this means and have been unable to find any good explanations of these terms on the Internet. What are properly partial and total value types?

$\endgroup$
  • 2
    $\begingroup$ Strange. I have never seen these terms before. Perhaps int is properly partial because its values do not really represent all integers? $\endgroup$ – xuq01 Jul 8 '18 at 18:09
3
$\begingroup$

$ \newcommand{\llbracket}{[\![} \newcommand{\rrbracket}{]\!]} $First, a proper subset is a subset that is not equal to the whole set. In other words, $A$ is a proper subset of $B$ iff $A \subseteq B$ and $A \ne B$.

If you formulate a denotational semantics for a language, then each type $T$ has an associated set $\llbracket T \rrbracket$ which is called the denotation of $T$. Stepanov and McJones calls this set the abstract species corresponding to the type $T$ (in this particular semantics). For example, it is natural to associate the set of integers $\mathbb{Z}$ to the type $\mathtt{int}$, with value semantics $\llbracket \mathtt{0} \rrbracket = 0$, $\llbracket \mathtt{1} \rrbracket = 1$, $\llbracket \mathtt{-1} \rrbracket = -1$, etc. and the set of truth values $\{\mathsf{T},\mathsf{F}\}$ to the type $\mathtt{bool}$ with value semantics $\llbracket \mathtt{false} \rrbracket = \mathsf{F}$ and $\llbracket \mathtt{true} \rrbracket = \mathsf{T}$.

A type is total under a denotational semantics iff the set of denotations of values of that type is equal to the denotation of the type. A type is properly partial iff is it not total, that is, iff the set of denotations of values is a proper subset of the denotation of the type. (The denotation of a value must be a member of the denotation of the type, otherwise the semantics is not valid, thus the denotations of values always form subset of the denotation of the type.)

For example, the set of denotations of values of the type $\mathtt{bool}$ under the semantics above is $\{\llbracket \mathtt{false} \rrbracket, \llbracket \mathtt{true} \rrbracket\} = \{\mathsf{F}, \mathsf{T}\} = \llbracket \mathtt{bool} \rrbracket$ so the type $\mathtt{bool}$ is total under this semantics. On the other hand, the set of denotations of values of type $\mathtt{int}$ consists only of values in the range $[-2^{N-1}, 2^{N-1}-1]$, assuming a typical implementation of the type $\mathtt{int}$ with $N$ bits, therefore $\mathtt{int}$ is properly partial under this semantics.

Note that the totality of a type depends on the chosen semantics. For example, under a semantics where the denotation of $\mathtt{int}$ is the integer range $[-2^{N-1}, 2^{N-1}-1]$, the type $\mathtt{int}$ is total.

”Abstract species“ and “properly partial” are not widespread terminology. As far as I know, they were coined by these authors.

$\endgroup$
  • 1
    $\begingroup$ I'm not even sure if I would say "coined". Have they been used by others in these senses? Sometimes authors just need names for concepts and aren't trying to set a trend (though that can certainly happening even if not intended). At any rate, these seem like not great names given the prevalence of "partial" and "total" already in denotation semantics. I mean, the type of total functions is almost certainly properly partial in most (simple-minded) denotational semantics, to start having fun with confusing terms. $\endgroup$ – Derek Elkins Jul 9 '18 at 0:05
  • $\begingroup$ I would agree. Those are bad names, and I am not sure in what context does the author use them. $\endgroup$ – xuq01 Jul 9 '18 at 9:11
0
$\begingroup$

As Gilles implies in his answer, properly partial types come about mostly from the need to model infinite concepts using either finite representations or finite computations (i.e., finite both in workspace and in runtime).

The space of integers is infinite, but computer memory is always finite, so even arbitrary precision integer libraries will have a maximum amount of memory that they can allocate to the length of binary numbers, suggesting that all attempts to encode the integers on computers will always result in types that are at best properly partial.

Carrying these definitions forward brings us to such terms as partial or nontotal procedures and total procedures, and the need for definition-space predicates to guard procedures that are nontotal (to confirm as a precondition that the inputs are within the definition space of the procedure, so that, e.g., operations don't overflow).

"Implementations of some total functions are nontotal on the computer because of the finiteness of the representation. For example, addition on signed 32-bit integers is nontotal."
Elements of Programming, Chapter 2

All of this is also somewhat related to value types as correspondences between species and datums, where a datum is a finite sequence of 0s and 1s. A datum is a representation of an entity, and the entity is the interpretation of the datum. The datum together with its interpretation is a value. A datum is well formed with respect to a value type iff that datum represents an abstract entity.

For example, every sequence of 32 bits is well formed when interpreted as a two's-complement integer; an IEEE 754 floating-point NaN (Not a Number) is not well formed when interpreted as a real number.
— Elements of Programming, Chapter 1

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.