Today defense, intelligence and civilian agencies are focused on cyber security challenges. An informal analysis of emerging capabilities in the DARPA Open Catalog indicates that type safety is a common requirement for increased assurance levels in these agencies. Common requirements associated with emerging capabilities are especially relevant to planning and architecture. This article is an abridged version of a longer article that describes how to increase assurance levels with a type safe technical architecture.
Early Verification with a Type-Safe Technical Architecture
This section describes how programs already familiar with the Unified Modeling Language can represent type safety in a technical architecture.
It is claimed that type safety stops programs from going wrong. So how do we stop programs from going wrong in a technical architecture? We include a feature called templates in our UML artifacts to represent the rules enforced by the type checker. 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.
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 1 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 1 – Type Safe Construction of Natural Numbers Using Templates
This simple class diagram visually represents that the 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 used in a verifiable architecture milestone. 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 2 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 2 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 2 – 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 2, 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 3 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 3 – Applicative Elaboration
Figure 4 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 encawpsulation 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 4 – Monad and Maybe Type Elaboration
Figure 4 also elaborates the Maybe class. In its elided state in Figure 3 Maybe had little resemblance to Nat. In Figure 4 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.