Hacker News Reader

Comment by tanin | Hacker News Reader

Is Spec simply a test? Or is it something more? I keep hearing about it, but it seems to be more than just a test case.

Let's take a simple example. I have an object with the method named "get". But I call "fetch" in my code. When will I see this error? During compile time or run time?

View on HN

Think of it this way: spec gives you an easy way to ensure that your data conforms to arbitrary predicate functions.

Suppose you have an XML format, <library> that has books and authors[1]. The elements look something like this: <book author-id="0000"/>, <author id="0000" name="Plath"/>. Obviously, you want to make sure that book's author-id attribute will always refer to an author that actually exists. This is something a (Java-style) static type system can't do: it doesn't know at compile-time what the contents of a variable will be. But spec can do this because it is a runtime check[2]: you'd just write a function that ensures all author-ids refer to extant authors and register it with spec, telling it that this must be true for valid <library>s.

As for your example, I don't think that is a use-case that spec was intended to handle. You could write a spec to ensure that an object has certain properties/methods, but I'm not spec would be too useful for a function invocation on that object.

[1]: For a worked out example of this in spec, see a blog post I wrote: https://lgessler.com/posts/2018-07-12-choosing-the-right-too...

[2]: It sounds expensive, but there's a compiler flag that lets you turn off all spec checks, so you can have them only run in dev builds if you like.

>Suppose you have an XML format, <library> that has books and authors[1]. The elements look something like this: <book author-id="0000"/>, <author id="0000" name="Plath"/>. Obviously, you want to make sure that book's author-id attribute will always refer to an author that actually exists. This is something a (Java-style) static type system can't do: it doesn't know at compile-time what the contents of a variable will be. But spec can do this because it is a runtime check[2]: you'd just write a function that ensures all author-ids refer to extant authors and register it with spec, telling it that this must be true for valid <library>s.

So is it similar to or different from assertions?

That blog post was a nice read, thanks!

I realize this is just one example, but you might be interested to know that I've done some work making this kind of invariant enforceable via static types (though in practice, you need a combination of features that aren't found in many mainstream language besides Haskell afaik).

See the README here for motivation and some examples (in Haskell, but hopefully the idea is still clear): https://github.com/matt-noonan/justified-containers

Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3...

Or this paper, if you really want to go off the deep end: http://kataskeue.com/gdp.pdf

I found your explanation of the relationship between an existentially quantified type and rank 2 polymorphism to be quite illuminating. Do you have any ideas why Haskell didnt have the direct way to express existential quantification in the type signature? Is it a technical limitation or something else?

I don't have a good answer but I did write something about this once http://h2.jaguarpaw.co.uk/posts/exists/

I'm not sure about the history. It looks like UHC supported existential types at some point, but I'm not sure how that would interact with what I am presuming is a more sophisticated system in GHC Haskell.

This post had some interesting tidbits about technical challenges, but I didn't fully grasp everything on first read: http://blog.ezyang.com/2016/04/hindley-milner-with-top-level...

I really like tome's observation in the other comment: universally-quantified types have a direct encoding in System F as type abstractions, but there is no such direct encoding for existentially-quantified types.

Thank you. I think I have a good idea what it is now. It's a constraint of a field. But it goes a bit further to ensures that, for example, an author id refers to a valid entity.

In Clojure unresolved names are a compile failure, and Spec would not be involved. Spec is just a nice library for writing runtime assertions about data. An example would be calling a third-party API and then validating the response with Spec to make sure it matches your expectations, or even validating the responses you are about to return from your own API. Similar to a type system the Spec can also serve as a sort of documentation about what's in the data structure.

You'd see it at run-time, but most likely at test-time. Which is not a "time" we often think about.

Spec is designed so that you setup automated generative tests on your specced functions. These perform brute force search of the input space.

So, they won't give you FOR ALL guarantees, but will still catch quite a lot. For functions with small input domains, it would actually prove FOR ALL.

The trade off is that, you can test for much more. You can test for properties of the values, not just type. Like say making sure that the output is always smaller than the input. Or that the input never is a blank or empty string.

A downside, it doesn't work well for unpure functions. Since the generative brute force doesn't have a way to brute force the side effect, or assert properties about it. For those, you'd need to write your own tests.

All in all, don't expect it to be at all like a static type checker. It's a very different beast, which you'll want to use very differently, and which offers a very different value proposition. For example, you could want to use Spec even if you had a static type system. Just like people still write tests. Spec is a new kind of tool that can be leveraged to mitigate software defects.

This is spec: https://clojure.org/about/spec

All spec errors turn up at run time. See the guide for more details: https://clojure.org/guides/spec.

You can combine spec with test.check (Clojure's quick check library) https://clojure.org/guides/spec#_generators

It's a way to describe the shape of data, a bit like schema but focus on non-exhaustive description and composability. The practical uses can be generative tests, is-a queries, conformity tests, "describe deviations from spec" queries, etc. You can also write spec for diffs in data structures, so you can use it for state changes. It's pretty open-ended.

At its core, spec lets you ask "Do I have what I need to do my job?", and if you have more, spec doesn't care. Type systems answer the question "Do I have exactly the machine primitives I expected, no less and no more".

It's about inspecting and verifying minimums at runtime.

Reply on news.ycombinator.com