Type-Theory Use Case: Validator Tree

Justin Dekeyser
Javarevisited
Published in
8 min readNov 18, 2021

In this short text, we explore how one could benefit from juggling with functional and type-theoretic thinking, to solve a concrete common problem found in programming. The language is Java (yet keep your Spring away), and the use case we focus on is the topic of validator trees.

A young tree — if ever it wasn’t obvious

The final result we target

Throughout the text, we are going to often refer to the following model example:

Our model example

Yes sir/m’dam, you got it right! It’s a schematic, over-simplified email address format validator.

Here are the desired outputs when we run this tree on different inputs:

Input: null reference
Error list: [
Input cannot be null
]
Input: hello
Error list: [
Input does not contain one @ symbol
]
Input: ju@
Error list: [
Local Length must be 3 chars long at least,
Domain cannot be blank
]
Input: @jude
Error list: [
Local cannot be blank,
Local Length must be 3 chars long at least
]
Input: @
Error list: [
Local cannot be blank,
Local Length must be 3 chars long at least,
Domain cannot be blank
]
Input: ju@de@keyser
Error list: [
Input contains too many @ symbols
]
Input: jude+123@keyser
Error list: [
Local cannot contain a '+' segment
]
Input: jude@keyser
Error list: []

Our goal is to implement this machine, with an approach driven by a kind of functional programming whose primary objects are types.

Implementation

The implementation we propose is based on functional programming, following a type-theoretic approach.

Referential transparency, pure functions, immutable data, … Forget about them in this reading. For once, we are going to shift our attention from those aspects to other ones: types, and how we compose them.

We are not going to introduce a lot of material, as we’d prefer things to stay intuitive and familiar. The reader can take as granted he knows enough if the following terminology does not make him panic:

  • Type definition: what does it mean to define a type (=:= operator)
  • Arrow operator: a way to create an arrow type A -> B from the given of two types A and B (function type)
  • Boolean pattern matching: just like pattern matching, but with boolean discriminant (so, in other words, if-then-else)
  • Product type: a way to create a product A x B from the given of two types A and B (think of it as a pair)
  • Plural monad: it’s a hand-made vocabulary to speak about “many things”, so actually: a list; we denote that by the suffix -s .

Introducing a functional Validator type

What do we really want from a Validator? Pretty straightforward: a way to map an input onto a list of failures:

Validator =:= Input -> Failure-s

How do we translate that in Java? Well, there could be many ways, but we’ve chosen this one, as we find it really convenient:

The Validator type, as an arrow Input -> Failure-s

It readily translates that we want to map an Input onto a plural form of Failure . We’ve chosen the built-in standard List interface, because it has an isEmpty method to quickly pattern-match on whether the list is empty or not (= do we have failures, or not?), and it has good interoperability with the Stream interface, which is the closest of the notion of monad in Java.

Sum of validators

We propose the following sum operation on validators of the same kind:

(Validator1 + Validator2)(ipt) = Validator1(ipt) + Validator2(ipt)

In other words, we enrich the validator type with a sum, compatible with the summation on the plural type. A natural choice of neutral element is the trivial validator, that validates everything:

neutralValidator = input -> emptyList

Java does not really have summation of lists, neither operator overloading. We therefore suggest the following static helper (we call it chain and not sum, because we think it may sound more intuitive):

Chaining validators with a sum-like approach

The neutral element is the result of chain() , or simply emptyList() .

Composition of validators

The mechanism behind a validator node that blocks validation or delegates on its children on success, is our notion of composition (“and then” wording). We implement it with an elementary boolean pattern matching:

(Validator1 # Validator2)(input) = if Validator1(input) is empty
then Validator2(input)
else Validator1(input)

We are not going to design a andThen method like the one of Function , because it’s not the approach we’ve chosen for the sum neither. We suggest the following variadic static operator instead:

The tree mapping, as a validator composition

Pull-back of validators

And finally the last mapping: a way to pull back a validator through an external mapping. Given a Output -> Failure-s together with a map Input -> Output, we can infer a new validator on the input by regular arrow composition (excuse my poor category theoretic diagram):

Input ----> Output ----> Failure-s
| |
\ - - - - - - - - - - - /

We have chosen to use the built-in Function type to encode the notion of “regular map”, taking advantage of method reference instantiation to easily bridge any kind of functional type.

Our suggestion is again based on a variadic static helper:

Pull-back of validators through a regular mapping

Composing is good, but we need a start

So far, we only sketched how to compose validators (summation, pull-back, and by a special tree converter).

The basic type, as a Input -> Failure-s is generic enough to fit any kind of implementation (method reference, a class, a singleton Spring component in case you have’t dropped Spring yet, …). It could also be nice to provide an easy way to create validators from predicates, as they’ll likely be a need for very basic, fundamental validations.

We thus seek for a converter

TEST : Failure x Predicate<Input> -> Validator<Input, Failure>TEST(failure, predicate) -> if predicate is true
then neutralElement
else of(failure)

The above exploits the two possible units on the List monad (where the empty is the unit on the empty list monad, which is also the neutral of the list monad; and of is the unit of non empty lists).

Yet again, the Java approach is really straightforward (just avoid to class, you don’t need it… really):

A test mapping to turn a predicate and the error, to a validator.

All together

The library code

Here is the entire library code we distilled through the article:

Full code, without the imports

I let it fit on 80 chars width max, just because I find it cool. Warning suppression is due to what the compiler calls “heap pollution”; in our case it’s fine.

The model example

And now the model example implementation:

Our model example (the same as above; we repeat for clarity)

We left it as an exercise to write down the complete model tree with the symbols and notations we introduced above.

Model example implementation

You can now reuse the Validator as you want: make it a static somewhere, compose it on-the-fly on another configurable validator, … whatever.

Take-away’s

Data-oriented programming?

Designing without classes in a language where everything is meant to be a class, is quite challenging. Recent Java versions allow some kind of lighter syntax: although the compiler interprets lambda expressions and method references as anonymous classes and instantiate objects accordingly, the look-and-feel is quite pleasant.

The key point here is: do not rush into data and classes. You don’t always need data.

As we’ve seen, the major part of the job was about function composition. The test factory method could be considered as the only “data holder” in this picture, and half of its own DNA is a Predicate .

Functional programming or Object-oriented programming?

Our approach has a bit of functional programming in its DNA.

The basic type we’ve chosen to work with, clearly is of functional nature. But we didn’t just use “pure static functions”. Instead, we first designed a type whose purpose is to create objects (likely by method reference or lambda expressions, but any other implementation can fit).

Designing with static methods wouldn’t bring so much flexibility in the way composition can be achieved (especially in Java where built-in methods cannot be passed as arguments): there is only one way to compose a method in Java, and it looks like an Assembly jump.

Having functional objects greatly improves composition features, and helps us deriving composition and summation features. (Those operators are static in our text, but could as well be encoded as Validator#add and Validator#andThen methods, respectively). Pull-back is an easy exercise, as composition is already available onFunction objects.

Type-oriented programming?

The approach we’ve followed here may be surprising.

It’s often the case in Java you’ll find wording shortcuts like “products are records” and “unions are sealed types/enums”. While those construct certainly reflect those notions partially, there are a lot more to say! We’ve shown here that method arguments can already be thought of as products. Overloading provides a way to speak about unions. And it’s perfectly enough here…

We gave up on the task of reflecting products, unions, pull-back, … inside the core Java’s type system. It’s not what one could call “a language meant to achieve this goal”. However, it doesn’t mean we threw away type-theory, on the contrary! We’ve shown you can use it, if not at a syntactic level, at least as a meta level.

We could have exposed the content of this article with standard OOP patterns like factory methods, decorators, … and that’s certainly another way to put things in perspective. The advantage of type theory is its algebra: on paper, when we thought about the patterns, we had an algebra ( x, |, ->, ... ) to guide us and help us. That’s where standard patterns cann’t rivalize: they essentially are unstructured, may it be in code, or on paper.

The take-away on type-theory we could give is: types can also be used as a pattern, and they rock at being! Enforcing record types and sealed types is, without contest, a powerful tool we shouldn’t throw away. But types can also be used differently, as patterns. In our opinion, this type-theoretic approach compensates what standard object-oriented patterns from the GoF lack of: an algebra to compose patterns easily.

Hope you enjoyed it :-)

All code is available in the gist: https://gist.github.com/Judekeyser/d2f316861deeeac8d861bcfb97816701

--

--

Justin Dekeyser
Javarevisited

PhD. in Mathematics, W3C huge fan and Java profound lover ❤