Subsets

Given a contract like nat32, we can define contracts that are more restrictive:

var positive32 = function (n) {
  nat32(n);
  if (n === 0) {
    throw new TypeError('Expected a ' +
        'strictly positive integer.');
  }
  return n;
}

The set of values that pass the positive32 contract is a subset of the values that pass the nat32 contract. A subcontract S of a contract C is a contract such that if a value v passes S, then it also passes C. The contract positive32 is therefore a subcontract of nat32.

For any contract C, there is a category whose objects are all the subcontracts of C and whose morphisms are injections. This is a subcategory (defined in the obvious way) of the category of all contracts and injections between them.

Advertisements

6 Comments to “Subsets”

  1. Maybe I have missed it. Could you please provide the code for the function “nat32”. Thanks.

    • The definition of nat32 was given way back here. But just for reference, it’s

      var nat32 = function (n) {
        if ((n | 0) !== n || n < 0) {
          throw new TypeError('Expected ' +
              'a natural number.');
        }
        return n;
      };
      
  2. Thanks. Now I have found it. It is within the “contracts” post.

    Just one more question. I don’t understand why (n|0) !==n catches all values >= 2^32. As far as I know the operator “|” is a bitwise “or”. So (n|0) should always be equal to n.

    • JavaScript has two numeric types masquerading as one. Most of the time it uses IEEE 754 floating point (except that -0 == +0 and -0 === +0), but when using bitwise operators like |, &, ^, >>, and <<, the floating point number is cast to a 32-bit signed integer by a complicated algorithm, then the operator is applied, and the result is cast back. You can read about the complicated algorithm in section 9.5 of the language spec.

      • Interesting. But shouldn’t you call your function “nat32” better “nat31”?.

        As far as I understood the spec, in the expression “n|0” the number n is first converted to an int32 number which can represent only values x: -2^31 <= x < 2^31, i.e. the numeric value 2^31 will be chopped to zero, because it does not fit into the range. Therefore (2^31|0)!==2^31 and the exception is thrown.

        Sorry for being that pedantic. But I am eager to understand it. Did I miss something?

        • No, you’re right; I originally defined int32 but because arrays can’t have negative lengths, I changed int to nat. Think of it as “the natural numbers intersect int32”.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: