In my understanding Rust may gain this feature via “pattern types.”

Where can I sign?

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

Ada has this ability to define ranges for subtypes. I wish language designers would look at Ada more often.

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.

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

>But it takes a while

*Checks watch*

We're going on 45 years now.

Naaa ... most "new" languages are just reinventions of stuff that's been around for ... 45 years, by people who should know better.

Well, ada is practical

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.

<3

Hello! I was curious if you would happen to have any advice or particular comp sci papers you would point as aspiring compiler developer towards.

I think I'm sort of who you're talking about. I have no formal education and I am excited to have my compiler up to the point I can run a basic web server. I think it's a fairly traditional approach with a lexer, recursive decent parser, static analysis, then codegen. I'm going for a balance between languages like Ruby and Rust to get the best of both worlds.

You'll probably find it funny that I don't know the name for the technique Im using for dynamic dispatch. The idea is that as long as a collection doesn't have mixed types then the compiler statically knows the type even in loops and such. Only for mixed type collections, or maybe trait functions, will the compiler be forced to fall back to runtime dynamic dispatch. I find this cool because experts can write fast static code, but beginners won't be blocked by the compiler complaining about things they shouldn't have to care about yet. But, syntax highlighting or something may hint there are improvements to be made. If there is a name for this, or if it's too small a piece to deserve one, I would be very curious to know!

On Refinement Types, I not sure they are a good idea for general purpose languages and would love to be challenged on this. Succinctly, I think it's a leaky abstraction. To elaborate, having something like a `OneThroughTen` type seems helpful at first, but in reality it's spreading behaviour potentially all over the app as opposed to having a single function with the desired behaviour. If a developer has multiple spots they're generating a number and one spot is missing a check and causes a bug, then hopefully a lesson was learned not to do that and instead have a single spot for that logic. The heavy handed complexity of Refinement Types is not worth it to solve this situation.

If there are any thoughts out there they would be greatly appreciated!

Pascal had this many decades ago, how long do we have to wait?

VHDL has this feature too, being based on Ada.

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.

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.

And I wish people would remember Pascal and Modula-2 had it before Ada. :)

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.

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.

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.

It can work. It depends on context. Like let's say these types are from a well renowned library or one that's been used by the codebase for a long time.

If you trust the type, then it's fine. The code is safer. In the world of of the code itself things are easier.

Of course like what you're complaining about, this opens up the possibility of more bugs in the world of types, and debugging that can be a pain. Trade offs.

In practice people usually don't go crazy with type level functions. They can do small stuff, but usually nothing super crazy. So type script by design sort of fits the complexity dynamic you're looking for. Yes you can do type level functions that are super complex, but the language is not designed around it and it doesn't promote that style either. But you CAN go a little deeper with types then say a language with less power in the type system like say Rust.

Typescript's type system is turing complete, so you can do basically anything with it if this sort of thing is fun to you. Which is pretty much my problem with it: this sort of thing can be fun, feels intellectually stimulating. But the added power doesn't make coding easier or make the code more sound. I've heard this sort of thing called the "type puzzle trap" and I agree with that.

I'll take a modern hindley milner variant any day. Sophisticated enough to model nearly any type information you'll have need of, without blurring the lines or admitting the temptation of encoding complex logic in it.

Typescript’s type system can run Doom.

https://youtu.be/0mCsluv5FXA

(derogatory)

I hope in 10 years we look to this typescript phase the way we see the coffeescript hype.

Coffeescript went obsolete because many of the features were directly folded into JS ES6.

If you think typescript will go the way of coffeescript. Well. First off, coffeescript was waaay less popular than typescript. Second, if it does it just means types will get folded directly into js.

>Which is pretty much my problem with it: this sort of thing can be fun, feels intellectually stimulating. But the added power doesn't make coding easier or make the code more sound.

In practice nobody goes too crazy with it. You have a problem with a feature almost nobody uses. It's there and Range<N> is like the upper bound of complexity I've seen in production but that is literally extremely rare as well.

There is no "temptation" of coding complex logic in it at all as the language doesn't promote these features at all. It's just available if needed. It's not well known but typescript types can be easily used to be 1 to 1 with any hindley milner variant. It's the reputational baggage of JS and frontend that keeps this fact from being well known.

In short: Typescript is more powerful then hindley milner, a subset of it has one to one parity with it, the parts that are more powerful then hindley milner aren't popular and used that widely nor does the flow of the language itself promote there usage. The feature is just there if you need it.

If you want a language where you do this stuff in practice take a look at Idris. That language has these features built into the language AND it's an ML style language like haskell.

I have definitely worked in TS code bases with overly gnarly types, seen more experienced devs spend an entire workday "refactoring" a set of interrelated types and producing an even gnarlier one that more closely modeled some real world system but was in no way easier to reason about or work with in code. The advantage of HM is the inference means there is no incentive to do this, it feels foolish from the beginning.

ATS does this. Works quite well since multiplication by known factors and addition of type variables + inequalities is decidable (and in fact quadratic).

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/

[1]: https://github.com/microsoft/TypeScript/issues/43505

Related 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... - 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

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

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.

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.

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.

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.

What the GP described could be achieved with dependent types, but could also be achieved with a less powerful type system, and the reduced power can sometimes lead to enormous benefits in terms of how pleasant it actually is to use. Check out "refinement types" (implemented in Liquid Haskell for example). Many constraints can be encoded in the type system, and an SMT solver runs at compile time to check if these constrains are guaranteed to be satisfied by your code. The result is that you can start with a number that's known to be in [0..10), then double it and add five, and then you can pass that to a function that expects a number in [10..20). Dependent types would typically require some annoying boilerplate to prove that your argument to the function would fall within that range, but an SMT solver can chew through that without any problem.

There's refinement types, which are less general than dependant types, but sufficient to provide ranges, and simpler to implement because the type only needs to be associated with a predicate.

in raku, that’s spelled

  subset OneToTen of Int where 1..10:

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

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

mainly I find Raku (and the community) much -Ofun

In Common Lisp it's

  (deftype One-To-Ten ()
    '(Integer 1 10))

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.

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.

Here is example of compile time error with wrong newtype argument:

https://play.rust-lang.org/?version=stable&mode=debug&editio...

rust-analyzer gives an error directly in IDE.

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.

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

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?

Clojure does bounded values/regex natively in Clojure Spec, and also the Malli library from Metosin

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.