5 ms·

> I think types should express intent. > If you write a lib that takes inputs that should never be negative you can express this without writing a single line o

> I think types should express intent. > If you write a lib that takes inputs that should never be negative you can express this without writing a single line of documentation So, let's make an odd_int_less_than_20587 type and a billion of other types? "Not negative" normally helps only one tiny bit towards documenting anything about the accepted values. Making a separate type for that and complicating everything is ridiculous. > If you write a lib that takes inputs that should never be negative Have you ever compared the difference between two unsigned integers? Because unsigned integers don't have "natural" subtraction. Did you ever find the need for signed numbers to interact with unsigned numbers? Because if you did, it's a bad idea to separate them without need. Premature isolation is a prime cause of complexity.

morelisp 5y ago
> So, let's make an odd_int_less_than_20587 type and a billion of other types? Bounded integer types have been extremely useful for me on a few occassions, and I wish more languages had type systems powerful enough to support them. They also address your concerns about subtraction.
virtualritz 5y ago
I think you assume my comments are regarding C/C++. They are not. I write mostly Rust these days.
- jstimpfle 5y ago
  I don't really care, why would Rust be much different in that regard?
jcelerier 5y ago
> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, what's wrong with that ? Every variable's type should be defined as precisely as possible when meaningful, that's the whole point (and C/C++ not easily allowing to do that is one of their biggest drawbacks imho.)
- cle 5y ago
  There's a tradeoff around strictness of nominal types and evolvability, e.g. changing the threshold on such a strict type would be a breaking change.
  - yakubin 5y ago
    Changing the threshold without signaling the change in the type system is also a breaking change. It's just that your compiler won't warn you about it when you inevitably forget to update your code. Instead your code is going to break at runtime.
    - cle 5y ago
      Not necessarily, it depends on what you do with the value.
    - jstimpfle 5y ago
      Obviously if you have at most 8/16/32/64 bit types (only making new types because of physical constraints), you'll have way, way fewer breaking changes than if you try to encode bounds extremely tightly and try to update them whenever you 2 instead of 1 somewhere. In fact most software is designed such that the physical sizes are chosen first, and then the practical bounds follow from that.
- jstimpfle 5y ago
  Are you seriously asking? Because what I suggested rhetorically would be the death of all your programs for the simple cause that line count would quadruple and you would have to touch half your codebase every time you make a tiny change.
  - jcelerier 5y ago
    When I make a change today like renaming a method I just let my IDE apply it to the codebase, why would that be different ?
