In Pascal these are called range types, e.g.
month: 1..12
would define an integer where the type system would ensure that it is always between 1 and 12.
Apart from Ada this seems to be an alien concept to all other languages. The concept of a "range type" also seems to have other meanings.
What is the Pascal "range type" properly called in type theory and what is its relationship to refinement types?
Subrange = range[0..5]
PositiveFloat = range[0.0..Inf]There's the concept of dependent types in e.g. Idris which lets us correctly do this sort of range check throughout the program (not just on literal assignment) but it comes with strict requirements on what the compiler can allow, such as no unbounded recursion, because checking dependent types is roughly equivalent to running the program.
If you mean to go all the way on units, dimensions and typing, there's a bestiary there, quited maintained (with several Ada 'takes' too) https://www.gmpreussner.com/research/dimensional-analysis-in...
How does Pascal handle overflow/underflow? E.g. Month 10 + Month 11 = Month 21?
$ cat a.pp
{$R+}
var
a: 1..12;
b: 1..12;
c: 1..12;
begin
a := 10;
b := 11;
c := a + b;
Writeln(c)
end.
$ fpc a.pp
Free Pascal Compiler version 3.2.2 [2021/05/19] for x86_64
Copyright (c) 1993-2021 by Florian Klaempfl and others
Target OS: Linux for x86-64
Compiling a.pp
Linking a
12 lines compiled, 0.1 sec
$ ./a
Runtime error 201 at $00000000004010D8
$00000000004010D8
$0000000000422EEC type
Month = enum Jan, Feb, Mar, Apr, May, ...
SpringMonth = range[Mar..May]
var m: SpringMonth = Mar
e.g. { x:Int8 | 1 ≤ x ≤ 12 }
Similarly, if you have tuples (or structs with anon fields etc) in the language, you could unify those with arrays such that struct { int; int; } is the same as int[2].