Domain Modeling For Better Contracts

In the post about communicating contracts through enforcing endpoint contracts, we took a look at some basic types which are available in Signet. Today we are going to talk about how to add more information to your types by creating your own data types.

Last week we took a look at how to build types as sets with characteristic functions. This week we will apply that information in order to add extra information to our types.

By this point I’m certain there are plenty of people who are thinking I’ve gone completely off the rails. Javascript, after all, is a dynamically typed language. Don’t burden yourself with all of this type stuff and just write some code!

Although this is true, most people view types as a constraint which only causes pain. Though this might be true if you are coming from a language like Java which contains lots of artificial constraints around type creation, and after all is said and done, the types are still weak and restrictive.

On the other hand, if we consider types as a way to add a layer of correctness checking and a tool for communicating with others, types become less a restriction and more a tool we can use to make our programs better. Good types will make a program transparent and predictable. These are traits we definitely want in our programs.

Just as a refresher, let’s have a look at where we left off with our purchase API from the enforcing endpoints blog post. This way we have a common position to understand where we started and where we’re going.

Now that we have our API defined with regard to basic types, we can start to ask more meaningful questions. Instead of asking things like “what does this function do,” we can ask directed questions to inform our programming better: What kind of numbers are they? What is in the array? What kind of argument must the function take?

The last two questions are easiest to answer since we don’t have to look any farther than higher-kinded types. This is, of course, scary sounding the first time you hear it. I had no clue what a higher-kinded type was the first time I heard the word. Fortunately, many of you may already be familiar with them even if you don’t know the word. Java and C# both support higher-kinded types.

Higher-Kinded Types and You

First and foremost, let’s discuss what a higher-kinded type actually is. (It’s a type.) Once we have a better grasp on that, we will use it in code to make everything a little more clear.

A higher-kinded type is simply a type which takes a type as an argument and returns a type. I know, that sounds weird. How does a number take a string and return a type? I asked the same thing.

It turns out, however, that it’s not nearly as foreign as it might seem. One very common type we rarely think about in Javascript which could easily be handled as a higher-kinded type is an array. An array is, itself, a type, but it contains values which are also typed. This means, if we had a language to express it, we could declare an array which contains only a single type.

As it turns out, there are potentially infinite different types which are, or could be, higher-kinded. In this post we are going to look at just two: array and function. With the type signature language available with signet, we can explicitly declare an array type as needed. This means we can do things like the following.

We can see both of the tested arrays are completely valid Javascript arrays, but the second is not an array of exclusively numbers. There are ways we could create an array which would support numbers and strings, but that’s beyond the scope of this post.

Just like we can declare information about arrays, we can also say something about the expectations around a function. Instead of simply saying a value is “function,” we can actually say a value is a “function which takes a number.” In much the same way we declare our types in arrays, our function type declaration is “function.”

Now that we have an expanded type language to draw upon, let’s update our API and clarify the communication of our domain model.

Subtyping With Characteristics

Now we just have the ‘number’ type scattered everywhere throughout our code. Although this is better than nothing, it would be SO MUCH better if we actually knew something about those numbers. What do they mean? How are they used? What are the constraints?

It turns out we have just the thing to remedy this pain, it’s called characteristic functions. As we know from our earlier discussions on characteristics, we can add richness to our type system through set-describing predicate functions. (Protip: all predicates describe sets)

Before we dive into creating new types willy-nilly, let’s take a moment to account for the different number types we have. By properly identifying the actual domain language we care about, we can create better types which will allow us to clearly describe our application to people who might know nothing about it.

Ultimately, we care about tax, price, amount of tax to pay (tax amount) and purchase total. If we were to simplify this list a bit, we can identify a couple of distinct bits of information.

First let’s consider tax. Tax is a percentage amount. Since, where I live, taxes are always greater than or equal to 0%, but always less than 100%, I am going to say tax is a percent value which will always fall between 0 and 1. For example, in San Diego, sales tax is currently around 8% or 0.08.

Now, we can take a look at price, tax amount and purchase total. Each of these is a value which is related to a value an amount our customer will be paying. This means we can roll these all into some aspect of price. We will say a price value will be greater than or equal to 0. This describes our data pretty accurately for the moment, so let’s go with that.

With our base types sorted out in a way we can jump off from, we can start building characteristics. By clearly defining our characteristics, we give our new types programmatic meaning. Let’s see what our basic characteristic functions will look like for price and percent.