masklinn 5y ago
> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yees? Bounded integers are a relatively common feature of programming languages (and one which is sorely missing from Rust, it's technically possible currently but not super fun, when fleshed out enough const generics should make them much nicer, possibly even built-in)
- jstimpfle 5y ago
  What is the point of bounded integers? Most quantities don't have natural bounds, and practical bounds only arise from physical limitations (8/16/32/64 bit etc).
  - atq2119 5y ago
    Those practical bounds have a tendency to percolate into bounding other things. So you can only have 2**10 foos because they're indexed by a 10-bit bitfield somewhere? Now maybe you can only have 204 bars, because every bar has at least 5 foos. And so on. If you genuinely wanted to reason solidly about such limits, you do end up needing arbitrarily bounded integers. Of course, most people don't want to do that, for good reasons. And even if you wanted it, there's a reasonable question whether adding them to the language syntax is really the right thing to do.
    - jstimpfle 5y ago
      Yup, that kinda was my point, and where you say "at least" that is also a good point why setting up some complicated static system to maintain limits is not practical. Hence my philosophy has been for a long time to set the physical constraints that just have to be decided (and do that as best as I can). And then to not worry (more than a tiny bit) about statically deciding the rest, or it'll end in a nightmare.
tel 5y ago
Not every type pays it’s way, but the distinction between N and Z is well worn and useful. N measures the size of things while Z is a little more abstract. I think u64 can quickly convey a powerful intent.
- jstimpfle 5y ago
  If we're talking about N and Z (which makes sense since most programs are grounded in a mathematical model with some physical constraints added on top), then please acknowledge that N doesn't have subtraction defined, which illustrates why it's not very useful for most code. You could also argue that subtraction for unsigned numbers is only partially defined, just like for signed numbers. But that would be missing the point, since most numbers in practical programs are small, and for these numbers the signed range is indeed much more useful since subtraction is defined for signed integers (e.g. i32) for small numbers. This is not the case for unsigned, where 3u-4u is usually not what you want.
  - tel 5y ago
    Even without subtraction defined, N is useful. Partial subtraction on N, as it is, is also useful. When I'm dealing with counts I pretty explicitly either want truncated subtraction or warnings when I overflow. Perhaps the biggest issue all together is just that many languages will let you do 3u - 4u instead of outright making the syntax more obviously annoying to force you to think about the caveats and pick between {truncated, throwing, overflow} variants.
jandrewrogers 5y ago
> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, and at least in C++ it isn't that difficult to trivially generate these types as you need them with a modicum of template-fu. You don't need that many integer type templates to capture most of the common cases and provide contextually sane operators. This might be a little more difficult in other languages. This is pretty standard type safety practice and usually well worth it in terms of writing robust low-defect code.
- jstimpfle 5y ago
  Show me where this is standard safety practice?
  - jandrewrogers 5y ago
    Eh, what? This has been idiomatic for many years for C++. Not doing it, especially today, is just malpractice. Every company I've worked at since I was doing C++ professionally required this. There is no accounting for how random companies do their software engineering but that doesn't mean competent software engineering organizations don't exist. I do database engines. This has been a standard part of code standards for a really long time, at least as long as the programming languages we used practically supported it. I've done it ever since. The only type that is allowed to flow through the code is size_t, where it makes sense.
    - jstimpfle 5y ago
      I'm really curious what that means and how it looks. I assume it's casually going beyond simple typedefs for types whose size might change? And what does "flow through the code" mean here? That you can't mention "int" or "uint64_t" anywhere? That you can't pass these things as arguments? Are there any open source examples to study this style? I don't know where to look, but admittedly studying C++ codebases is not what I do for fun. In my personal experience, it never worked putting layers of abstractions to hide physical representations. That makes the implementation code really hard to grok, and your hands are bound in the code because you're not allowed to _assume_. What worked for me instead is making sure that certain decisions that are likely to change are contained inside a module and for the rest of the code hidden behind an API or simply not accessible. Runtime assertions can be useful too, but maybe that is part of what you are describing by "template-foo". Finally, I try to stay true to my decisions and am not trying to act like I could have to replace floats by doubles at every corner. Some code that I've seen was littered with templates for that single reason, and I'm pretty sure the developers didn't have an intimate understanding how floating points works. Interestingly, size_t is one of the things that I tend to avoid, and in my perception a majority of the programmer population agrees it was a mistake to have it be an unsigned type. A type which can represent "the size of an object" is too general for all but maybe OS APIs IMO. Usually I know that the size of my objects is bounded by a certain size, well below what fits in 32 bits.
mamcx 5y ago
Totally! This is one of the best features of the pascal family: http://www.delphibasics.co.uk/Article.asp?Name=Sets http://www.delphibasics.co.uk/Article.asp?Name=Sets (look in "SubRanges")
- jstimpfle 5y ago
  Almost useless in my opinion (because not a lot of practical invariants can be expressed with simple ranges) and will only create confusion when using non-0, non-1 based indexing and also create confusion about the representation/the space required for representation. The examples shown there are similar to the Animal-Cat-Dog examples that are popular to "prove" that classes and inheritance are useful. That, plus the type incompatibility that arises from mixing such types with other integer types.
  - mamcx 5y ago
    Do you have uses Pascal? The ones that used it like it...
    - jstimpfle 5y ago
      I have worked on an enterprise application written in Delphi full-time for 6 months.
JD557 5y ago
> So, let's make an odd_int_less_than_20587 type and a billion of other types? I see your point, but I think that (while not always), it can still be pretty helpful to add your custom types to make invalid states unrepresentable. This can sound ridiculous on something like C, but if your language has refined types, it's not that bad. For example, this doesn't look awful to me: ``` type WeirdId = Int Refined (Odd And Less[20587]) val myId: WeirdId = 5 // OK val myInt: Int = myId // Can be used as an Int val myRuntimeId: Either[String, WeirdId] = refineV[Odd And Less[20587]](myId + 2) // Runtime Check val myInvalidId: WeirdId = 6 // Compilation Error ``` https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA
- jstimpfle 5y ago
  I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-level and code level, and I'm completely fine with sprinkling a few runtime assertions in most cases. Normal code syntax is much more suited to expressing invariants. Obviously I'm not into statically proving the correctness of my programs, so if that's your cup of tea things are probably looking different (and I'm sorry for you).
  - atq2119 5y ago
    I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.

