Hacker News Reader

Comment by geospeck | Hacker News Reader

> And doing things dynamically means we can enforce stronger constraints than possible with static type systems.

Can someone please explain this to a novice like me?

Taken literally the claim isn’t true - a Turing complete type system can enforce any constraint that a Turing complete programming language can. But your everyday type systems typically can’t express concepts like “a list of at least 3 elements” or “a number which is a power of 2”.

Pardon my ignorance, but can this spec thing automatically deduce that 8^n evaluates to "a number which is a power of 2" or log(2, "a number which is a power of 2") is an integer?

If yes, then I agree this is super helpful (and magical).

If not, how is this different from a normal constrcutor (with runtime input validation)?

No, it's not automatic like that. You define predicate functions that need to evaluate to true to pass. One of the reasons this is better than a normal constructor is these predicate functions are attached outside of the function they're describing. So they're inspectable and composable.

I think he's referring to the fact that you have more information at runtime (the actual request) than you do at compile time.

But your distinction about the theoretical limitations vs the practical capabilities of current type systems is also a good point.

Refinement types and Dependent types can do all of that. But you are right that mainstream languages ca’t do that today. Hopefully that will change.

The biggest manifestation of this is clojure spec:

https://clojure.org/about/spec

If your impression is that this is like sugary unit tests: It is not. You can run specs during development, while running a in-editor REPL, code gets evaluated while you type it so to speak.

It is way more expressive than a type system and it is opt-in, but it doesn't give the same guarantees obviously. It is also not meant to be a type system but rather a tool to express the shape of your data. It is used for obvious things like validation but also for documentation (over time) and generative testing among other things.

Most static time type systems can enforce that a voting age is an Integer, say, but can't validate that any value is at least 18, for example.

Turbo Pascal could.

In practice the only benefit is very similar to checked exceptions - can't forget to check that value is in range.

They can, this is a misconception. Create a new type, and make it so that it's only produced by a function that checks if the age is superior to 18.

That's a poor hack, it moves an invariant that could be enforced at compile time to not much more than a convention that has to be preserved by code review.

E.g. a colleague implements de-serialisation for your type but adds an empty constructor to make their life easier. You might not learn there's a hole in the boat before your first bug.

I wouldn't call it a poor hack. In a way it's a parser, which aren't really poor hacks, but can be abused. Sure, it's not perfect and I'd like it better if it was checked at compile time, but it's way better than using a simple int. Also, the moment you have a bug, tracking it is really easy: just list the functions that returns this specific type.

Yes, but this can be easily worked around by creating custom types that wrap the integer (and can be unwrapped on compile time) and some conversion functions. So slightly more tedious but saying one can't define complex constraints on static types is not quite correct.

This is not really true if you include ML languages. Most of the time you create a specific type for a type that is constrained. Ada has pretty good support for this and ML languages too. Once you have a specific type you make all your functions accept only VoterAge instead of Int.

I think this would work with every language that has nominal and not structural typing. If you have structural typing, you have to wrap the int. For example, this is "branding" in Typescript. I'm not sure if there is a performance penalty and how big it is though.

FSharp can easily do this.

You can have arbitrary types. Like a PrimeInteger type or a NameStartingWithD type or a complex hashmap with types defined for each key, like found in most configuration files.

IMO the sentence is incorrect. Static type systems would "enforce the stronger constraint" at run time... same as the dynamic type system. Perhaps the dynamic type system can have a fancy linter that does something crazy like running your code... but I'm not aware of any such linter.

> Perhaps the dynamic type system can have a fancy linter that does something crazy like running your code... but I'm not aware of any such linter.

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

>which can be much more sophisticated than what is commonly used in static systems, even with refinement types

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

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).

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.

Sorry, I don't understand

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

A popular (stupid) talking point in the stupid discussions about static/dynamic while missing that the axes were orthogonal, was for proponents of static types to claim that dynamic languages were "unityped" based on some convoluted logic about tagging data at runtime.

As someone who prefers static types, I agree with you that claiming dynamic languages are "unityped" is stupid. Javascript/Python/Clojure all literally have types.

Reply on news.ycombinator.com