true ? 1 : "Hello"

Take a look at the Java expression on the left hand side. Off of the top of your head, can you tell me if it will type check? If so what will be its type?

If you had asked me this question out of the blue, I would have probably said no; I would reason it as follows: this is a Java expression, so it must be assigned a type, meaning that we’re giving a system of equations saying that the type of 1 and the type of "Hello" must be equal; this is clearly not the case as one is an Integer and the other a String, so this can’t possibly type check!

Of course, I’m actually just suffering from a common case of overlooking the obvious. It turns out that I’m forgetting about the whole subtyping thing built into Java and that I can actually assign Object o = true ? 1 : "Hello";, because the type Object sits at the of the type ordering.

1. Subtyping as Inequalities

Since we’re speaking of subtyping as a type relation anyways, let’s give it a symbolic name to make it easier for us: we’ll let and range over types in Java, and we’ll say

to mean that is a subtype of . Under one interpretation, we can think of this as saying that if we’re expecting a somewhere, we should theoretically be allowed to plug in a in its place and not expect weird or undefined behaviors as a result. Another perhaps more practical view is to claim that there exists some function called the coercion function (which we will denote, for the sake of historical consistency, ) that, given some subtype relation , will be able to translate an object of type into an object of type that behaves “similarly”.

Anyways, It’s obvious that both and (since everything’s a subtype of Object), so we can draw a subtyping hierarchy as a tree:

and we can type check true?1:"Hello" : Object. This seems to suggest that we can typecheck all instances of to some type if we can typecheck to , to , and . In otherwords, is an upper bound of the types of and .

Of course, upon closer inspection, it turns out that both Integer and String share another common supertype: Serializable.

So just as well, we could claim that the ternary expression above extends Serializable. But if we want to “assign” a type to an expression, we don’t just want its supertypes.

2. Most Precise Supertype

Looking at the type hierarchy above, it’s clear that the lower a type is on that hierarchy, the more “precise” it is. When we say that an expression has a type, we don’t mean that it is bounded above by some set of super types; we actually mean that its most “precise” type is so and so. For example, we could just as well draw the type hierarchy for Integers as

and claim that a is a Serializable; but when I typically talk about the type of the expression , I’m usually talking about Integer, not Serializable.

From this, it’s clear that we also want a way to find the most precise (smallest) type of true ? 1 : "Hello" such that it is also an upper bound of both and “Hello”; this is called the least upper bound, and we will for historical reasons call this the “join” of two types.

Symbolically, if we want to find the most precise upperbound (join) type of two types and , we will denote it as such that

the reason that the least upper bound is usually denoted as a square union symbol is actually somewhat natural: the union of two sets is the least upper bound of those two sets in the partial order (set inclusion), convince yourself that this is actually the case.

Note that whenever we join two types, the resulting type is “less precise”. We are after all finding an upper bound!

Going back to the problem at hand, the entire point of this exercise is then very simple: we want to find the least upper bound of Integer and String:

We’ve already seen earlier that both Object and Serializable are upper bounds of both Integer and String, but we also know that , so Serializable is a more precise (less) upper bound than Object is, but is Serializable the most precise?

In order to answer this question and find the least upper bound, we’re going to need the complete subtyping hierarchy. Consulting the Java documentation, we find that Integer is a subtype of Numbers, which are Serializable, and are themselves Comparable with other Integers. Furthermore, Strings are also Serializable and Comparable with other Strings! This gives the slightly more convoluted typing hierarchy:

3. Problems

At first first glance, it doesn’t seem possible that there’s a least upper bound: it seems like both Comparable and Serializable are the most precise upper bounds. Furthermore, this isn’t even necessarily true as Comparable itself might be too imprecise.

Wildcards and Bounded Quantifiers

Consider the constraint

now, we know that

so we can rewrite this as

by plugging in into the in . (Wildcards, amiright?) Similarly, we can say the same about integers, so we get

but we , so a more precise upper bound of is . But now, we can construct a sequence

each of which a more precise approximation than the previous, which undoubtedly converges to the most precise type: and here’s the kicker, that type cannot be expressed finitely!

So how does Java handle these types? Let’s try it out. I wanted Java to output the internal type representation, so I need to get a type-mismatch error during compile time.

Comparable Type

It seems as if Java is reporting the type of the two as an unbounded quantification: just Comparable<?>. This is intentional, Java treats the ? extends ... as a constraint (or a system of inequalities) and discards them during type checking and coercion in order to use them later solely for typechecking, so we seemed to have for now solved the problem (So even though , we’re going to treat them as if they weren’t).

