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.
This is the 5th post in the Learning Clojure focus series.Other posts include:
- Decoding Clojure code, getting your feet wet
- Learning Clojure: coping with dynamic typing
- Learning Clojure: the arrow and doto macros
- Learning Clojure: dynamic dispatch
- Learning Clojure: dependent types and contract-based programming (this post)
- Learning Clojure: comparing with Java streams
- Feedback on Learning Clojure: comparing with Java streams
- Learning Clojure: transducers
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]) ; trueNow, 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-ofone. This composition is made possible with the aptly-named boolean macrosandandor.(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]))p1andp2have 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) ; AssertionErrorConclusion
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.