For example Ada's type system, which has equivalent of Common Lisp's SATISFIES construct, which implements a runtime type assert that can use all the power of the language.
>Most static type systems that can do what clojure.spec can do tend to include runtime assertion and type checks and do not erase type data from runtime (what some static type zealots call "uni-type" approach).
When you don't erase the type data... you're gonna have more than one type. How is this a "uni-type" approach?
Names in Clojure codebases and libraries are pretty reliably annotated with trailing exclamation marks, looking like: `save!`.
To that end, running Clojure code blindly to test it and its types is a fairly practical practice, coming up in cases like Ghostwheel [1], which uses this for generative testing of clojure.spec types, which can be much more sophisticated than what is commonly used in static systems, even with refinement types.
[1]: https://github.com/gnl/ghostwheel#staying-sane-with-function...
Can you elaborate on this? I have some experience with Clojure, and have been relatively unimpressed with spec. Everything it does I can do with (refinement) types (I think). Reading over the Spec documentation it constantly talks about predicates... which is exactly what a refinement type is.
Spec/Clojure has the problem where it validates... but doesn't parse. See: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...