The other piece of this puzzle is, we need to register our types with Signet. Fortunately, this is a simple process. We know that each of these types is actually a number, so we can simply use the subtype function and declare these two functions as new types, inheriting from number. This is also why we didn’t need to test each value to see if it is a number, our subtyping will guarantee we only verify numbers.

We can use our price type to create our other two types by simply aliasing them and using the price definition to ensure our data constraints are clear.

Let’s have a look at our updated API and see how our types are coming along!

Duck Typing our Object

At this point, our API is pretty clear, but there is still one last type which just doesn’t quite convey the information we want to know. Our array of purchases is still described, simply, as an array of objects. This could be much better, if only there were a way to check it.

As it turns out, the Go language has popularized the notion of object similarity through duck typing and that is precisely what we are going to do here. If we know enough information, we can tell whether our object satisfies the Liskov substitution principle, and can be used in place of our intended object.

Signet provides a means to perform duck typing as well, so we don’t have to build our characteristic function from the ground up every time, because that could end up being a LOT of repeated code. Let’s build a duck typing characteristic and finish up our API types.

Now we have a name for our purchase object type, which means we can easily check whether our array of purchases actually adheres to our expectations. Plus this will provide a way for others to understand what we intended when we wrote the code, making it much easier to write new code against the existing API.

Wrapping Things Up

Although this just scratches the surface of using types in your program, hopefully this exercise helps you communicate intent and define a clear domain model. By taking core types we already know and applying a small amount of predicate logic, we surface a new way to talk about our program and the data we use.

Instead of simply using old code as a reference for what it does, add a little annotation, a little bit of logic and get a lot more bang for your buck. In the end, types don’t make everything correct all the time, but they do a lot to make you and others like you a lot more awesome!

Comments Off on Domain Modeling For Better Contracts

Types, Sets and Characteristics

A couple weeks ago, we looked at using Signet and some of the core types to add type information to function calls. Although it is handy to have a variety of base types available to provide signatures for your functions, sometimes you want more control and finer-grained behavior.

At the most foundational level, applied types can be viewed as sets of values. This means, for any type, we can easily construct a set which will describe that type. For instance, the type ‘string’ can be written as the set of all values which are strings. Although this may seem like a trivial way to perform a conversion of a type to a set, it gives us a way to start rethinking the way we interact with type information.

Sets as Types

We can, somewhat informally, say that sets are types. Although this doesn’t capture the nuance of types, it allows us to capture a lot of power in a simple idea. We looked at defining the string type as a set of values. What this really means is, strings are a certain set of values within all values assignable.

If we begin our sets by considering all values assignable and available in within Javascript, we can refer to that set as our “universe.” Within that universe, we could choose a variety of different sets, but regardless of which set we choose, the new set will be contained completely within the original universe.

Using this universal definition, we can consider our strings again and consider how we might describe our set of all strings. First of all, we can ask if a value is contained within our universe. A good example of a value which is distinctly NOT in the Javascript universe is 1000! (1000 factorial). Although this is an integer which actually exists, Javascript will simply evaluate it as infinity. This is not something we will need to test for, it is simply the indication of an upper bound in Javascript.

We could, however, define a set of numbers we declare as our domain set. We can call this an explicit set definition. By turns, we can define a set by way of excluding items which are not in the set. This inverse set can, equally, be declared explicitly, or we can define a function which will simply tell us whether something is in the set or not. This implicit method of creating a set can be referred to as an induced set.

Let’s take a look at a meaningful question we could ask. Let’s ask if a value is a number. This means we are going to call a function which accepts type of * and returns a boolean. This kind of function is called a characteristic function.

Although this function, by itself, is not a big step away from what we already know, it lays the groundwork for defining a richer set of types we can interact with. From the function isNumber, we get an induced set of all values which are numbers, rather than defining the type set explicitly.

Propositions and Predicates

It has been shown in the academic community that propositions are types. What this means is we can actually consider propositions such as A and B in the expression A ∨ B as types unto themselves.

Any proposition can either resolve to a theorem (⊤) or an antitheorem (⊥) which roughly equates to the idea of true or false. In other words, we can ask a question and the answer will either be “yes” or “no.” Although this seems non-obvious, at its face, this is the foundation we will use to construct a richer set of types within Javascript.