morelisp 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Bounded integer types have been extremely useful for me on a few occassions, and I wish more languages had type systems powerful enough to support them. They also address your concerns about subtraction.

virtualritz 5y ago

I think you assume my comments are regarding C/C++. They are not. I write mostly Rust these days.

jstimpfle 5y ago
I don't really care, why would Rust be much different in that regard?

jcelerier 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, what's wrong with that ? Every variable's type should be defined as precisely as possible when meaningful, that's the whole point (and C/C++ not easily allowing to do that is one of their biggest drawbacks imho.)

cle 5y ago
There's a tradeoff around strictness of nominal types and evolvability, e.g. changing the threshold on such a strict type would be a breaking change.
- yakubin 5y ago
  Changing the threshold without signaling the change in the type system is also a breaking change. It's just that your compiler won't warn you about it when you inevitably forget to update your code. Instead your code is going to break at runtime.
  - cle 5y ago
    Not necessarily, it depends on what you do with the value.
  - jstimpfle 5y ago
    Obviously if you have at most 8/16/32/64 bit types (only making new types because of physical constraints), you'll have way, way fewer breaking changes than if you try to encode bounds extremely tightly and try to update them whenever you 2 instead of 1 somewhere. In fact most software is designed such that the physical sizes are chosen first, and then the practical bounds follow from that.
jstimpfle 5y ago
Are you seriously asking? Because what I suggested rhetorically would be the death of all your programs for the simple cause that line count would quadruple and you would have to touch half your codebase every time you make a tiny change.
- jcelerier 5y ago
  When I make a change today like renaming a method I just let my IDE apply it to the codebase, why would that be different ?

