Recently, Jim Newton reached out to me to clarify a post he submitted to ClojureVerse.

Jim is doing interesting work on defining heterogeneous types in Common Lisp, with a set-theoretic flavor. In ongoing followup work, he is generalizing his approach to to other languages and type systems, and he wants to learn more about Clojure and how it relates to Common Lisp, and how Typed Clojure and clojure.spec fit into the story.

I’m glad Jim reached out, since I had no idea Common Lisp included a formal definition of of a type with a subtyping algorithm that can return 3 answers (“yes”, “no”, “maybe”).

Jim asks:

1. What is a 'type' in Clojure?
2. Does the isa? function implement subtyping?
3. Is isa? decidable?

My response:

There are a few perspectives to answer this from, since:

1. Clojure has no official standard (unlike Common Lisp),
2. Typed Clojure is merely an unofficial optional type checker, and
3. spec is just a library.

Clojure’s perspective

Clojure has nothing as ambitious as SUBTYPEP, nor a rigorous definition of a “type”. There’s not much to see here, Clojure has no formal semantics or specification.

isa? is very simple and decidable. Here is the complete definition. The most “interesting” part is that it uses isAssignableFrom, which is also decidable.

(defn isa?
  "Returns true if (= child parent), or child is directly or indirectly derived from
  parent, either via a Java type inheritance relationship or a
  relationship established via derive. h must be a hierarchy obtained
  from make-hierarchy, if not supplied defaults to the global
  hierarchy"
  {:added "1.0"}
  ([child parent] (isa? global-hierarchy child parent))
  ([h child parent]
   (or (= child parent)
       (and (class? parent) (class? child)
            (. ^Class parent isAssignableFrom child))
       (contains? ((:ancestors h) child) parent)
       (and (class? child) (some #(contains? ((:ancestors h) %) parent) (supers child)))
       (and (vector? parent) (vector? child)
            (= (count parent) (count child))
            (loop [ret true i 0]
              (if (or (not ret) (= i (count parent)))
                ret
                (recur (isa? h (child i) (parent i)) (inc i))))))))

It turns out isa? is central to how Clojure multimethods work, so my ESOP16 paper goes into depth about how to model it in a type checker. But isa? is pretty much unrelated to subtyping a la SUBTYPEP.

clojure.spec’s perspective

clojure.spec implements runtime predicates and destructuring similar to the runtime portion of your ELS17 paper. It has the same regex operators for sequences, for example.

However I don’t know of any rigorous work of defining a subtyping algorithm between specs. Actually, I’m in the middle of thinking about how to do this, so it’s very convenient that you brought your ELS17 paper to my attention, since I was going to start looking at XDuce/CDuce for inspiration on how to deal with semantic subtyping with regex ops.

In summary, spec has no formal semantics, and is somewhat self-describing in some ways. eg., integer? is a spec/type that represents all values that passes the integer? predicate. If you’re looking for a more rigorous definition of spec, you might enjoy looking at my quals where I talk more about spec in Q2 and define a formal model of spec in Q3.

Typed Clojure’s perspective

Types in Typed Clojure are not set-theoretic (though that’s a future direction I’m working towards).

Subtyping is straight out of TAPL with equi-recursive types.

Local type variable inference is straight from LTI (Pierce & Turner) with extensions from Strickland et al.’s ESOP09.

I’ve played with a few extensions to interleave symbolic execution, but definitely not set-theoretic.

Thanks, Ambrose