Hacker News Reader

Comment by jstimpfle | Hacker News Reader

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

View on HN

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

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.

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.

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.

Not necessarily, it depends on what you do with the value.

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.

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 ?

Because if you change one type to include the number 235498 it will also affect 377 other types.

why would it ? if you set things such that expected ranges are set where they matter (e.g. where you do arithmetic) you should only have to change the types for which range issues occur, like this (very quick and dirty, likely wrong, but you get the idea): https://gcc.godbolt.org/z/4v6dW9czP

Not to hurt anyone's feelings but no I don't get the idea. I find this irritating and very unconvincing. So much work and boilerplate to prove peanuts. Have you ever seen anyone doing serious software development like that? I mean, not just toy examples of some 10-line bean counting program blown up to 100 lines.

> void foo(ranged_int<1, 5> a, ranged_int<3, 7> b)

Why would I _ever_ write a function like that? Practical proofs need to be about runtime values, not just constants and types. They also need to put multiple values in relation. They need to handle type casts and many more things. Constant integer ranges might be of some use but it's a tiny fraction of the invariants that a programmer juggles in practice, and the source code is already blown up out of proportion just for these ranges. This thing is just not gonna fly.

Just multiply some "good" values a few times and there is no way that you can statically prove that the result is going to be in the range as well, even though it might always be the case due to how the values combine each time (simple example: offset + size that the code checked to be within array bounds). Invariants in practice are relations over the runtime values of multiple variables. The focus on single values is basically already where types fail as a correctness tool.

> Just multiply some "good" values a few times and there is no way that you can statically prove that the result is going to be in the range as well, even though it might always be the case due to how the values combine each time (simple example: offset + size that the code checked to be within array bounds).

I don't understand, there's literally a CVE about that elsewhere in this thread, basically

    struct my_structure { 
      int size;
      int offset;
    };

either you restrict both size and offset to e.g. 2^30 so that you can safely sum both, or you will have an issue because you'll be doing if(size + offset < max_size) and size + offset overflows because absolutely no one can be trusted to write overflow checks, you gotta use a library for that.

If you're not making assumptions about the values stored in your variables, then every little arithmetic operation can lead to unexpected wraps (UB for signed types). What follows is that we need to make assumptions. Don't write an if conditional in front of every operation like a forgetful person - but assume that "my_structure" contains good values that you can safely add.

Usually it's very easy - require that size and offset are validly indexing an object, and require that objects are of a sane size (I rarely have in-memory objects larger than a few megabytes, and for most code I posit that it is a mistake to not chunk and stream huge datasets). Done, no real need to worry.

If you cannot make any assumptions about the values contained in a "my_structure" then that means the code is at an API boundary, which is the perfect place where such check (if-statement) must be placed. At internal code places, checks are wasted effort, and at most a compiler switch to detect wraps (logic errors) would often be a much better choice than paranoid code where each line of code can't trust the previous line, and where one can't see actual work being done because it's all covered in mistrust. Unnecessary mistrust (i.e. mistrust at places strictly inside maintenance boundaries which are not strategic checkpoints) only makes it hard to write code that actually does something, and might possibly cause more bugs than it could ever save.

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

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

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

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.

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.

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

Show me where this is standard safety practice?

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.

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.

> 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

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

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.

Exactly. It pains me when someone comes up with a new language with dependent types, but then to encode a simple constraint they first define integers via peano axioms using some kind of template metaprogramming. (The example I'm remembering was Coq or a Haskell dialect or something.)

There was a dialect of C#, Sing# or Spec#, that allowed you to specifying pre and post conditions in the same expression language as the main language, and they were checked at compile time. This is what comes closest I think.

Totally!

This is one of the best features of the pascal family:

http://www.delphibasics.co.uk/Article.asp?Name=Sets

(look in "SubRanges")

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.

Do you have uses Pascal?

The ones that used it like it...

I have worked on an enterprise application written in Delphi full-time for 6 months.

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.

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.

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.

I think you assume my comments are regarding C/C++.

They are not. I write mostly Rust these days.

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

Reply on news.ycombinator.com