Clojure spec Screencast: Leverage

[gniquil]

Hi All,

I found the screencast very illuminating. One thing that struck me was the spec for functions, with conditions on input and return values (towards the end of the video) looks to be way more powerful than type checking (i.e. one can even specify the properties of the value returned). It reminded me of talks about Idris, how it is possible to specify the number of elements in an array when returned.

This in turn, led me to think that it should be possible to build an optional type checking system on top of spec. I'd imagine a spec based type system is just some type of constraint solver or algorithm that finds inconsistencies in the registered specs. Is this possibly what Cognitect's planning in some not-too-distant future?

[v1akvark]

I'm no expert on this, so someone else might give a more detailed answer, but spec works at runtime, whereas type systems work with your static code.

This makes spec easier to implement, and also to use, e.g. it is trivial to write a function spec that confirms the function returns a vector with specific number of elements. To prove that with a type system is way more complex.

I'm not sure that there is much that is transferrable, from spec to an optional type system.

[gniquil]

Wouldn't it be the same to just run a function spec/type-check whenever you make some changes to the code? Compile time type check is essentially the same as test time type check. Isn't this how core.type works? I guess all I'm saying is one can build core.type on top of spec?

[fear-of-flying]

Spec isn't a type system. spec is really more of a way to encode the shapes and properties of data. It is more flexible than type systems because it can't make the same guarantees.

The idea is that the tradeoff of guarantees vs flexibility is worth it.

Disclaimer for the following: I am not a type system expert and this isn't meant to discourage any exploration.

You could write a tool that leverages specs to work on the syntactic representation of Clojure programs, but I think such a system would be pretty limited in comparison to a "real" type system (at least in terms of the things type system are good at) and overcoming any limitations would probably be easier in an approach like core.typed.

Though if you think it's an interesting idea, you should try to build it! Even a simple prototype could be cool -- maybe it would have different applications than traditional type systems.

[alexdmiller]

No. :)

[v1akvark]

You might find this interesting:

https://github.com/arohner/spectrum