Once Upon an Algorithm

Home > Other > Once Upon an Algorithm > Page 29
Once Upon an Algorithm Page 29

by Martin Erwig


  Second, the type of an object tells us what algorithms we can use to transform it. For example, if we are given a list, we know that we can count the items in the list. If the items in the list can be compared, we know that we can also sort the list. An object can be levitated with the Wingardium Leviosa spell. Objects of a specific type can be transformed by any algorithm that has this type as an argument type.

  Third, if we have to compute something of a particular type, the result types of algorithms tell us which computations can in principle be used for this task. Together with the types of available arguments, the set of applicable algorithms can be narrowed down further. For example, to levitate an object, the Wingardium Leviosa spell seems to be the right choice. Objects of a desired type can be built only by an algorithm that has the same result type.

  The pervasive nature and use of types is due to their power to organize knowledge effectively. Types allow us to abstract from individual examples and reason about situations on a general level. For example, knowing that only a witch or a wizard can fly on a broomstick, we can infer that Harry Potter might be able to fly on a broomstick but his muggle aunt Petunia cannot. Or when Harry uses his invisibility cloak, he relies on its property that everything it covers is invisible. Numerous examples can be found in everyday, nonmagical life, as when we select a specific tool because of the general properties associated with it (screwdrivers, umbrellas, watches, blenders, etc.), or when we predict the outcomes of specific interactions (think of colliding objects, plugging-in an electrical gadget, or how people behave in different roles, such as, customer, patient, parent, and so on).

  Rules Rule

  In addition to supporting the efficient derivation of information about particular objects, types enable reasoning about the interaction of objects and thus provide a way to make predictions about the world. This can be achieved through a set of rules, called typing rules, that describe whether and how objects of different types can interact. For example, if something fragile drops onto a hard floor, it will likely break. In this case, the prediction can be derived from a rule that invokes several types: the types of fragile and of broken things, the type of accelerated movements, and the type of hard surfaces. The rule says that something belonging to the type of fragile things will likely belong to the type of broken things after it has experienced an accelerated movement against a hard surface. This general rule can be employed to make predictions in many different scenarios involving all kinds of fragile things (eggs, glasses, ice cream cones), hard surfaces (paved roads, brick walls, driveways), and accelerated movements (dropping, throwing). The rule compresses a large set of facts into one compact description. The compression is achieved by using types instead of individual names to represent the pertinent properties.

  A typing rule describes the type of an object under certain conditions. The conditions that must be fulfilled for a rule to be applicable are called its premises, and the statement about the type of an object that the rule derives from the premises is called its conclusion. The rule about the breaking of fragile objects has three premises, namely, that the object is fragile, that it is dropped, and that the surface it lands on is hard. The rule’s conclusion is that the object is broken. A typing rule that has only a conclusion but no premises is called an axiom to indicate that it is unconditionally true. Examples are “Harry Potter is a wizard,” “3 is a number,” or “thin glass is fragile.”

  The identification of types and the assignment of types to objects is a matter of design and is guided by particular situations and purposes. For example, the distinction between muggles and wizards is important in the context of the Harry Potter story but is not useful in contexts where magic does not exist. Most rules about objects in everyday life originally evolved to help us with survival in the natural world. They help us to avoid lethal mistakes. With new technology and culture, new rules are required to effectively navigate all areas of modern life like how to operate an elevator or a cell phone or how to sign up for and use health insurance. These examples demonstrate that the design of types and typing rules is an ongoing process driven by specific goals.

  The most important and fundamental typing rule for computation is the application rule. It relates the type of an algorithm to the type of the argument it is applied to and the type of the result it produces. The rule requires that an algorithm can be applied only to arguments whose type is identical to the algorithm’s input type. In that case, the type of the result delivered by the algorithm is the same as the algorithm’s output type. Typing rules are often shown by displaying the premises above a horizontal line and the conclusion beneath it. In this style, the rule for applying an algorithm to its arguments is as follows:

  The first premise of the rule requires an algorithm to have an input and output type. This requirement is closely related to Gamp’s Law of Elemental Transfiguration, presented in Harry Potter and the Deathly Hallows, which says that food cannot be created out of thin air; it can only be summoned from a different place or enlarged in size. The application rule reflects a fundamental property of algorithms, namely, that they depend on input to produce variable output.

  Only if all the premises of a rule are fulfilled can the conclusion of the rule be drawn. For example, an egg dropped onto a driveway will satisfy the rule about the breaking of fragile things, and thus the conclusion that the egg will be broken is warranted. Moreover, since 6 is a valid hour and 30 is a valid minute, and since the argument type of a wake-up algorithm is (Hour, Minute), we can apply this algorithm to the two arguments and conclude that the result is a valid behavior of type Alarm. An application of a typing rule is obtained by substituting a specific algorithm for Alg and argument(s) for Arg together with the corresponding types for Input and Output. The application of the algorithm typing rule to a wake-up algorithm looks as follows:

  Similarly, if L is a list of numbers, we can use the rule with the type List(Number) → List(Number) for Qsort to conclude that applying Qsort to L will produce a list of numbers:

  The ability to predict the outcome of situations from just the types of the involved objects is a powerful reasoning mechanism that causes rational people to use a spoon for eating soup or to undress before taking a shower. Types and typing rules provide us with a compact representation of similar objects and events that makes this process efficient. And this does not work just for reasoning about everyday situations but also in domains such as the magic world of Harry Potter or the world of computing.

  In the realm of Harry Potter the power of magic overrides many of the laws of the natural world. Therefore, wizards sometimes reason differently about everyday objects and act accordingly. For example, wizards can avoid much of the tedious work that muggles are forced to do, as when Ron Weasley’s mother uses magic to aid her with cooking and sweeping. For wizards it simply doesn’t make sense to do this by hand. Another example is driving in a regular car, which is shunned by the wizarding community because it isn’t economical compared to magical forms of transportation, such as teleportation, floo powder, portkeys, and, of course, flying.

  Types of algorithms predict outcomes of computations and can be used to reason about those as well. Suppose you are tasked with sorting a list and you don’t know how to do it. You are given three sealed envelopes A, B, and C that each contain a different algorithm. You don’t know which algorithm is contained in which envelope, but you know that one of them contains the sorting algorithm. As a hint, the type of each algorithm is written on the outside of each envelope. The envelopes show the following types:

  Envelope A: (Hour, Minute) → Alarm

  Envelope B: List(any) → Number

  Envelope C: List(comparable) → List(comparable

  Which envelope should you pick?

  When Rules Do Not Apply

  Types and typing rules provide a framework for reasoning that is very effective when applicable. But there are often situations when the rules don’t apply. Whenever one or more of the premises are not
satisfied, a rule is not applicable, which means that its conclusion is not valid. For example, a hammer being dropped onto a driveway doesn’t satisfy the premise regarding the fragile object, and a scenario in which an egg is dropped into a box of sawdust doesn’t satisfy the premise regarding the hard surface. Therefore, in either case the conclusion about the breaking of the object cannot be drawn. Similarly, when Ron Weasley tries to perform the Wingardium Leviosa spell to levitate a feather, the feather doesn’t move because his spell incantation is incorrect:

  “Wingardium Leviosa!” he [Ron] shouted, waving his long arms like a windmill. “You’re saying it wrong,” Harry heard Hermione snap. “It’s Wing-gardium Levi-o-sa, make the ‘gar’ nice and long.”

  Since one of the premises of the levitation spell is not fulfilled, the rule doesn’t apply, and its conclusion, the levitation of the feather, does not follow.

  Encountering a situation in which a typing rule is not applicable does not mean that the rule is wrong; it only means that it is limited in its scope and cannot be used to predict the behavior in the current situation. Moreover, when a rule is not applicable, it does not follow that the conclusion of that rule is definitely false. It could still be true because of other factors that are not covered by the rule. For example, the rule “If it’s raining, the driveway is wet” is not applicable when it’s sunny. However, the driveway could still be wet if the sprinklers were running. Or, to take an example from Harry Potter, even if Ron doesn’t perform the Wingardium Leviosa spell correctly, the feather could still start to levitate because somebody else could apply a spell to it simultaneously. Or the dropped hammer might still break when it hits the floor because its handle was already fractured to begin with. Therefore, when a rule is not applicable, no conclusion can be drawn either way.

  Thus it may not seem like such a big deal when typing rules don’t apply. However, that really depends on how important it is to ensure that a particular conclusion is true. While levitating feathers or the breaking of a dropped object are mere curiosities, there are many situations where the conclusion really matters. Think of all the “famous last word” jokes that play on incorrect conclusions, such as “The red wire is safe to cut,” “Nice doggy,” “These are the good kind of mushrooms,” and so on. For a computation, getting the types correct is similarly important. While seldom lethal, operating on a value of the wrong type will in most cases cause a computation to fail. Here is why. Each step of an algorithm transforms one or more values, and each operation that is applied in this process relies on its arguments to be of a particular type because it is only defined to do something meaningful for such values. Remember, we can’t sort a wake-up time, and we can’t compute the square root of a list. If any step of an algorithm encounters a value of a type that is not expected, it doesn’t know what to do with it and gets stuck. As a consequence, the computation cannot be completed successfully and cannot deliver a meaningful result. In short, the success of a computation depends on submitting only values of correct types to operations.

  Therefore, typing rules are a crucial component of computation because they can ensure that operations don’t get stuck on wrong values and that the computation as a whole can be completed successfully.3 Just as typing rules can be used to identify meaningless sentences, such as “Harry Potter drank a spell,” they can spot nonsensical applications of algorithms, such as Qsort(6:30am). And since an algorithm consists of many steps that involve the application of operations and other algorithms to values, typing rules can be used to identify mistakes within the definition of an algorithm, and they can actively support the construction of type-correct algorithms, a process sometimes called type-directed programming.

  Typing rules prevent not only impossible applications of operations to values that get stuck but also ones that don’t make sense in a certain context. For example, your height and age can be both expressed as numbers, but it doesn’t make sense to add these two numbers. The addition makes no sense in this case because the two numbers are representations of different things (see chapter 3), and thus the sum of the two numbers is not a representation of anything and therefore meaningless.4 We find examples in Harry Potter as well. For example, in the game of Quidditch two teams try to score goals by tossing a ball, the quaffle, into one of the opponent team’s goal posts. Now this would be rather easy using a teleportation spell, but that would make the game rather boring, and it would undermine the goal of the game, which is to determine the better Quidditch team. Therefore, employing magic other than flying a broomstick is not allowed for the players of the game. Such restrictions are ubiquitous in games. The requirement to follow suit in a card game or move a bishop in chess only diagonally does not reflect the impossibility of playing a different card or moving the bishop in a straight line; it is a restriction in a particular context in support of the goals of the game. Types can be used to track these representations alongside computations to ensure that operations respect the rules of combination for the represented values.

  A violation of a typing rule in an algorithm is called a type error. It indicates an inconsistency in the combination of operations and values. An algorithm that does not contain any type errors is said to be type correct. A type error in an algorithm can have different kinds of effects. First, it can cause the computation to get stuck, which in turn may lead to aborting the computation, potentially followed by reporting an error. The attempt to divide a number by zero typically has such an effect. In Harry Potter and the Chamber of Secrets, Ron’s wand breaks and causes all his spells to malfunction. For example, the Eat Slugs spell that he casts on Malfoy backfires, and his attempt to transform a rat into a goblet results in a furry cup with a tail. While the exact outcome might be a surprise, the lack of success in Ron’s magic was predictable, since his broken wand violates one of the premises of the typing rule for magic. In these cases, the effects of the nonworking magic are immediately visible. Second, a type error might not lead to any immediately noticeable effect, which means the computation continues and eventually finishes. But it does so with a meaningless value and thus ultimately produces an incorrect result. Adding the age and height of a person is such an example.

  While an abrupt interruption of a computation without a final result seems bad, a computation that continues but leads to a meaningless result can be much worse. The problem in that case is that one might not recognize that the result is incorrect and base an important decision on that wrong result. An example of this is when Harry Potter mispronounces “Diagon Alley” as “Diagonally” when attempting to travel by floo powder, which causes him to end up incorrectly in Knockturn Alley instead. The travel was not aborted, and the floo powder still worked, but it produced a wrong result. It would have been better for Harry if the trip had simply aborted, because he nearly gets kidnapped and has a run-in with some dark artifacts in the store he ends up in.

  Law Enforcement

  Since type correctness is an important prerequisite for the correct functioning of any algorithm, it is a good idea to check for type correctness automatically using an algorithm. Such an algorithm is called a type checker. A type checker determines whether the steps in an algorithm conform to the typing rules about control structures, variables, and values. A type checker can spot type errors in an algorithm and thus prevent erroneous computations.

  The types in an algorithm can be checked in two different ways. One possibility is to check the types during the execution of the algorithm. This approach is called dynamic type checking, since it happens while the dynamic behavior of an algorithm comes into effect. Right before an operation is performed, it is determined whether the types of the arguments match the typing requirements of the operation to be applied. A problem with this approach is that it is not really of any help in case a type error is detected. In most cases, the only possibility is to abort the computation, which can be quite frustrating, in particular, in cases when much of the intended computation has already happened and the algorithm aborts r
ight before the final result is obtained. It would be much better to know ahead of time whether the computation can be successfully completed without encountering a type error and not spend resources on a computation that is doomed to fail.

  The alternative approach inspects the algorithm without executing it and checks whether all steps respect the typing rules. The algorithm is then executed only if no type errors are found. In this case, one can be sure that the algorithm will not abort with a type error. This approach is called static type checking, since it happens without considering the dynamic behavior of executing an algorithm, and it requires only the static description of the algorithm. Static type checking would have told Ron not to try any magic with his broken wand.

  A further advantage of static type checking is that an algorithm needs to be checked only once. After that it can be executed repeatedly for different arguments without any more type checking. Moreover, while dynamic type checking has to check the operations in a loop repeatedly—in fact, as often as the loop is repeated—static type checking has to check any operation only once, which leads to faster execution of the algorithm. In contrast, dynamic type checking must be performed every time an algorithm is executed.

  However, dynamic type checking has the advantage that it is generally more precise, because it takes into account the values processed by the algorithm. Whereas static type checking only knows the types of parameters, dynamic type checking knows the concrete values. Static type checking would have prevented Ron from using his broken wand at all, and thus would have prevented any failures, while dynamic type checking lets him try out spells, and succeed and fail in different situations. For example, when Ron tries to transfigure a rat into a cup, he only partly succeeds: the cup still has a tail.

 

‹ Prev