[skybrian]

I think people do understand the basics of static type systems, but disagree about which types are essential in a "system language" (whatever that is).

An integer range is a very basic type, too, conceptually, but many languages don't support them in the type system. You get an unsigned int type if you're lucky.

[edflsafoiewq]

> An integer range is a very basic type, too

Not really, its semantics get hairy almost instantly. Eg does it incrementing it produce a new range?

[randomdata]

The semantics are always complex. The same type of question arises for all basic types. For example, what does adding a string to an integer produce?

Or do you give up on answering that and simply prevent adding strings and integers? When one wants to add them they can first manually apply an appropriate type conversion.

That is certainly a valid way to address your question – i.e. don't allow incrementing said type. Force converting it to a type that supports incrementing, and then from that the developer can, if they so choose, convert it back to an appropriate range type, including the original range type if suitable.

Of course, different languages will have different opinions about what is the "right" answer to these questions.

[noelwelsh]

I think you're confusing the type and value level.

The original statement was about a range type, that is something like an integer that is statically constrained to a range of, say, 1..4 (1, 2, 3, 4).

To work with this as a type you need to have type level operations, such as adding two ranges (which can yield a disjoint range!), adding elements to the range, and so on, which produce new types. These all have to work on types, not on values. If 1..4 + 5..8 = 1..8 this has to happen at the type level, or, in other words, at compile-time.

Range types are very complicated types, compared to the types most people deal with.

Converting a string to an int is very simple to type (String => Int if you ignore errors) and adding integers is also simple to type ((Int, Int) => Int)

[skybrian]

A range type could be very simple if it were just used for storage - you couldn’t do anything with it other than passing it around and converting it to something else, and there would be a runtime check when creating it.

But such a thing would be useful mostly for fields in data structures, and the runtime checks would add overhead. (Though, perhaps it would replace an array bounds check somewhere else?)

[foldr]

OP is just saying that you don't have to permit operations such as addition or incrementation on range types, in which case you don't need the corresponding type-level operations.

[noelwelsh]

> That is certainly a valid way to address your question – i.e. don't allow incrementing said type. Force converting it to a type that supports incrementing, and then from that the developer can, if they so choose, convert it back to an appropriate range type, including the original range type if suitable.

The quoted part above is an argument for dependent types. The conversion back to a range type creates a type that depends on a value, which is the essence of dependent typing.

[foldr]

No, I think the idea is that you'd get a runtime exception if the value was outside the range. No need for dependent types. It is no different conceptually from casting, say, a 64-bit integer to a 32-bit integer. If the value is outside the range for a 32-bit integer, then (depending on the language semantics) you either raise a runtime error, or the result is some kind of nonsense value. You do not need to introduce dependent types into your language to enable such casts (as long as you're willing to enforce the relevant checks only at runtime, or forego such checks altogether).

[dwattttt]

I regularly find quite smart people assume Rust's references must be fat pointers to handle lifetimes, and check them all at runtime.

[fooker]

> An integer range is a very basic type, too, conceptually

Just signed vs unsigned makes this a complex topic.