News for hackers. Stuff that matters.

A comment on What would it take to add refinement types to Rust?.

Re:What would it take to add refinement types to Rust? by weinzierl on Tuesday December 24, 2024 @05:11PM (#42505296)
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?

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by 3eb7988a1663 on Tuesday December 24, 2024 @06:17PM (#42505664)
Nim calls these subranges https://nim-lang.org/docs/manual.html#types-subrange-types

  Subrange = range[0..5]
  PositiveFloat = range[0.0..Inf]
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by frogulis on Tuesday December 24, 2024 @06:12PM (#42505639)
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.

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by bspammer on Tuesday December 24, 2024 @05:51PM (#42505521)
I frequently wish I had a natural number type. So many programs would benefit from the type system guaranteeing that numbers are never negative.
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by josephg on Tuesday December 24, 2024 @07:02PM (#42505878)
Rust has this one - though the ergonomics are a little awkward. Its called NonZero:

https://doc.rust-lang.org/std/num/type.NonZeroU32.html

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by frogulis on Tuesday December 24, 2024 @06:13PM (#42505649)
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.
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by archargelod on Tuesday December 24, 2024 @10:24PM (#42506625)
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.
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by munchler on Tuesday December 24, 2024 @05:22PM (#42505364)
> 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?

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by eddsolves on Wednesday December 25, 2024 @02:57AM (#42507584)
I assume modulo?
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by loeg on Wednesday December 25, 2024 @10:46AM (#42509319)
Uh, seemingly, yeah. 10+11 = 21. No bounds checking on addition or assignment.

https://onlinegdb.com/3KhhaReLV

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by int_19h on Wednesday December 25, 2024 @10:30PM (#42512948)
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".
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by dannymi on Thursday December 26, 2024 @12:11PM (#42516345) 

  $ 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
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by evertedsphere on Wednesday December 25, 2024 @02:52AM (#42507567)
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 }

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by riffraff on Wednesday December 25, 2024 @04:03AM (#42507792)
raku has "type subsets" which can do this (and more)

https://docs.raku.org/language/typesystem#subset

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by williamdclt on Wednesday December 25, 2024 @06:13AM (#42508216)
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
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by int_19h on Wednesday December 25, 2024 @10:18PM (#42512900)
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].

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by cpa on Wednesday December 25, 2024 @08:08AM (#42508613)
Haskell calls it Ord, for ordinal. https://en.m.wikipedia.org/wiki/Ordinal_data_type
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by DylanSp on Wednesday December 25, 2024 @09:46AM (#42509020)
Haskell's Ord typeclass is for ordering; it just represents types that have a total order, it doesn't represent ranges.
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by cpa on Wednesday December 25, 2024 @11:50AM (#42509672)
My bad the ordinal data type class is Enum not Ord!
[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by touisteur on Wednesday December 25, 2024 @11:58AM (#42509727)
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...

[ Parent | on HN ]
Re:What would it take to add refinement types to Rust? by amelius on Wednesday December 25, 2024 @03:48PM (#42511060)
In Pascal, how would you denote a type that can take all integers between 1 and 1000 except 123?
[ Parent | on HN ]