4 ms·

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
  - dabears 1y ago
    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!
- ninalanyon 1y ago
  Pascal had this many decades ago, how long do we have to wait?
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.

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
- dabears 1y ago
  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!
ninalanyon 1y ago
Pascal had this many decades ago, how long do we have to wait?

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.