No least upper bound?

But we still have another problem, there’s is no least upper bound in the above hierarchy! Again, let’s see what Java does:

Intersection Type

It turns out that the least upper bound is just the “intersection” over the three types, which should then be the LEAST upper-bound of all three.

If you’re like me, you spend your flight pondering the deepest and darkest corners of human knowledge, like

1. was the cashier flirting with me? (she wasn’t)
2. which one is better, the integral or the derivative? (definitely the derivative)
3. are we there yet? (no.)
4. are airlines the mortal enemies of tall people? (they are)

Of course, after a day of mentally exhausting travel, I’d like to sit back, relax, and ask myself how, given a specific type declaration in , I can figure out the number of all possible instances of that type.

For example, there is just one instance of the type unit (kind of funny because its name is unit) corresponding to the object in . There are two distinct instances of the type bool corresponding to the set , and about distinct instances of the type int.

1. Types in

Now, before we go on any further, let’s first take a look at the syntax of types.

this type declaration says that we want to create a new type whose instances are either labeled Diamond, Club, Heart, or Spade. The labels are capitalized to mean that they can serve as constructors of the type. So if you type in Diamond into the OCaml, it’ll construct an object of type suit corresponding to the Diamond label. Note that Diamond isn’t itself a type here.

It’s quite obvious that there are 4 distinct instances of the type suit that we can construct, namely .

We can also give each type constructor some extra stuff. For example, if we want types corresponding to the individual cards rather than suits, we can write something like

so that we can construct an instance of the card Jack of Clubs as Club 11. Here, there are different instances of the type (we’re only familiar with 52 of these). Alternatively, we can also write each card as a pair of a suit and an integer.

here, the notation suit * int stands for types whose objects are pairs, the first element of which is an instance of a suit and the second an integer; for example, Card (Club, 11) would be the jack of clubs.

One really interesting thing to observe here is that the two different ways of writing the card type above should be equivalent. In each, we are specifying a suit and also a value. Therefore, if there are distinct instances of the first type, there should also be instances of the second type, and it turns out, there are.

Furthermore, if we want to “parameterize” the types to be more generalized, we can do so by introducing type variables (variables that corresponds to types) as 'x that starts with a single apostrophe. So for example, if we want to build a linked list of whatever type we want, we could do something like

where the list of type int list (so we make the substitution ) is constructed from Cons(1, Cons(2, Cons(3, Null))).

A binary tree can be build up like

where the tree

has type int tree (so we make the substitution ) is constructed from

