This part is the 4^{th} in a series dedicated to learning the Clojure JVM language. Previous posts include:

While describing how to cope with dynamic typing, we used the spec library. The library is not a true replacement for types - checks are executed at runtime instead of compile-time. On the flip side, it can go further than mere types, including emulating dependent types and programming-by-contract.

## Dependent types

Let’s start by defining what is a dependent type:

In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.

https://en.wikipedia.org/wiki/Dependent_type

Let’s try to model the types mentioned in the above definition using spec.

Obviously, a "pair of integers" can be modeled as a collection of size 2 containing `int`

in a set order.

We will use an incremental approach:

- first model a collection of
`int`

- then, add a restriction on the size
- finally check for value ordering

Let’s start by modeling a collection of `int`

. The `coll-of`

function seen in the first post is a good match to specify such a collection.

Remember that its argument is a predicate applied to each element of the collection |

```
(s/def ::ints (s/coll-of int?))
(s/valid? ::ints [2 "2"]) ; false
(s/valid? ::ints ["4" "4"]) ; false
(s/valid? ::ints [3 5]) ; true
(s/valid? ::ints [2]) ; true
(s/valid? ::ints [2 2 2]) ; true
```

Now, let’s limit the number of elements to 2 to form a pair. The relevant code is quite straightforward, as the function `coll-of`

allows a `:count`

key to specify the required number of elements:

`(s/def ::pair-of-ints (s/coll-of int? :count 2)) `**(1)**
(s/valid? ::pair-of-ints [2 2]) ; true
(s/valid? ::pair-of-ints [4 4]) ; true
(s/valid? ::pair-of-ints [3 5]) ; true
(s/valid? ::pair-of-ints [2]) ; false
(s/valid? ::pair-of-ints [2 2 2]) ; false

1 | Any two `int` |

It’s time to add the final requirement: the second value must be greater than the first. This is clearly a dependent type, as it implies checking on values.

- This requires creating the predicate checking for that:
`(defn ordered? [pair] (> (last pair) (first pair)))`

- Then, we need to compose this custom predicate and the out-of-the-box
`coll-of`

one. This composition is made possible with the aptly-named boolean macros`and`

and`or`

.`(s/def ::dependent (s/and (s/coll-of int? :count 2)`

**(1)**ordered?)) (s/valid? ::dependent [2 2]) ; false (s/valid? ::dependent [3 4]) ; true (s/valid? ::dependent [2 1]) ; false (s/valid? ::dependent [1 2 3]) ; false

That’s it, we have defined a (runtime) dependent type. All building blocks are available to build more complex types.

This is not the end of all, though. Types - whether dependent or not, are not that useful by themselves.

What if we could combine them with functions?

## Contract-based programming

Only setting dependent types as in the above section is not very useful: it requires explicitly calling `(s/valid)`

on every variable, which is quite clumsy. There’s another option offered by Clojure, though.

I’ve already written about Programming by contract on the JVM (*a.k.a.* Contract-based programming) where I addressed Java and Kotlin. Clojure allows to call an indeterminate number of functions before and after executing a function’s body. This is achieved by defining a map with a specific to the desired function: `:pre`

and `:post`

respectively accepts an array of predicates to be executed before and after the function.

Combining those pre/post executions with spec achieves Contract-based programming.

Let’s create an `add`

function that adds two pairs like the above. The function should look something like:

```
(defn add
[p1, p2]
"Add two pairs"
(let [s1 (+ (first p1) (first p2))
s2 (+ (last p1) (last p2))]
[s1 s2]))
```

`p1`

and`p2`

have both to be validated by`::dependent`

. This translates into:`{:pre [(s/valid? ::dependent p1), (s/valid? ::dependent p2)]}`

- The returned value should also be validated with the same predicate, since if the first term of both is lower than the second, adding terms shouldn’t change that. To reference the value, use
`%`

:`{:post (s/valid? ::dependent %)}`

The final function is:

```
(defn add
[p1, p2]
{:pre [(s/valid? ::dependent p1),
(s/valid? ::dependent p2)]
:post (s/valid? ::dependent %)}
(let [s1 (+ (first p1) (first p2))
s2 (+ (last p1) (last p2))]
[s1 s2]))
```

And it can be called like:

```
(add [1 2] [3 4]) ; [4 6]
(add [2] [3 4]) ; AssertionError
(add ["1" 2] [3 4]) ; AssertionError
(add [1 2] 4) ; AssertionError
```

## Conclusion

In this post, we described how to go further than mere types, and put constraint on values with dependent types. Coupled with Programming by contract, this is a real help in making your code more reliable.

**To go further:**