4 ms·

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>

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-tools-for-a-language-documentat.html#sec-3-2 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.

vram22 8y ago
>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?
matt-noonan 8y ago
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 https://github.com/matt-noonan/justified-containers Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3.0.0/docs/Data-Map-Justified-Tutorial.html 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 http://kataskeue.com/gdp.pdf
- CMCDragonkai 8y ago
  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?
  - tome 8y ago
    I don't have a good answer but I did write something about this once http://h2.jaguarpaw.co.uk/posts/exists/ http://h2.jaguarpaw.co.uk/posts/exists/
  - matt-noonan 8y ago
    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-existentials/ 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.
tanin 8y ago
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.

vram22 8y ago

>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?

matt-noonan 8y ago

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 https://github.com/matt-noonan/justified-containers Or the tutorial module here: https://hackage.haskell.org/package/justified-containers-0.3.0.0/docs/Data-Map-Justified-Tutorial.html 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 http://kataskeue.com/gdp.pdf

CMCDragonkai 8y ago
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?
- tome 8y ago
  I don't have a good answer but I did write something about this once http://h2.jaguarpaw.co.uk/posts/exists/ http://h2.jaguarpaw.co.uk/posts/exists/
- matt-noonan 8y ago
  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-existentials/ 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.

tanin 8y ago

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.