Node(
    Node(Leaf, 2, Leaf),
  1,
    Node(
        Node(Leaf, 4, Leaf),
      3,
        Node(Leaf, 5, Leaf)
)

2. Counting instances

One or unit

Now, we get to the interesting part. As discussed previously, we have already established that there’s only one object of the unit type (just ) and two (True and False) of the boolean type. Of course, there’s also only one object of the type

and in fact, we can rename the constructor to anything (assuming that we don’t care about it being valid ocaml code) including the unit object , so it turns out that is equivalent to all types with a single constructor and equivalence isn’t effected under renaming of the constructor (well, there are certain rules to this renaming/substitution, and we’ll call this property equivalence). But is this the only property that preserves the count of the number of instances? Well, no, as it turns out, the following all only have one element.

this is intuitive, if we have only one possible object for the argument of the constructor, and we only have that one constructor, then we can only construct one object for that type. In fact, from now on, we will say that an argument-less type construct C is just a syntax sugar for C of unit because doing so will not change the number of instances for that type.

Two or bool

We’ve also established that there are two instances of booleans, and . In type parlance, this would be

but remember earlier that we said if we give a type constructor not expecting any argument the unit argument, the type’s size is preserved. Therefore, we can rewrite the above as

and since renaming things doesn’t affect the size of the set of objects satisfying this type, this is also equivalent to

Neat. Let’s count up one more.

Three

There’s no native type in \f{OCaml} that only contains three instances, but it’s not too hard to guess how we’re going to construct this.

Here, we can either have or as instances of the type three. This gives a natural meaning to the notion of “or”. If I have types and , then the type

can either be one the or one of the , but since the two cases are necessarily distinct (because the label ), then if there are objects of type and objects of type , there must be objects of type .

It’s no coincidence either that the type is called a sum type between and (albeit for different reasons). Now that we’re warming to the notion that we can use these types almost as if we did in highschool algebra, let’s make some simplifications:

Since we do not ever care about what the labels themselves are, only that they are distinct, we can entirely leave out the labels for the type constructors. Therefore, we can write suit (type suit = Diamond of unit | Club of unit | ...) as

and the card type as either

or as

where the means the objects are of a pair type (with both a first and a second element). Note that we can also substitute suit directly in this type as in the second declaration of :

it’s no coincidence that there are also objects of type , but it’s also obvious that the two types are not equal syntactically. That is, .

Of course, it’s useful to construct another equivalence relation whereby type is translationally equivalent to type if both have the same number of type objects. In that case, we’ll say . As you probably have already guessed, we’re going to define some kind of a translation between these types into numbers denoting the number of objects of that type. We’ll go into detail more, but needless to say, we would translate as .

Four

Okay, at this point, we kind of already know what we are after. But first, I want to establish some basic laws seen in school algebra.

Recall that

and that

Now, obviously,

but let’s look at something else. Suppose we have a pair type such that

now, there are again four instances of , they are

so it seems as if as well. In fact it’s not hard to show that product types correspond to multiplication in the same that cartesian products corresponds to multiplication of the cardinality. (In fact, this question reduces to the cardinality of sets case).

Eight

Just to get to the point, how many functions are there for which the domain is of size and the codomain is of size ? For example, suppose that I have the type

where is taken to mean a function that maps a type with three elements to a type with two. Well, in general, suppose I have a function , then it turns out that there are such functions: reduce this problem to counting in base .

Suppose I have elements in that need to be mapped into . Suppose both and are finite and are order into the sequences and respectively, then I can encode one such function

and a second function

but since we don’t really want to clutter up the notation with all of the braces, the subscripts, and everything, we could just encode each function as a stream of digits where the digit = corresponds to which the element maps to. Then, we can just write

but this is the same as counting up to in base .

Anyways, from this argument, we would expect to have distinct objects, and hence .

3. The Translation

Let’s now define a translation between a simplified type declaration and a number denoting the total number of objects with that type declaration. We’ll write this relation . For now, pretend that is the naturals , but this will cause some subtle issues later on because we might not be able to translate certain types (like the list) directly into . Furthermore, is almost a function, but as discussed a few seconds ago, if we let be the naturals, it will not be able to translate certain types, so at best, it is a partial function. In that case, we will use the syntax to mean that .

To define this translation, let’s do it “recursively”. The validity of such a technique is beyond my scope, but convince yourself that because the right hand side is always translating smaller and smaller pieces, then eventually, the translation of any arbitrary type will terminate. Here, I will use to mean some type expression; that is, we will use it as a metavariable over the domain of types. Assume the same precedence level of as and power in school algebra.

Next, we define a notion of translational equivalence.

Translational Equivalence

note that is a weaker notion of syntactic equality of , therefore, if , then so too must owing to the fact that is a partial function. Furthermore, because of the construction of the sequence

then is obviously onto . However, because we need to have this notion of , it’s also very obvious that two different type expressions could have the same number of instances and hence is not one-one.

4. Examples

We’re going to take some extraordinary risks here (because we’re not mathematicians) and assume that this translation is correct (there are in fact many problems). Let’s do something with this new translation of ours

Associativity

Distributivity

in fact, under translational equality, we can manipulate types algebraically as if in school algebra. More amazingly, that means that we can encode everything the same exact way. Therefore, if we wanted to pass around an object of type , then we can instead pass around an object of type instead!

Parameterized Types (Advanced, skip if you want)

Suppose we wanted to translate the list type above:

unfortunately, we don’t have a definition of . Rather, we merely have an equation that is expected to be satisfied in order for an object to be considered an instance of the type. This equation is

it turns out that is the least fixed point of the function . This is going a bit beyond the scope of this post, but that least fixed point can be computed on the ordering of immediate sub-type expression which turns the sequence into a complete partial order (complete because all subsets contain a least upper bound). Therefore, by the fixed point theorem, that least upper bound is the mysterious expression (where means the least upper bound)

now, the translation function is “continuous” in the sense that it preserves least upper bounds on the CPO . (Of course, this is why we can’t have = ), but loosely speaking, the operations can be substituted as

therefore,

unfortunately, if , the above sum diverges to the top element in , .

However, an interesting question arises that this type of analysis can readily answer: how many instances of the list type are translationally equivalent to the -tuple. In this case, it turns out that for whatever base-type , there are exactly lists.

Of course, there’s a slightly easier hack which comes from the above derivation directly (namely because the translation preserves monotonicity, verify this!).

Lists – the easier way

Why don’t we just translate the equation directly?

We’ll get

In fact, we could even get this by solving the equation and finding its generating function.

Neat. However, this brings up a good question. Can all such equations be solved? Unfortunately, no.

Unheaded List – unsolvable

Let’s define a type

if we translate it, we get

now, if our codomain of the translation is just , then we would be forced to abandon hope. However, what we really did was we packed that codomain to include that you can think of as . What this can be interpreted as is that no matter what type variable becomes, type is going to diverge.

However, using the above trick, we still get the expansion

which says that all instances of are translationally equivalent to .

Binary Trees

Let

which under translation gives

where corresponds to the catalan numbers (i.e., we’re generating the sequence that count the number of binary trees translationally equivalent to the -tuple, which is the number of binary trees with nodes).

1. Uh Oh

This is puzzling, since it’s fairly obvious that is smooth everywhere; we can only conclude that floating point roundoff is to blame, and seeing the error manifest already on just an order of means that this equation itself isn’t enough to solve our problem. In fact, using arbitrary precision floating point arithmetic, we see that is indeed smooth within this region, so we know who the culprit is.

We’re plagued by roundoff because and are extremely close together, so the IEEE standard guarantees that their subtraction will be flawless. Well, if this subtraction doesn’t incur any error whatsoever, why is there round-off? While the subtraction itself is error-free, the same cannot be said of the . A crude bound analysis on the relative error of the form

and

where the function says whatever is in its argument will be evaluated under floating point arithmetic, represents one of the arithmetic operations or standard transcendental functions, and represents the relative error associated with an operation or with the representation of a number. Let’s look at the example in the problem. We’re going to assume that the subtraction gives no error, or that . Furthermore, let’s just for the sake of simplicity assume that is perfectly represented (so that as well, and since integers will never overflow, we have is perfectly computed as well)

This analysis is intriguing: it tells us that at the very worst, we can expect our relative error of the entire computation to be bounded by where each of the term is bounded above by , so the entire is bounded to an order of magnitude of . This spells out why the error gets blown up at around . Our relative error is basically , and the absolute error is then just , where when , the absolute error is around , which is definitely not good enough.

Hold on, the original relative error of the computation only incurred a relative error of just , why did the final error get blown up by that many orders of magnitude? (if you do the calculation, )? Here’s a more intuitive way of seeing this: when we computed , we got a small amount of relative error on a large number. However, this amounts to amount of absolute error. When we subtracted off the rest of the , we’re still left with an absolute error of , but this is the error on a much smaller number (), so the original absolute error now becomes a rather large amount of relative error.

2. The Fix?

Intuition plays a large role here since finding workarounds to floating point issues is pretty much a dark art. Here, the subtraction is actively amplifying our error, so what if we find some equivalent form of this expression that doesn’t subtract two large but close numbers? Through simple algebra, we see that by multiplying the conjugate we get

Is this form better? Let’s try it out.

In this case, getting rid of the subtraction got our method’s error down to just , which is much better than what we’re looking for.

1. A closed form equation for

function S = S(n)
    S = 1 - 1/(1+n);
end

It’s a really simple problem, and if you do a little bit of algebra, you can make the following simplification

From this, it follows immediately that , or . Great, now that we have a closed form expression for , what else do we need to do? Of course, just to make sure that my derivation is sound, I wrote out the full sum program anyways. (Note: this behavior will only happen when you use single precision floating point storage)

n = 1e6;
S = 0;
for k=1:n
    S = single(double(S) + 1/(k*(k+1)));
end
(1 - 1/(n+1)) - S

After computing for a few small values and comparing them to the value of , I found that seems to compute the same value as my expression; but for large values of , rapidly gets farther and farther away from the value computed by . I just attributed this to roundoff error, afterall, this is roundoff. I concluded that the more expensive summation isn’t a good solution at all and thought that was the end of it.

2. Uh oh

Later that day, I showed my friend this question and he told me that while he agrees that the closed form formula is indeed better, he sees no significant loss of accuracy in his implementation. For equals to a million, his solution only has amount of error (on par with for single precision) using only single precision storage types.

“What? No, that’s not possible, I already tried it on mine and I got an error of around ”
“Well, try it yourself”

So I ran his code in . At first I saw no difference in our two implementations, but then it hit me; “he’s computing the series backwards”

n = 1e6;
S = 0;
for k=n:-1:1
    S = single(double(S) + 1/(k*(k+1)));
end
(1 - 1/(n+1)) - S

and sure enough, I get the same error he does. What the hell is going on?

3. An explanation

It turns out that the problem stems from how roundoff works under certain rounding mode for addition. First, the IEEE guarantees that addition for floating point numbers that are within of each other will be perfectly computed.

Now, a single precision floating point number can store about 8 digits accurately, therefore, adding 1 to will only return 1 since the number will take more than 8 digits to store and hence will truncate the lower few digits. In general, you can assume that if two numbers differ by 8 orders of magnitude, then adding them will have no effect.

Now, when we compute the series in the forward direction, what we’re really doing is computing an approximation such that.

As we’ve already shown, , so at each iteration, we’re making the floating point computation . Relatively speaking, for large values of the expression tends towards just ; futhermore, will become more than 8 orders of magnitude away from 1 when is merely 10-thousand (however round off will be noticeable much earlier) therefore, for the last 999000 operations, our method is effectively doing nothing. You can actually verify this in by seeing that both and output the same long-formatted float when the true answer is about away.

Okay, so how does doing this summation in reverse help in any way or form? Well, suppose that each iteration of the reverse method produces a number at step , then it’s obvious that ; furthermore, for large enough value of , , so we can just have . The inductive definition also states that . Now, there’s something intriguing about this expression: so that the relative difference between and is around which is and can never exceed for (so the roundoff is at the worst in the beginning, but that’s also where this difference formula make assumptions that no longer hold, namely that the linear factor dominates the quadratic factor in , so the relative magnitude between the two terms isn’t really that big of a deal. Anyways, the roundoff will progressively become better and better as grows). Therefore, rather than having a significant vast majority of the computations do nothing, every step now counts. This is largely the reason why summing the series backwards gives less roundoff overall than doing the “same” set of operations in the other direction. This is one case where the “non-associativity” of arithmetic in floating point will give you trouble.

Next: How to fix floating point error

This gives the system of ODE

Unfortunately, we don’t know what is; but we do have the parameterization parameter , so we can solve the system backwards in time.

which is equivalent to the second order ODE

which has the solution

Now, we know that , so we want to find the time such that , or , then

and

Let’s quickly verify that this is indeed the solution

Since this is fully linear, the solution is unique and the characteristics intersect.

We first prove a useful lemma in working with algebraic manipulations in modular arithmetic.

1. Lemma:

Here, we take the traditional definition that .

2. Show that

By construction of the , we know that . It follow that

The last two lines of the above gives another congruence expression:

Suppose that as must be positive. Because are both relatively prime to , then by the above lemma, we know that

Likewise, we can divide out from both sides

this gives us our final congruence equivalence

Because, , the above simplifies down to .

Alternatively

The same logic above can be used to justify that , therefore, you can also show inductively, on the steps of the euclidean algorithm, that it preserves the properties of congruence mod m.

1. Find a closed form expression of

We start with the construction of .

Since the first term of our series is a one, and the terms alternate in sign on odd powers, we should only consider polynomials

Okay, but we still can’t completely remove the odd terms from the combinations. However, we see that if we were to add in another polynomial of the same degree, we can match up the terms so that the coefficients on the odd are canceled. That is, we find the pair such that

In order to get , we need to set

From this, we get the closed form expression of .

2. Find a recurrence relation for

This may seem counter-intuitive, but the problem looks like one that can be solved via induction on , which is much easier to do on a linear recurrence.

Recall from earlier and differential equation that is of the form of a linear recurrence with characteristic polynomial whose roots are . Let’s construct this polynomial in order to find the recurrence.

Recall that the characteristic polynomial of is , therefore, is the characteristic polynomial associated with

3. Show that

As brought up previously, we will prove this by induction on . Let , we will show that

This concludes our proof that .

We now construct a closed form expression for

Therefore, we see by construction that .

is linear in

We show this inductively on the naturals. Suppose , then, we show

This concludes our proof that for some number , and is hence linear in .

Therefore , and without loss of generality, we can replace with any arbitrary number. We will pick for the sake of simplicity.

Guess and check

Let’s generate a few numbers for with

This naturally suggests that

(1)  

Show that

We will prove this via induction on the naturals. Let , then from the table above, it is obvious that holds. We will now show that . Informally, we will expand the term within the first order recursive expansion of along with the equivalent construct . The body of the induction is as follows:

This concludes our proof that and the proof that does not depend on .

Therefore, , which means that .