Dependent types with clojure.spec (requires clojure-1.9alpha16+)

intro.clj

;; "Can you model dependent types in clojure.spec?"

;; What are dependent types?
;; -> Parts of the data depend on each other
;; -> The structure of the data depends on certain values in the data itself

   [3 "A" "B" "C"]
;; [count & elements]

;; Valid:
[3 "A" "B" "C"]
[1 "X"]
[0]

;; Invalid:
[5 "a"]
[1 "x" "y" "z"]

;; is this useful?
;; -> Yes, I think so
;; -> Checksum based data (ISBN, IBAN)
;; -> is this valid?    "ISBN 0-321-12521-5"   
;;                                        ^
;;                                     checksum (cross-sum mod 11)



;; Should be easy in spec, because it works at runtime!
[3 "A" "B" "C"]

naive-version.clj

(ns spec-depedent-types.naive
  (:require [clojure.spec.alpha :as s]))

(defn size-matches? [coll]
  (= (count coll)
     (inc (first coll))))

(s/def ::dependent-spec (s/and sequential?
                               #(integer? (first %))
                               size-matches?))

(s/valid? ::dependent-spec [5 1 2 3 4 5])
;; => true
(s/valid? ::dependent-spec [3 "a" "b" "c"])
;; => true
(s/conform ::dependent-spec [3 "a" "b" "c"])
;; => [3 "a" "b" "c"]

(s/valid? ::dependent-spec [4 "singleElement"])
;; => false
(s/explain ::dependent-spec [4 "singleElement"])
;; => val: [4 "singleElement"] fails spec: :spec-depedent-types.naive/dependent-spec predicate: size-matches?

(s/valid? ::dependent-spec [0])
;; => true


(defn do-something [coll]
  (when (not (s/valid? ::dependent-spec coll))
    (throw (RuntimeException.)))
  (let [size (first coll)
        [_ & elements] coll]
    (println "Size: " size ", elements: " elements)))

(do-something [3 "a" "b" "c"])
;; => Size:  3 , elements:  (a b c)

nice-version.clj

(ns spec-depedent-types.nice
  (:require [clojure.spec.alpha :as s]))

(defn size-matches? [m]
  (= (:count m)
     (count (:elements m))))

;; The naive version doesn't work, why?
#_(defn size-matches? [coll]
  (= (count coll)
     (inc (first coll))))

(s/def ::dependent-spec (s/and ::annotated-list
                               size-matches?))

(s/def ::annotated-list (s/cat :count nat-int?         ;; s/cat implies order
                               :elements (s/* any?)))

(s/conform ::dependent-spec [3 "a" "b" "c"])
;; => {:count 3, :elements ["a" "b" "c"]}





(s/valid? ::dependent-spec [5 "a" "b" "c" "d" "e"])
;; => true

(s/valid? ::dependent-spec [3 "a" "b" "c"])
;; => true

(s/valid? ::dependent-spec [4 "singleElement"])
;; => false

(s/explain ::dependent-spec [4 "singleElement"])
;; => val: {:count 4, :elements ["singleElement"]} fails spec: ::dependent-spec predicate: size-matches?

(s/valid? ::dependent-spec [0])
;; => true



(defn do-something [coll]
  (when (not (s/valid? ::dependent-spec coll))
    (throw (RuntimeException.)))
  (let [conformed (s/conform ::dependent-spec coll)]
    (str "Size: " (:count conformed) ", elements: " (:elements conformed))))

(do-something [3 "a" "b" "c"])
;; => Size:  3 , elements:  [a b c]


;; Bonus Question
;; -> what happens, when I decide to change the pattern to ["a" "b" "c" 3] ?!

outro.clj

;; Conclusion

;; -> dependent types useful for checksum-based data
;; -> s/and passes conformed data on to the successive specs
;; -> specs "encapsulate" knowledge about order
;; -> spec can model things that are impossible (or at least hard) to model in type systems