We have already seen type construction where we use a predicate to manage inclusion in a type set. We are stating that a value α must be in the set of numbers if α is a number. Even stronger than that, we can say, since our set contains ONLY values which are numbers that if α is in the set of numbers it has a type of number. This relationship between sets and type implementations is important for capturing greater amounts of information about a value as we construct subsets from sets we have defined. Let’s have a look at the logical notation to see predicates in action, so we can tie that together with our predicate notation.

Njs = the set of all values which are Javascript numbers
A: α is a Javascript number
B: α ∈ Njs;

A → B
B → A

Of course in our implementation we really only worry about the second relation, i.e. that if a value is in the set of values which conform to the number type, the value must also conform to the number type. Given the definition of B, α ∈ Njs;, we can actually conclude that the first relation is true given the definition of Njs.

We can actually reformulate this to express the type-set relation more generally. If we simply replace our specific number set with a set of any type Τ we get a new, very useful formulation we can use to extend our type reach well beyond the specifics of the language.

Τjs = the set of all values expressible in Javascript of type τ
A: ατ is a Javascript value of type τ
B: ατ ∈ Τjs

A → B
B → A

That’s a lot of symbols, words and relations. What this really means is we can identify and define any arbitrary type logically and, in turn, define a set containing all values of that type, which will induce an “if and only if” (iff) relationship. That’s a lot of words and symbols. Let’s take a look at how we might use this to implement our own type.

Defining a New Javascript Type

Clearly we won’t be able to build our type into the core language without getting on TC39, issuing a new standard and waiting for several years while everyone adopts it, but we can induce our type through a new predicate function. Let’s suppose we want to define a new type, Integer. We could express our type in the following way:

Intjs = the set of all values expressible in Javascript of type number which are integers
αint ∈ Intjs

With this, we can define a function expressing this relationship, which we can use to verify whether a value is in our set Intjs or not. With regard to the relation between types, expressible values in Javascript and our integer set, we can guarantee the stability of our type and the correctness of our verification.

Although this function is sufficient for verifying whether a value is an integer, we are actually duplicating our efforts. Moreover, it lacks a certain expressiveness which we might like to see. Let’s use our original isNumber function to say a little more about the meaning of our int type.

This new function performs the same check as the original, but it reflects a deeper relationship between our number set, Njs, and our integer set, Intjs. In other words, what we can see expressed here is the typical inheritance property of the is-a relationship.

The Is-A Relationship of Types

As is true for objects in classical object oriented programming, types can also have an inheritance relationship where one type is a subtype of another. This is what we mean by is-a relationship. We can say an integer is a number, or a name is a string. Although an integer can be a type in its own right, we know the number type is the foundation type in Javascript for any numeric representation. This means, for any function which requires a number, an integer is an acceptable value.

Our isInt function demonstrates the is-a relationship by using the number set definition as the first requirement of our check for set inclusion. Let’s continue the chain and create a characteristic function to defining our natural number. Our natural number set will be a strict subset of our integer set.

Now we can see that a natural number is an integer which is a number. This, of course, is similar to OO subtyping with regard to relationship, but is compositional in nature. In fact we can actually describe this type relationship as a relationship of sets, like so:

Naturaljs ⊂ Intjs ⊂ Numberjs

With the repeated behavior of including a function call from the superset, we can start looking for a way to uniformly describe our sets and their relationships. Let’s create a new function, subtype, to help us create set relationships in order to streamline the process of defining type relationships.

Subtype allows us to define our types with functional composition and define our new characteristics with the assumption that we are already working from within a specific type. Let’s rewrite our isNatural check using subtype.

Now the body of our characteristic function is expressed with an implicit relation to the superset of natural numbers, integers. This kind of higher-order function use to express set relations is extremely powerful for defining and describing value types we can use in our development.

Wrapping Up

This was a somewhat dense tour of how we can construct types in Javascript, so don’t worry if it takes a little while to pull the pieces together. The important take-away is that we can construct our own types with meaningful names and clear relationships in order to better understand the way our programs work.

At the end of the day, we are human, so expecting us to actively deal in generalized abstractions such as strings and numbers may not be a reasonable request. Instead, we can reclaim the reins and define our own type language which speaks to future developers in the language of our intent. Go make types and make your programs better!

Comments Off on Types, Sets and Characteristics