masklinn 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yees? Bounded integers are a relatively common feature of programming languages (and one which is sorely missing from Rust, it's technically possible currently but not super fun, when fleshed out enough const generics should make them much nicer, possibly even built-in)

jstimpfle 5y ago
What is the point of bounded integers? Most quantities don't have natural bounds, and practical bounds only arise from physical limitations (8/16/32/64 bit etc).
- atq2119 5y ago
  Those practical bounds have a tendency to percolate into bounding other things. So you can only have 2**10 foos because they're indexed by a 10-bit bitfield somewhere? Now maybe you can only have 204 bars, because every bar has at least 5 foos. And so on. If you genuinely wanted to reason solidly about such limits, you do end up needing arbitrarily bounded integers. Of course, most people don't want to do that, for good reasons. And even if you wanted it, there's a reasonable question whether adding them to the language syntax is really the right thing to do.
  - jstimpfle 5y ago
    Yup, that kinda was my point, and where you say "at least" that is also a good point why setting up some complicated static system to maintain limits is not practical. Hence my philosophy has been for a long time to set the physical constraints that just have to be decided (and do that as best as I can). And then to not worry (more than a tiny bit) about statically deciding the rest, or it'll end in a nightmare.

tel 5y ago

Not every type pays it’s way, but the distinction between N and Z is well worn and useful. N measures the size of things while Z is a little more abstract. I think u64 can quickly convey a powerful intent.

jstimpfle 5y ago
If we're talking about N and Z (which makes sense since most programs are grounded in a mathematical model with some physical constraints added on top), then please acknowledge that N doesn't have subtraction defined, which illustrates why it's not very useful for most code. You could also argue that subtraction for unsigned numbers is only partially defined, just like for signed numbers. But that would be missing the point, since most numbers in practical programs are small, and for these numbers the signed range is indeed much more useful since subtraction is defined for signed integers (e.g. i32) for small numbers. This is not the case for unsigned, where 3u-4u is usually not what you want.
- tel 5y ago
  Even without subtraction defined, N is useful. Partial subtraction on N, as it is, is also useful. When I'm dealing with counts I pretty explicitly either want truncated subtraction or warnings when I overflow. Perhaps the biggest issue all together is just that many languages will let you do 3u - 4u instead of outright making the syntax more obviously annoying to force you to think about the caveats and pick between {truncated, throwing, overflow} variants.

jandrewrogers 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? Yes, and at least in C++ it isn't that difficult to trivially generate these types as you need them with a modicum of template-fu. You don't need that many integer type templates to capture most of the common cases and provide contextually sane operators. This might be a little more difficult in other languages. This is pretty standard type safety practice and usually well worth it in terms of writing robust low-defect code.

jstimpfle 5y ago
Show me where this is standard safety practice?
- jandrewrogers 5y ago
  Eh, what? This has been idiomatic for many years for C++. Not doing it, especially today, is just malpractice. Every company I've worked at since I was doing C++ professionally required this. There is no accounting for how random companies do their software engineering but that doesn't mean competent software engineering organizations don't exist. I do database engines. This has been a standard part of code standards for a really long time, at least as long as the programming languages we used practically supported it. I've done it ever since. The only type that is allowed to flow through the code is size_t, where it makes sense.
  - jstimpfle 5y ago
    I'm really curious what that means and how it looks. I assume it's casually going beyond simple typedefs for types whose size might change? And what does "flow through the code" mean here? That you can't mention "int" or "uint64_t" anywhere? That you can't pass these things as arguments? Are there any open source examples to study this style? I don't know where to look, but admittedly studying C++ codebases is not what I do for fun. In my personal experience, it never worked putting layers of abstractions to hide physical representations. That makes the implementation code really hard to grok, and your hands are bound in the code because you're not allowed to _assume_. What worked for me instead is making sure that certain decisions that are likely to change are contained inside a module and for the rest of the code hidden behind an API or simply not accessible. Runtime assertions can be useful too, but maybe that is part of what you are describing by "template-foo". Finally, I try to stay true to my decisions and am not trying to act like I could have to replace floats by doubles at every corner. Some code that I've seen was littered with templates for that single reason, and I'm pretty sure the developers didn't have an intimate understanding how floating points works. Interestingly, size_t is one of the things that I tend to avoid, and in my perception a majority of the programmer population agrees it was a mistake to have it be an unsigned type. A type which can represent "the size of an object" is too general for all but maybe OS APIs IMO. Usually I know that the size of my objects is bounded by a certain size, well below what fits in 32 bits.

mamcx 5y ago

Totally! This is one of the best features of the pascal family: http://www.delphibasics.co.uk/Article.asp?Name=Sets http://www.delphibasics.co.uk/Article.asp?Name=Sets (look in "SubRanges")

jstimpfle 5y ago
Almost useless in my opinion (because not a lot of practical invariants can be expressed with simple ranges) and will only create confusion when using non-0, non-1 based indexing and also create confusion about the representation/the space required for representation. The examples shown there are similar to the Animal-Cat-Dog examples that are popular to "prove" that classes and inheritance are useful. That, plus the type incompatibility that arises from mixing such types with other integer types.
- mamcx 5y ago
  Do you have uses Pascal? The ones that used it like it...
  - jstimpfle 5y ago
    I have worked on an enterprise application written in Delphi full-time for 6 months.

JD557 5y ago

> So, let's make an odd_int_less_than_20587 type and a billion of other types? I see your point, but I think that (while not always), it can still be pretty helpful to add your custom types to make invalid states unrepresentable. This can sound ridiculous on something like C, but if your language has refined types, it's not that bad. For example, this doesn't look awful to me: ``` type WeirdId = Int Refined (Odd And Less[20587]) val myId: WeirdId = 5 // OK val myInt: Int = myId // Can be used as an Int val myRuntimeId: Either[String, WeirdId] = refineV[Odd And Less[20587]](myId + 2) // Runtime Check val myInvalidId: WeirdId = 6 // Compilation Error ``` https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA https://scastie.scala-lang.org/qoSHgL4PQCW6lC2MUHc5YA

jstimpfle 5y ago
I've spent some time pondering things like that, but ultimately concluded that we should keep these things away because there is a duplication between type-level and code level, and I'm completely fine with sprinkling a few runtime assertions in most cases. Normal code syntax is much more suited to expressing invariants. Obviously I'm not into statically proving the correctness of my programs, so if that's your cup of tea things are probably looking different (and I'm sorry for you).
- atq2119 5y ago
  I would love to be able to do more formal proving of programs in practice, but I 100% agree with you. A lot of what the advanced typing crowd seem to be doing is to re-invent programming but at the type level, and it's unclear to me why that should count as progress. It reminds me uncomfortably of C++ template metaprogramming -- and for good reasons, C++ has made steps towards replacing that with statically evaluated expressions written in regular syntax. My gut feeling is that the right way forward is to have a fairly standard type system visible in the source language augmented by contracts written in regular code. Basically a slight augmentation of assert(). A formal prover could internally reason about an extended type system where those contracts are automatically lifted to the type level if that helps for some reason, but programmers wouldn't be bothered with it. This seems unlikely to be a genuinely novel idea, so I'd be curious to hear whether systems like that already exist.