Early Verification with Type-Safe Technical Architecture
This section describes how programs already familiar with the Unified Modeling Language can represent type safety in a technical architecture.
So how do we stop programs from going wrong? We include a feature called templates in our UML artifacts to represent the rules enforced by the type checker. Recall the type checker enforces progress and preservation rules. UML Superstructure, Auxiliary Constructs (17) describes templates as “A parameterable element is an element that can be exposed as a formal template parameter for a template, or specified as an actual parameter in a binding of a template.” Templates allow for parametric polymorphism in UML artifacts. Parametric polymorphism is a feature of type systems that enforce type safety. Templates are known alternatively as generics in mainstream programming languages like C++, Java, C# and Scala. By including templates in the artifacts of our architecture, we represent the rules verified by the type checker. Type safety is enforced early in the Executable Architecture milestone of the Elaboration phase of the Early Evolutionary life cycle.
We continue with four examples of how to represent type safety with UML templates. Examples 1 & 2 provide a static view of type safe structure. Example 1 describes the type safe construction of natural numbers. Example 2 provides an overview of key functional programming abstractions. Examples 3 & 4 provide a dynamic view of type safe operations. Example 3 explains type safe operations required to lift a function into the Maybe Monad. Example 4 explains the safe application of the lifted function to a value. Recall that our purpose is to demonstrate how to represent type safety.
Example 1 – Type Safe Construction of Natural Numbers Using Templates
Figure 4 is a UML Class diagram with Templates. Nat, representing the natural numbers, is an abstract UML class. Because Class extends Classifier, Nat, like Class, is a templateable, or parametrized, element. The additional box outlined in dashed in the top-right corner of Nat class is the template. Nat is parametrized by A, a type parameter. TA is its formal parameter bound to the class A representing the type variable A. The right arrow (>) represents the binding. The sub classes Zero and Suc are data type constructors as indicated by their stereotypes. The data type constructors are also parametrized. Notice that Zero has a private, no-arg constructor restricting access so its parameter will never be used as required by the progress and preservation rules. Zero is also static and final further restricting its use. Suc takes values of type Nat as a parameter in its single arg constructor allowing recursive construction of countably infinite values. Suc too is static and final.
Figure 4. Type Safe Construction of Natural Numbers Using Templates
This simple class diagram visually represents that type checker enforces type safety in the construction of natural numbers at compile time. Enforcing type safety at compile time stops the program from going wrong. A UML architect would be expected to provide the verification rules. The code snippets at the bottom of the diagram illustrate the syntax of two type safe languages: Haskell and Java. The section below on type safety and software verification explains compile-time constraints in source code.
Example 2 – Overview of Functional Programming Abstractions
Figure 5 expands on our first example of type safety with an overview of functional programming abstractions. Type safety is a recurring theme in functional languages. Representing functional abstractions in UML introduces type safety to a broader audience in support technology transition. More defense, intelligence and civilian programs will be familiar with UML than the commutative diagrams of category theory. Reading Figure 5 from top left to bottom right we again see the natural numbers. Nat, Zero and Suc are elided to save space. To the right we see that Nat implements Functor. Functor is an abstraction through which it operates on its own elements using fmap, its only operation. Functor has two parameters A and B. Fmap takes a function, operates on values of its type and returns a function that lifts the values into the type of the Functor. Lifting a value into the type of Functor encapsulates the value in the type. Operations on the lifted value must now satisfy the progress and preservation properties of the Functor. Notice that the function type of fmap is also parametrized with similar binding syntax. The UML syntax of the annotation “[]” to the Function return type is incomplete because the UML modeling tool did not provide adequate type checking or type inference.
Also notice that Functor is a functional interface as reflected in its stereotype. Stereotypes can be combined into UML Profiles that are useful in extending the semantics of UML. We do not discuss profiles further in this article.
Below Functor is Function. Representing Function as a UML interface is consistent with the evolution of mainstream programming languages like Java. What were once object oriented languages now incorporate functional capabilities to strengthen type safety in the language. It too is a functional interface with two parameters A and B. Classes that implement Function must implement its only operation, apply, which takes a single argument that is a type parameter A and returns a single argument type parameter B. PlusOne and PureJust implement Function. They are also parametrized. PlusOne implements a new operation, add, which takes arguments of type Nat and returns results of type Suc. Apply is elided on PlusOne in the diagram to save space.
Figure 5. Overview of Functional Programming Abstractions
To the right of Function both above and below appear the classes Applicative and Monad. Applicative and Monad are parametrized, but the attributes and operations of Applicative and Monad are elided in Figure 5, we elaborate each in detail below. Applicative encapsulates a value and allows the sequencing of computations to combine their results. Monad allows for control in sequencing the effect of a computation.
Figure 6 illustrates the Applicative class with Templates. Applicative has two: A and B bound to TA and TB respectively. Applicative and Monad are equipped with functions that operate on values of the parametrized type. The intuition behind Applicative and Monad are that their operations happen inside the type and that the type system protects the values inside the box. Applicative comes equipped with get, unit and apply. Unit puts a value inside the box. Apply takes an applicative and returns a function that takes an Applicative into Applicative. A function that takes a function into a function is called higher order. It is this function that allows the sequencing of operations. Example 4 below describes the sequencing of operations with Applicative.
Figure 6 – Applicative Elaboration
Figure 7 elaborates the Monad class. Like Applicative, Monad has two parameters A and B bound to TA and TB respectively. Monad comes equipped with the following operations: return, bind, yield, join, fail, fmap and map. Return takes a value and encapsulates it in the monad. Bind takes an encapsulated value and a function that operates on the encapsulated value and returns the result of the function on the value. Join takes an encapsulated value and reduces the encapsulation by one level. Yield returns an encapsulated value. Fail takes string explaining the error into the monad. Monad also includes operations inherited from Functor and Applicative.
Figure 7 – Monad and Maybe Type Elaboration
Figure 7 also elaborates the Maybe class. In its elided state in Figure 6 Maybe had little resemblance to Nat. In Figure 7 we see that it is an abstract parametrized class with two final subclasses. We also see that Maybe is a Monad. It provides an abstract parametrized method, instance, that returns Maybe. The instance method is inherited by its sub classes, Nothing and Just. Nothing is static and final and an inner class. It is a singleton with an instance method inherited from Maybe. Just is final, but not static, nor is it an inner class. It has single, private constructor. Just overrides instance with the single input parameter that is a type variable and it returns Just [].
Now that we have a static view of the functional abstractions with attributes and operations of each class and interface we provide a dynamic view of their type safe operations using sequence diagrams.
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 8 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 5, 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 8 – A Dynamic View of Type Safe Operations – Lift PlusOne
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 9 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 8. 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.
Figure 9 – Safe Apply with Applicative
This section provided four examples of type safety in a technical architecture with UML Templates. We now understand how artifacts specified in the Elaboration phase of the Early Evolutionary life cycle increase assurance levels. The UML artifacts in the four examples above are the result of the Type Safe Design and Interactive Proving disciplines executed by architects and engineers in the Amplification and Synthesis iterations resulting in the Executable Architecture milestone.
We have come a long way on our journey to increasing assurance levels through early verification with type safety. This next section provides code samples from the Construction phase of how we stop programs from going wrong. Although later in the life cycle than architecture, during development, type safety and verification remain relevant because the type checker stops the compiler rather than defer exceptions to run-time.