5 ms·

I find the idea of being able to specify numerical types with arbitrary ranges very appealing. In Pascal these are called range types, e.g. month: 1..12 woul

I find the idea of being able to specify numerical types with arbitrary ranges very appealing. 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?

munchler 2y ago
> an integer where the type system would ensure that it is always between 1 and 12 How does Pascal handle overflow/underflow? E.g. Month 10 + Month 11 = Month 21?
- eddsolves 2y ago
  I assume modulo?
- loeg 2y ago
  Uh, seemingly, yeah. 10+11 = 21. No bounds checking on addition or assignment. https://onlinegdb.com/3KhhaReLV https://onlinegdb.com/3KhhaReLV
  - int_19h 2y ago
    That is just this one particular implementation of Pascal (unsure which one). The language spec does say that it is an error to assign a value out of range, but as far as what this actually means, it only says that "a complying processor is required to provide documentation concerning its treatment of errors".
  - dannymi 2y ago
    $ 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
bspammer 2y ago
I frequently wish I had a natural number type. So many programs would benefit from the type system guaranteeing that numbers are never negative.
- frogulis 2y ago
  Easy enough to write in some languages... as long as you only need to support addition and multiplication, or a very limited set of numbers.
- josephg 2y ago
  Rust has this one - though the ergonomics are a little awkward. Its called NonZero: https://doc.rust-lang.org/std/num/type.NonZeroU32.html https://doc.rust-lang.org/std/num/type.NonZeroU32.html
- archargelod 2y ago
  Nim has Natural and Positive (signed int) types that checked at compile and runtime. You can also define arbitrary range types for any ordinal type, for example enums: type Month = enum Jan, Feb, Mar, Apr, May, ... SpringMonth = range[Mar..May] var m: SpringMonth = Mar It will raise under/overflow exception if value falls out of range.
frogulis 2y ago
Anybody correct me if I'm wrong -- in Pascal these subranges can specify the size of the variable in memory and check compile-type assignment to a literal value, but don't (can't) do much else. 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.
3eb7988a1663 2y ago
Nim calls these subranges https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types Subrange = range[0..5] PositiveFloat = range[0.0..Inf]
evertedsphere 2y ago
it is a refinement type over the base number type, where the predicate constrains the number to lie in an interval e.g. { x:Int8 | 1 ≤ x ≤ 12 }
riffraff 2y ago
raku has "type subsets" which can do this (and more) https://docs.raku.org/language/typesystem#subset https://docs.raku.org/language/typesystem#subset
williamdclt 2y ago
I’ve seen “month” being implemented in typescript as a big sum type ‘1 | 2 | 3 | … | 12’ :) probably ranges could just be syntactical sugar on top of that, but I suppose it probably causes big inefficiencies for the compiler
- int_19h 2y ago
  It can be syntactic sugar in terms of how it's defined, but the implementation can still be smart and use a compact representation where possible (this is basically RLE). 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].
cpa 2y ago
Haskell calls it Ord, for ordinal. https://en.m.wikipedia.org/wiki/Ordinal_data_type https://en.m.wikipedia.org/wiki/Ordinal_data_type
- DylanSp 2y ago
  Haskell's Ord typeclass is for ordering; it just represents types that have a total order, it doesn't represent ranges.
  - cpa 2y ago
    My bad the ordinal data type class is Enum not Ord!
touisteur 2y ago
Ranges are awfully useful in Ada, but a very small help in dimensionality/units analyis. 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-programming-languages#ada https://www.gmpreussner.com/research/dimensional-analysis-in...
amelius 2y ago
In Pascal, how would you denote a type that can take all integers between 1 and 1000 except 123?

munchler 2y ago

> an integer where the type system would ensure that it is always between 1 and 12 How does Pascal handle overflow/underflow? E.g. Month 10 + Month 11 = Month 21?

eddsolves 2y ago
I assume modulo?
loeg 2y ago
Uh, seemingly, yeah. 10+11 = 21. No bounds checking on addition or assignment. https://onlinegdb.com/3KhhaReLV https://onlinegdb.com/3KhhaReLV
- int_19h 2y ago
  That is just this one particular implementation of Pascal (unsure which one). The language spec does say that it is an error to assign a value out of range, but as far as what this actually means, it only says that "a complying processor is required to provide documentation concerning its treatment of errors".
- dannymi 2y ago
  $ 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

bspammer 2y ago

I frequently wish I had a natural number type. So many programs would benefit from the type system guaranteeing that numbers are never negative.

frogulis 2y ago
Easy enough to write in some languages... as long as you only need to support addition and multiplication, or a very limited set of numbers.
josephg 2y ago
Rust has this one - though the ergonomics are a little awkward. Its called NonZero: https://doc.rust-lang.org/std/num/type.NonZeroU32.html https://doc.rust-lang.org/std/num/type.NonZeroU32.html
archargelod 2y ago
Nim has Natural and Positive (signed int) types that checked at compile and runtime. You can also define arbitrary range types for any ordinal type, for example enums: type Month = enum Jan, Feb, Mar, Apr, May, ... SpringMonth = range[Mar..May] var m: SpringMonth = Mar It will raise under/overflow exception if value falls out of range.

frogulis 2y ago

Anybody correct me if I'm wrong -- in Pascal these subranges can specify the size of the variable in memory and check compile-type assignment to a literal value, but don't (can't) do much else. 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.

3eb7988a1663 2y ago

Nim calls these subranges https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types Subrange = range[0..5] PositiveFloat = range[0.0..Inf]

evertedsphere 2y ago

it is a refinement type over the base number type, where the predicate constrains the number to lie in an interval e.g. { x:Int8 | 1 ≤ x ≤ 12 }

riffraff 2y ago

raku has "type subsets" which can do this (and more) https://docs.raku.org/language/typesystem#subset https://docs.raku.org/language/typesystem#subset

williamdclt 2y ago

I’ve seen “month” being implemented in typescript as a big sum type ‘1 | 2 | 3 | … | 12’ :) probably ranges could just be syntactical sugar on top of that, but I suppose it probably causes big inefficiencies for the compiler

int_19h 2y ago
It can be syntactic sugar in terms of how it's defined, but the implementation can still be smart and use a compact representation where possible (this is basically RLE). 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].

cpa 2y ago

Haskell calls it Ord, for ordinal. https://en.m.wikipedia.org/wiki/Ordinal_data_type https://en.m.wikipedia.org/wiki/Ordinal_data_type

DylanSp 2y ago
Haskell's Ord typeclass is for ordering; it just represents types that have a total order, it doesn't represent ranges.
- cpa 2y ago
  My bad the ordinal data type class is Enum not Ord!

touisteur 2y ago

Ranges are awfully useful in Ada, but a very small help in dimensionality/units analyis. 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-programming-languages#ada https://www.gmpreussner.com/research/dimensional-analysis-in...

amelius 2y ago

In Pascal, how would you denote a type that can take all integers between 1 and 1000 except 123?