6 ms·

> And doing things dynamically means we can enforce stronger constraints than possible with static type systems. Can someone please explain this to a novice li

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

elmers-glue 5y ago
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.
- ajuc 5y ago
  Turbo Pascal could. In practice the only benefit is very similar to checked exceptions - can't forget to check that value is in range.
- Zababa 5y ago
  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.
  - CraigJPerry 5y ago
    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.
    - Zababa 5y ago
      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.
- LeonidasXIV 5y ago
  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.
- StreamBright 5y ago
  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.
  - Zababa 5y ago
    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.
- nojito 5y ago
  FSharp can easily do this.
jahewson 5y ago
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”.
- SCLeo 5y ago
  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)?
  - travisjungroth 5y ago
    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.
- jwhitlark 5y ago
  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.
- mbrodersen 5y ago
  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.
dgb23 5y ago
The biggest manifestation of this is clojure spec: https://clojure.org/about/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.
dharmaturtle 5y ago
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.
- tekacs 5y ago
  > 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-specs-and-generative-testing https://github.com/gnl/ghostwheel#staying-sane-with-function...
  - dharmaturtle 5y ago
    >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-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
- p_l 5y ago
  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.
divs1210 5y ago
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.

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

elmers-glue 5y ago

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.

ajuc 5y ago
Turbo Pascal could. In practice the only benefit is very similar to checked exceptions - can't forget to check that value is in range.
Zababa 5y ago
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.
- CraigJPerry 5y ago
  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.
  - Zababa 5y ago
    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.
LeonidasXIV 5y ago
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.
StreamBright 5y ago
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.
- Zababa 5y ago
  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.
nojito 5y ago
FSharp can easily do this.

jahewson 5y ago

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

SCLeo 5y ago
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)?
- travisjungroth 5y ago
  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.
jwhitlark 5y ago
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.
mbrodersen 5y ago
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.

dgb23 5y ago

The biggest manifestation of this is clojure spec: https://clojure.org/about/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.

dharmaturtle 5y ago

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.

tekacs 5y ago
> 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-specs-and-generative-testing https://github.com/gnl/ghostwheel#staying-sane-with-function...
- dharmaturtle 5y ago
  >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-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
p_l 5y ago
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.

divs1210 5y ago

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.