Skip to content

Instantly share code, notes, and snippets.

@Azel4231
Last active May 11, 2020
Embed
What would you like to do?
Dependent types with clojure.spec (requires clojure-1.9alpha16+)
;; "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"]
(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)
(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] ?!
;; 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment