5 ms·

Yep. For this reason, I wish more languages supported bound integers. Eg, rather than saying x: u32, I want to be able to use the type system to constrain x to

• steveklabnik 1y ago
  In my understanding Rust may gain this feature via “pattern types.”
  • ijustlovemath 1y ago
    Where can I sign?
    • steveklabnik 1y ago
      Gonna be honest, at this point, I don't know how this all works in the Rust Project. https://github.com/rust-lang/types-team/issues/126 https://github.com/rust-lang/types-team/issues/126
• mcculley 1y ago
  Ada has this ability to define ranges for subtypes. I wish language designers would look at Ada more often.
  • tylerhou 1y ago
    Academic language designers do! But it takes a while for academic features to trickle down to practical languages—especially because expressive-enough refinement typing on even the integers leads to an undecidable theory.
    • idbehold 1y ago
      >But it takes a while *Checks watch* We're going on 45 years now.
      • drpixie 1y ago
        Naaa ... most "new" languages are just reinventions of stuff that's been around for ... 45 years, by people who should know better.
        • deleted 1y ago
          [deleted]
    • spookie 1y ago
      Well, ada is practical
    • geysersam 1y ago
      Aren't most type systems in widely used languages Turing complete and (consequently) undecidable? Typescript and python are two examples that come to mind But yeah maybe expressive enough refinement typing leads to hard to write and slow type inference engines
    • voidhorse 1y ago
      Eh, idk. I think the reasons are predominantly social, not theoretical. For every engineer out there that gets excited when I say the words "refinement types" there are twenty that either give me a blank stare or scoff at the thought, since they a priori consider any idea that isn't already in their favorite (primitivistic) language either too complicated or too useless. Then they go and reinvent it as a static analysis layer on top of the language and give it their own name and pat themselves on the back for "inventing" such a great check. They don't read computer science papers.
      • y0ned4 1y ago
        <3
  • jjmarr 1y ago
    VHDL has this feature too, being based on Ada.
  • fny 1y ago
    Range checks in Ada are basically assignment guards with some cute arithmetic attached. Ada still does most of the useful checking at runtime, so you're really just introducing more "index out of bounds". Consumer this example: procedure Sum_Demo is subtype Index is Integer range 0 .. 10; subtype Small is Integer range 0 .. 10; Arr : array(Index) of Integer := (others => 0); X : Small := 0; I : Integer := Integer'Value(Integer'Image(X)); -- runtime evaluation begin for J in 1 .. 11 loop I := I + 1; end loop; Arr(I) := 42; -- possible out-of-bounds access if I = 11 end Sum_Demo; This compile, and the compiler will tell you: "warning: Constraint_Error will be raised at run time". It's a stupid example for sure. Here's a more complex one: procedure Sum_Demo is subtype Index is Integer range 0 .. 10; subtype Small is Integer range 0 .. 10; Arr : array(Index) of Integer := (others => 0); X : Small := 0; I : Integer := Integer'Value(Integer'Image(X)); -- runtime evaluation begin for J in 1 .. 11 loop I := I + 1; end loop; Arr(I) := 42; -- Let's crash it end Sum_Demo; This again compiles, but if you run it: raised CONSTRAINT_ERROR : sum_demo.adb:13 index check failed It's a cute feature, but it's useless for anything complex.
    • mcculley 1y ago
      The comment to which I replied is about two concepts: Defining subtypes and an optimization made possible by them. I get a lot of value out of compile time enforcement of subtypes (e.g., defining a function as requiring a parameter be Index instead of Integer) finding errors in my thinking. It is more than "cute" to me. As for the possible optimization of the array bounds check and it happening at runtime instead of compiletime, isn't that a failure of GNAT and not Ada? Can't a sufficiently smart compiler detect the problem in your example? Regardless, I am not convinced that getting around the compiletime type safety by casting with Integer'Value(Integer'Image(X)) proves anything. I will still prefer having subtypes over not having them.
  • pjmlp 1y ago
    And I wish people would remember Pascal and Modula-2 had it before Ada. :)
    • mcculley 1y ago
      Ah, well I never did Pascal as a job and never used Modula-2 at all, so I didn’t know that they had that also.
• ninetyninenine 1y ago
  This can be done in typescript. It’s not super well known because of typescripts association with frontend and JavaScript. But typescript is a language with one of the most powerful type systems ever. Among the popular languages like golang, rust or python typescript has the most powerful type system. How about a type with a number constrained between 0 and 10? You can already do this in typescript. type onetonine = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 You can even programmatically define functions at the type level. So you can create a function that outputs a type between 0 to N. type Range<N extends number, A extends number[] = []> = A['length'] extends N ? A[number] : Range<N, [...A, A['length']]>; The issue here is that it’s a bit awkward you want these types to compose right? If I add two constrained numbers say one with max value of 3 and another with max value of two the result should be max value of 5. Typescript doesn’t support this by default with default addition. But you can create a function that does this. // Build a tuple of length L type BuildTuple<L extends number, T extends unknown[] = []> = T['length'] extends L ? T : BuildTuple<L, [...T, unknown]>; // Add two numbers by concatenating their tuples type Add<A extends number, B extends number> = [...BuildTuple<A>, ...BuildTuple<B>]['length']; // Create a union: 0 | 1 | 2 | ... | N-1 type Range<N extends number, A extends number[] = []> = A['length'] extends N ? A[number] : Range<N, [...A, A['length']]>; function addRanges< A extends number, B extends number >( a: Range<A>, b: Range<B> ): Range<Add<A, B>> { return (a + b) as Range<Add<A, B>>; } The issue is to create these functions you have to use tuples to do addition at the type level and you need to use recursion as well. Typescript recursion stops at 100 so there’s limits. Additionally it’s not intrinsic to the type system. Like you need peanno numbers built into the number system and built in by default into the entire language for this to work perfectly. That means the code in the function is not type checked but if you assume that code is correct then this function type checks when composed with other primitives of your program.
  • lucianbr 1y ago
    Complexity is bad in software. I think this kind of thing does more harm than good. I get an error that I can't assign something that seems to me assignable, and to figure out why I need to study functions at type level using tuples and recursion. The cure is worse than the disease.
• vmchale 1y ago
  ATS does this. Works quite well since multiplication by known factors and addition of type variables + inequalities is decidable (and in fact quadratic).
• nikeee 1y ago
  I proposed a primitive for this in TypeScript a couple of years ago [1]. While I'm not entirely convinced myself whether it is worth the effort, it offers the ability to express "a number greater than 0". Using type narrowing and intersection types, open/closed intervals emerge naturally from that. Just check `if (a > 0 && a < 1)` and its type becomes `(>0)&(<1)`, so the interval (0, 1). I also built a simple playground that has a PoC implementation: https://nikeee.github.io/typescript-intervals/ https://nikeee.github.io/typescript-intervals/ [1]: https://github.com/microsoft/TypeScript/issues/43505 https://github.com/microsoft/TypeScript/issues/43505
  • mnahkies 1y ago
    Related https://github.com/microsoft/TypeScript/issues/54925 https://github.com/microsoft/TypeScript/issues/54925 My specific use case is pattern matching http status codes to an expected response type, and today I'm able to work around it with this kind of construct https://github.com/mnahkies/openapi-code-generator/blob/main/packages%2Ftypescript-fetch-runtime%2Fsrc%2Ftypes.ts#L1-L26 https://github.com/mnahkies/openapi-code-generator/blob/main... - but it's esoteric, and feels likely to be less efficient to check than what you propose / a range type. There's runtime checking as well in my implementation, but it's a priority for me to provide good errors at build time
• scottgg 1y ago
  The generic magic for this is called “dependant types” I believe - generics that can take values as well as types as parameters. Idris supports these
  • ameliaquining 1y ago
    The full-blown version that guarantees no bounds-check errors at runtime requires dependent types (and consequently requires programmers to work with a proof assistant, which is why it's not very popular). You could have a more lightweight version that instead just crashes the program at runtime if an out-of-range assignment is attempted, and optionally requires such fallible assignments to be marked as such in the code. Rust can do this today with const generics, though it's rather clunky as there's very little syntactic sugar and no implicit widening.
    • tialaramex 1y ago
      AIUI WUFFS doesn't need a full blown proof assistant because instead of attempting the difficult problem "Can we prove this code is safe?" it has the programmer provide elements of such a proof as they write their program so it can merely ask "Is this a proof that the program is safe?" instead.
      • ameliaquining 1y ago
        This is also approximately true of Idris. The thing that really helps Wuffs is that it's a pretty simple language without a lot of language features (e.g., no memory allocation and only very limited pointers) that complicate proofs. Also, nobody is particularly tempted to use it and then finds it unexpectedly forbidding, because most programmers don't ever have to write high-performance codecs; Wuffs's audience is people who are already experts.
        • ameliaquining 1y ago
          Also, Wuffs doesn't let you prove arbitrary correctness properties, it aims only to prove the absence of memory corruption. That reduces how expressive the proof system has to be.
• librasteve 1y ago
  in raku, that’s spelled subset OneToTen of Int where 1..10:
  • yoz-y 1y ago
    Off topic: do you use raku in day to day life? I tried learning it but perl5 remains my go-to when I just need to whip something up
    • librasteve 1y ago
      yes … I find it as useful as I used to find perl (spent 4 years as a perl coder back in the day) and use for ad hoc scripts … data migration, PDF/CSV scraping, some LLM prompt engineering in a business setting, wrote a module to manage/install Wordpress on EC2 for example raws-ec2 —eip —nsu launch raws-ec2 —q connect | pbcopy https://raku.land/zef:librasteve/CLI::AWS::EC2-Simple https://raku.land/zef:librasteve/CLI::AWS::EC2-Simple mainly I find Raku (and the community) much -Ofun
  • tmtvl 1y ago
    In Common Lisp it's (deftype One-To-Ten () '(Integer 1 10))
• someone_19 1y ago
  You can do this quite easily in Rust. But you have to overload operators to make your type make sense. That's also possible, you just need to define what type you get after dividing your type by a regular number and vice versa a regular number by your type. Or what should happen if when adding two of your types the sum is higher than the maximum value. This is quite verbose. Which can be done with generics or macros.
  • josephg 1y ago
    You can do it at runtime quite easily in rust. But the rust compiler doesn’t understand what you’re doing - so it can’t make use of that information for peephole optimisations or to elide array bounds checks when using your custom type. And you don’t get runtime errors instead of compile time errors if you try to assign the wrong value into your type.
    • deleted 1y ago
      [deleted]
    • someone_19 1y ago
      Here is example of compile time error with wrong newtype argument: https://play.rust-lang.org/?version=stable&mode=debug&edition=2024&gist=ecfa34c3577f8b0e3e60b336c189ab1c https://play.rust-lang.org/?version=stable&mode=debug&editio... rust-analyzer gives an error directly in IDE.
• bakul 1y ago
  Pascal had range types such as 0..9 (as of 1970). Subranges could also be defined for any scalar type. Further, array index types were such ranges.
• archargelod 1y ago
  Nim[0] supports subrange types: type Foo = range[1 .. 10] Bar = range[0.0 .. 1.0] # float works too var f:Foo = 42 # Error: cannot convert 42 to Foo = range 1..10(int) var p = Positive 22 # Positive and Natural types are pre-defined [0] - https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types
• fny 1y ago
  But wouldn't that also require code execution? For example even though the compiler already knows the size of an array and could do a bounds check on direct assigment (arr[1] = 1) in some wild nested loop you could exceed the bounds that the compiler can't see. Otherwise you could have type level asserts more generally. Why stop at a range check when you could check a regex too? This makes the difficulty more clear. For the simplest range case (pure assignment) you could just use an enum?
• 0_gravitas 1y ago
  Clojure does bounded values/regex natively in Clojure Spec, and also the Malli library from Metosin
  • iLemming 1y ago
    Spec and Malli in Clojure feel like effing magic - so expressive, so simple - "data as code" philosophy means validations schemas are first-class citizens that can be manipulated, stored, transmitted, and reasoned about like any other data and that's just beautiful. For some type checks you can express in them, it is nearly impossible to achieve in TS, Rust or even Haskell. Clojure makes the complex feel simple because the language itself is designed around data transformation. That power of course does come with a price, there does not exist a static analyzer that automatically checks things, even though you can pretty much generate beautiful tests based on specs. I think e.g. Rust teams can have more junior devs safely contribute due to enablement of less variability in code quality - the compiler enforces discipline. Clojure teams need higher baseline discipline but can move incredibly fast when everyone's aligned. It's saddening to see when Clojure gets outright dismissed for being "untyped", even though it absolutely can change one's perspective about type systems.