7 ms·
What would it take to add refinement types to Rust?
- sieabahlpark 2y ago[dead]
- pwdisswordfishz 2y ago[flagged]
- sagacity 2y agoIt's unfortunate that this is the only takeaway of the article for you.
- loeg 2y agoThe author didn't mention this, but maybe there could be a type (unit) canonicalization step that always produces the same reduced/simplified type for any equivalent set of Mul/Divs? So that you don't need the later equivalency check. E.g. with the article's example, where 'a' is Meters and 'b' is Seconds, 'a/(b*b)' and 'a/b/b' both have type 'Div<Meters, Mul<Seconds, Seconds>>' instead of one having the type 'Div<Div<Meters, Seconds>, Seconds>'. For only Muls and Divs you can basically just have a histogram of units to powers (e.g., m/s^2 => m: 1, s: -2) which uniquely represent equivalent types.
- hinkley 2y agoJames Gosling looked at this and wrote about it at the time. It can be a bit mind bending. Especially with units named after people. If you’re looking at statistics for current or power the type system might try to convert it to joules even though you wanted to look at average wattage.
- loeg 2y agoYeah, but equivalent units with different names is sort of only a display/formatting issue, right?
- weinzierl 2y agoThis is a matter of perspective. For example the unit Sievert is an official SI unit despite being just J/kg. This is because confusing equivalent dose and absorbed dose, which also has the unit of J/kg, could be very dangerous. Note, that this is different from J sometimes being written as Ws. While there are informal conventions, when we use J and when Ws, using the unconventional one would not be technically wrong because 1 J is simply 1 Ws, whereas 1 Sv is not necessarily 1 J/kg when the later is an absorbed dose. I think one could reasonably disagree with these decisions but that is how the SI people see it.
- dwattttt 2y ago> This is a matter of perspective. I'd make a stronger statement here; this is a specific example of when having units is most powerful. When even though two things are expressed in some common form, they nevertheless represent something different. > Yeah, but equivalent units with different names is sort of only a display/formatting issue, right? This could be said of two u32s as well.
- pests 2y ago> When even though two things are expressed in some common form, they nevertheless represent something different. This is where people go wrong trying to DRY and other refactors. Slightly forced example but function averagePerClassroom(total) { return total / 30; } // 30 kids per class function averagePerMonth(total) { return total / 30; } // assume 30 "Oh, the function body is the same therefore lets refactor this into an "averagePer" function" expect its two completely different concepts and once the code calculates the actual days per month or once classes are no longer 30 people suddenly things need to be un-refactored, or what I see more often, is just branching off inside the new single function based on an argument flag. Horrible.
- jph 2y agoType refinements are a great concept and I'd love to see them in Rust. And double-refinement types are great for helping with conversions, such as with Rust From/Into, and potentially a dynamic converter function. Examples of double-refinements that I'd like: - Common units like Length:Meter and Length:Foot. - Color bits like Color:RGB24 and Color:CYMK24. - Worldwide currency like Money:USD and Money:GBP with a converter function that knows exchange rates. - Human languages like String:English vs String:Cymraeg with a converter function that knows translations.
- spockz 2y agoThe currency converter is the odd one out because it context dependent. (Time, contract, etc)
- 0xFF0123 2y agoSimilar to time with a timezone?
- skissane 2y ago> - Worldwide currency like Money:USD and Money:GBP with a converter function that knows exchange rates. Exchange rates vary over time, so you'd arguably need a type which includes a timestamp (e.g. "USD 1000 at 2024-12-25"). And that's ignoring all these other complexities such as the spread, different currency converters offering differing rates, unofficial and multiple official rates in countries with currency controls (e.g. Argentina), hedging, etc
- jaza 2y agoPlus, perhaps the biggest complexity of all is that the currency rates are often not free, particularly if you want "live pricing" (updated every few seconds), and particularly if it's for commercial use. And, the fact that they may or may not be free, also illustrates well the fact that there are no definitive rates, there are only "rates according to X".
- magicalhippo 2y ago
- nmilo 2y agoIt should be easier now with const generics, I know the popular C++ library looks like Value<Unit, T, L, M, ...> where the letters are numbers representing the dimension of time, length, mass, etc. So m/s^2 would always be Value<f64, -2, 1, 0, ...>. By keeping it normalized you don't need Equivalent or whatever
- deleted 2y ago[deleted]
- marxisttemp 2y agoCould someone clarify to me the different between dependent types and refinement types?
- dietr1ch 2y agoRefinements embed a predicate that elements of the new type must pass. def Nat = Int: (|x| -> x >= 0) Dependent types allow types to be computed from functions (and depend on arguments, otherwise it seems they become just weird constants), def Five(as_type: String) -> NumericType(as_type): match as_type: "string" => "five" "int" => 5 "float" => 5.0f "double" => 5.0d _ => panic() // Unnecessary if you refine `as_type` from a String to an enum or a fixed set of strings. Dependent types seem weird, but they help making types first-class (https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s https://www.youtube.com/watch?v=mOtKD7ml0NU&t=325s) and gaining types like `Array<T, N>` that allow ensuring things are the right length, and define append/extend properly.
- xigoi 2y agoJust curious, what language is this?
- dietr1ch 2y agoI made up the syntax to try to keep it easy to read for people using python/rust/c. I just realized my lambda syntax on the Nat predicate is redundant because I didn't clean up and that using snake_case for function names would be better in a language that lets you operate on functions like they are values.
- tubthumper8 2y agoWhat happens when the predicate returns false for the refinement type? Like if `(Nat 5) - (Nat 6)`. Or is subtraction disallowed?
- klibertp 2y ago
- Waterluvian 2y agoIf I understand this properly, I’ve needed this in typescript a lot. I can make `type uuid = string` for self documentation, but a lot of plugins will just label it “string” and developers can (and have) mistakenly put some other identifier, like the robot’s hostname. Of course we validate at the API but it’d be more skookum if we could prevent accidental wiring together of front-end components that make this error. String literals help a ton. Gosh they’re wonderful to care about the shape of a string in the type system. But sometimes I really want to say “strict uuid” as in “I don’t care if it quacks like a duck, it’s not called duck.”
- mcfedr 2y agoCheck out what are often called tagged types. You basically define a `type A = string &{a: SomeSymbol}` And then have a type assertion function that just returns true, and you have control over the places A can come from
- Waterluvian 2y agoAh yeah I remember poking at that. I should review it again. I think at the time it felt like a bit of a hack, but maybe some features of the past years of TS updates have helped. I assume the idea is to lie to the type system about the existence of the symbol, and at runtime it is just a string.
- TOGoS 2y agoTo me it feels like less of a hack if I can make the type declaration not a lie. e.g. type FooID = string & { typeName? : "FooID" } Read as 'of course this thing doesn't have a typeName[1] property, since it's a string, but if it did have the property, the value would be "FooID"'. You can then cast between FooID and string, but not between FooID and some other type that declares a typeName property. [1] I actually tend to use 'classRef' with an RDFish long name for the type, but that makes examples longer and isn't the point.
- Waterluvian 2y ago
- amenghra 2y agoUnits might seem simple but they have a ton of edge cases. Do you want to be able to add inches and feet? Be careful about potential precision/rounding issues. What is the unit for a temperature delta? You can’t simply keep the original unit (eg C or F) because conversion from F to C is a different rule than ΔF to ΔC. Etc. Units do prevent bugs in programs, so they have an important role to play. But they also need to be designed very carefully. Java adopted units via JSR 385 (https://belief-driven-design.com/java-measurement-jsr-385-210f2/ https://belief-driven-design.com/java-measurement-jsr-385-21...)
- dwattttt 2y ago> Do you want to be able to add inches and feet? This probably doesn't have to be too complicated; the usual answer for Rust is "no". Rust doesn't even let you "just" add two unsigned integers of different sizes. Following that design, I would imagine units would require an explicit "turn feet into inches" or the other way around.
- vlovich123 2y agoMight be annoying if you’re working with floating point but given that each conversion introduces error, it’s probably good to be explicit and recommend internally to be consistent
- stouset 2y agoThanks to generics you could theoretically work with whatever underlying type makes the most sense for your use-case. let v1 : Inches<Ratio> = Ratio::new(5, 8).into(); let v2 : Inches<Ratio> = Ratio::new(3, 8).into(); let v3 : Feet<_> = (v1 + v2).into(); assert_equal!(v3, Ratio::new(1, 12));
- throwawaymaths 2y agono that's not the point. if you let rust automagically decide when and where to apply conversions you could easily wind up in a situation where you have more operations than you need, which increases numerical error, and also be a bitch to uncover or refactor to minimize conversions.
- thesuperbigfrog 2y agoI would love to see refinement types added to Rust. They are very handy for preventing errors and expressing intent in Ada: https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Developer/chapters/05_Type_System.html https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel...
- weinzierl 2y agoI 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 agoI assume modulo?
- loeg 2y agoUh, seemingly, yeah. 10+11 = 21. No bounds checking on addition or assignment. https://onlinegdb.com/3KhhaReLV https://onlinegdb.com/3KhhaReLV
- int_19h 2y agoThat 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
- JoshTriplett 2y agoAs a related concept, we've talked about adding "pattern types" to Rust: `Result<T> is Err(_)` (the type of a Result that you've just confirmed is an `Err`, so you don't have to handle the `Ok` case), or `u32 is 1..` (equivalent to `NonZero<u32>` but more flexible).
- bonzini 2y agoIs the former different from a hypothetical Result::Err type (I don't know if you'd spell that Result::Err<T> or Result::<T>::Err)?
- JoshTriplett 2y agoSame concept, but generalized to any type, not just enums.
- n_plus_1_acc 2y agoDifferent solutions to the same problem. Pattern types are more general than enum variant types.
- ordu 2y agoI'd really like to have them. If I'm writing an algorithm that maps interval (0, 1) of probabilities onto different intervals of u32 integers, and probabilites are also represented as integers (an integer part of p*2^n), I will want to have different units for those integer probabilites and their mapped values. I don't want to mix them accidentally and to add probability and a mapped probability accidentally. Probably I dont want to add cumulative probability and a probability, though I'm not really sure about that, because sometimes I want to add (for example when calculating cumulative probabilities) and I want to compare them. Though maybe it will work with some exotic rules, like CumProb-CumProb -> Prob, while CumProb+CumProb is forbidden? And there are more examples of that, I can have probabilities from different distributions, I don't want to add them accidentally, though multiplications of them is all over the place, so let it be. Of course I have no hope that any language could deal with the explosion of types that are needed to represent this, but if compiler just gave me f64 as a result of multiplication of probabilites, I'd be happy. It can be done in Rust on case by case bases, but it is a lot of boilerplate. The issue is the typedef IntProb = u32, treat IntProb like an alias to u32 and rustc converts these types into each other silently like C compiler converts int to char. One can do struct IntProb(u32), but then it would be needed to implement traits like Add, Mul, Cmp and so on, which is possible but it is too much work. If it was possible to force rustc to treat typedef MyType = {NumericType} as a distinct numeric type that requires explicit conversion into NumericType, while retaining all the traits of NumericType, just substituting in them NumericType with MyType, it would be great. I think, that all the complexities described in the article stem from the attempt to create an universal instrument that can do everything and to keep bees. The real difficulty is to pick a small subset of wants, that will cover 80% of needs, while being really simple. I see no issues with occasional .into::<Length<f64>>(), like I see no issues with (my_struc.index as usize), if I keep index as u8 to spare memory, but use it as usize of course. I see no need in different units for the same quantity, because in any case I'd want to convert everything into the same uniform units before I start adding and multiplying. But I'd like to have restrictions on available operations between different types, and I'd like to have a possibility to add optional dynamic checks for type value, that I could turn on for a debug build and turn off for a release one. For example, I'd like to check that any probability p fits into [0, 1].
- eddsolves 2y agoI think liquid Haskell is a great example of refinement types? https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/