I recently learned of dependent type systems. I’m trying to feel out the boundaries of dependent types and came to the question: Is Clojure Spec a dependent type system?
Dependent types are the back-bone of various theorem proving languages like Idris, Coq, and F*.
Dependent type systems allow types to depend on values. This allows types to be manipulated like other kinds of values. For example, an list wouldn’t need a special language feature to be generic. The type contained by the list could be a value that is set. Setting that value, say to int, would be the equivalent of creating a generic type list<int>. I’m still grappling with it and not the most reliable source. You can see a trustier example here.
My grappling raised the question “Is Clojure Spec a dependent type system?”
Spec doesn’t call itself such. It’s origin is the Specification Pattern.
On one hand, Clojure types are defined by the presence of values that meet certain criteria. By Clojure’s set semantics, the values are the type. At least one person seems to agree with this stance.
On the other hand, I’m not certain that specs are first-class values. This means they can be passed and operated on. I know specs references can be passed around. They must also be analyzable in order to support features like data generation. I’m not sure you can really pass a value to a spec type and have different variations of a single type based on those values. Specs also must be registered in a global registry (via s/def). Specs don’t presently provide compile-time verification either.
If Spec is dependent type system, then perhaps it too can benefit from theorem proving over automated random testing. Perhaps type-driven approaches in static languages could also use theorem proving for correctness, totality, and other provable properties when given the right conventions for finding value constraints.
This is all pretty new for me. Certainly a lot to think about.