types.clj

;; I hope this example illustrates why I think the types that Clojure
;; programmers use are hard to represent with the type systems I've seen in
;; other languages. I have only a very superficial knowledge of type theory, so
;; I may well be mixing terms or even spouting complete nonsense. Apologies in
;; advance!

;; Idiomatic Clojure code tends to use very few custom types, and instead
;; represents most data as a composition of built-in types like maps, vectors,
;; and sets. For example, instead of a Person type you might use a map like the
;; following:

(def john {:first-name "John"
           :last-name "Doe"
           :age 33})

;; Note that this is not syntax for creating records. It's a map literal whose
;; keys and values could have any types, but we usually use :keywords for keys.
;; (If you're not familiar with keywords, you can think of them as a special
;; kind of string.)

;; Here's a function that operates on maps like the one above, and which I
;; think would be quite difficult to type in most languages' type systems.

(defn happy-birthday [x]
  (update-in x [:age] inc))

;; This is how it works with the value `john` from above:

(happy-birthday john)
;= {:first-name "John"
;   :last-name "Doe"
;   :age 34}

;; Let's see what types we could assign to the terms in that function.

;; `inc` is an easy one, that's [Number -> Number]. Any type system can handle
;; that.

;; `:age` is simple as well, it's a Keyword, and `[:age]` is a Vector.

;; But what type should we assign to `x`? The function's been initially written
;; for maps representing persons, but it works just as well with any map-like
;; value that contains a Number under the key `:age`. "Any Map whose value has
;; certain properties" sounds to me like we're venturing into the realm of
;; dependent types. On the other hand just typing it as (Map Any Any) would
;; leave out so much detail (and open the door to so many illegal values) that
;; it's not much better than assigning it the dreaded type Any.

;; `update-in` (see https://clojuredocs.org/clojure.core/update-in) is even
;; trickier. We could take the easy way and type it as
;; [Any (Seq Any) [Any -> Any] -> Any] but that's really just a longwinded way
;; of saying we can't type it at all. What we'd really want to capture is that
;; the keys passed in as the second parameter must be recursively found in the
;; nested associative structures passed in as the first parameter, and whatever
;; value we find under those keys, the function passed in as the third parameter
;; must be applicable to that value.

;; Finally `happy-birthday` should be a function from <whatever type we assign
;; to `x`> to the same type. If we apply it to a map representing a person (e.g.
;; `(happy-birthday john)`), the type system should know that the return value
;; will also be a map representing a person. Apply it to a bottle of
;; wine, get back a bottle wine (not Any!). This makes it even harder to assign
;; a return type to `update-in`. I suspect the type system should use
;; structural typing, or allow switching between structural and nominal typing,
;; to reconcile `update-in`'s model of "map-likes in, map-likes out" with
;; application code's model of "persons in, persons out".

;; If you're not familiar with Clojure, this example may make it seem like
;; `update-in` is a peculiarly thorny built-in function that could be handled
;; with a bit of special-casing in the type checker. On the contrary, I've
;; picked it precisely because there's nothing special about it. It's just a
;; regular Clojure function, and Clojure libraries are full of such
;; data-wrangling utilities. If a type system can't handle `update-in`, it can't
;; handle Clojure.