Example 3 – A Dynamic View of Type Safe Operations – Lift PlusOne
We have seen that Functor, Applicative and Monad encapsulate values. The type checker ensures that operations on those values execute according to progress and preservation rules to stop the program from going wrong. Both arguments and results must satisfy progress and preservation rules. Figure 5 uses a sequence diagram to illustrate how to lift the function PlusOne into Just using fmap. Lifting the function into Just means the rules applicable to Maybe and Just are now applicable to PlusOne. Following the hierarchy in Figure 2, Just is a data constructor of Maybe. Maybe is a Monad and Monad is a Functor.
Evaluation begins in step 1 by constructing the encapsulated value Zero in the Just monad. In the next step 2 evaluation proceeds by constructing an instance of the function PlusOne. Step 3 proceeds with the evaluation of fmap which takes the function PlusOne as an argument. Notice the result type of fmap is a function which takes a Functor into a Functor. Step 4 lifts the function justPlusOne into Just. It does not apply justOne to Just Zero. The type checker now enforces progress and preservation rules on the encapsulated PlusOne. Also notice the syntax in the yellow comment box below step 4. On the left side of the equality the type checker has determined the returned function has an input type of a Nat encapsulated in Just and a result type of a successor encapsulated in Just. It makes sense because PlusOne increments Zero to its successor Suc Zero. We know that value as the number One ! Nothing else is allowed by the type checker.
Figure 5 – A Dynamic View of Type Safe Operations – Lift Plus One
Example 4 – A Dynamic View of Type Safe Operations – Safe Apply with Applicative
We have encapsulated Zero in Just and lifted the function PlusOne into the Just monad. The result is a function called justPlusOne. The type checker requires it to take only a Nat encapsulated in Just and return its successor. Our goal is to safely apply justPlusOne to the encapsulated value Just Zero.
Figure 6 illustrates the type safe application of justPlusOne using Applicative. Evaluation proceeds in step 1 with a call to apply on justPlusOne, the function returned in Figure 5. In step 2 the call to yield with argument PlusOne constructs an instance of Just. Notice that the type checker enforces the result type to Monad in steps 1 & 2. The call to unit in step 3 encapsulates its argument PlusOne in Just. Recall that Applicative is the superclass of Monad. In step 4, as required from the inheritance hierarchy, the compiler invokes the Applicative constructor when it constructs an instance of Just. Step 4 returns an instance of Applicative with two parameters: a function of two parameters and a type variable. Evaluation proceeds in step 5 with a call to apply in Applicative. Its argument is the encapsulated PlusOne from step 3. Its result type is a parametrized function that takes an Applicative into an Applicative. Step 6 evaluates apply in Just with argument Just Zero. Notice that step 6 contains two calls to the function get in Applicative. It is in step 7 that applicative accesses the lifted function PlusOne and in step 8 the encapsulated value Zero. Step 9 is a call to unit in Applicative. Its argument is the function PlusOne with argument Zero. In step 10 evaluation continues on apply with argument Zero in PlusOne. Step 11 is a call to the class PlusOne’s add function and in step 12 the call to add creates an instance of the Suc constructor with argument Zero. In step 13 the stack unwinds with the result Just (Suc Zero). Notice that execution returns within Monad and with the reference justOne. Notice the syntax in the yellow comment just above step 13. To the left of the equals sign we see the type checker identifies justOne as a reference to the Maybe Monad with successors as input and successors as a result.
This section provided four examples of type safety in a technical architecture with UML Templates. The unabridged version of this article elaborates on the information in this section.
Figure 6 – Safe Apply with Applicative
We have come a long way on our journey to increasing assurance levels through early verification with type safety. The next section provides code samples that stop programs from going wrong at compile time rather than defer exceptions to run-time. Increasing assurance levels in a type safe architecture is most relevant when the architecture represents a run-time implementation.
Type Safety and Software Verification
Well typed programs don’t go wrong, but how do we stop them from going wrong? UML templates are artifacts in a technical architecture that represent computation. What about the computation itself?
This section illustrates how type checking at compile-time stops programs from going wrong. Programs don’t go wrong because the type checker stops the compiler. The type checker enforces verification early at compile-time rather than allow exceptions at run-time.
We proceed with an example that illustrates compile-time type checking. The unabridged version of this article provides an additional example in the Agda logical framework using stronger type checking with dependent types.
Example 1 builds on the UML approach above and illustrates type checking with Java Generics. Recall that Generics in Java is a synonym for Templates in UML. We expect more agency programs are familiar with Java, so it serves our needs for technology transition. For more on UML Templates and Java Generics see Generic Architecture for Government : A Modest Proposal for Better Safety and Sharing [GAGM 2014].
Java 1.5 introduced generic types to enable future versions of the language to provide type checking. Type checking evolved in subsequent releases and support for type safety strengthened recently with type inference. Example 1 describes how Java generics eliminate run-time exceptions resulting from incorrect casts. We begin with a review of the Linked List example from the Generic Java Tutorial [BOSW 1998].
Figure 7 – Raw Types
Figure 8 – Compiler and Run-time OutputÂ