4 ms·

Here's my million dollar take: The linter/typechecker should add in the inferred types explicitly. If you want to refactor, it's up to you to delete the types.

Here's my million dollar take: The linter/typechecker should add in the inferred types explicitly. If you want to refactor, it's up to you to delete the types. Then a re-run of the linter/typechecker can re-check and add them back in. For bonus credit, we should also automate the removal of unnecessary explicit types. A de-expliciter program should be able to go delete all explicit types which are inferable. Personally I really like the spot readability of explicit types. I'd rather it be in the code, see the ripple out of changes to the codebase.

pvinis 4y ago
Fun! that would be cool, but I wonder how this would work if a func just returns 4 and then the number type was added, and then I change it to return "wow". Do I have a type error or does my func type updates?
- nawgz 4y ago
  Good point. For this case, it's easy to imagine - such a construct would infer the function's new return type, and then any call-sites which have a mismatch would require updating. But you raise the real question of how the compiler could know when types were added by the inference-er versus the programmer
- gjm11 4y ago
  I think that if I were building a system that worked this way, automatically-inserted type declarations would be distinguished somehow (preferably in a way that in good text editors just appears as different formatting), and then when you change the function to return "wow" the compiler/linter/magic-type-annotator will see that the only things that need updating are ones it inserted itself, and just do it. If you edit any of those automatically-inserted type declarations, though, they're fixed and doing things that violates them becomes a type error rather than an auto-rewriting opportunity.
psykotic 4y ago
> If you want to refactor, it's up to you to delete the types. The fact that f(g(x)) and { let y = g(x); f(y) } are equally robust to changes in g(x)'s type is an advantage of type inference. It doesn't seem reasonable to place an additional burden on the person who chose to assign a name to the subexpression value. > Personally I really like the spot readability of explicit types. You can use an IDE that displays inferred types as type inlays (for variables) and as sidebar info (for expressions). But I've often wanted a way to export such sideband data (including subexpression types and cross-reference links) so you could display it for code reviews, etc, without teaching those tools about your language specifically, so I'm sympathetic to the general goal. Regarding explicitness and readability, I like Rust's idea of letting you partially specify types by using _ as a placeholder to say "infer this part". For example, you can specify that something is a Vec without specifying its item type: let v: Vec<_> = iter.collect();
- mike_hock 4y ago
  Explicit types are a form of assertion. In the example { let y = g(x); f(y) } I do not want to assert anything on the type of y but in { let y: Foo = g(x); // Do complex stuff with y f(y) } I wrote the middle part with a specific mental model of what y is, and if that changes, I want to review that section to make sure that the semantics still match what I thought they were and does not just happen to be valid syntactically. I do not want some automated tool to either strip assertions from my code, nor do I want it to synthesize assertions from a static analysis run of a particular version of the code. If I'm just gonna mindlessly remove all assertions and re-synthesize them on every refactor, they're useless.
- rektide 4y ago
  > You can use an IDE that displays inferred types as type inlays This isn't captured in the code & that is a huge weakness. Being able to see the code change over time is, in my view, a huge advantage. Reliance on high-tech tools to discern meaning & do the inference for us feels far weaker than simply encoding the good information into the code. That just seems far better to me, far more robust. Some of this is that I'm a vim user and don't want to have to go lookup & configure a LSP daemon for each file I evaluate, but some of it just feels like base common sense, that the tradeoff of actually being explicit are overwhelming & clear. I think I argued against this pretty resolutely the first time around. I don't think your post adds anything or changes my mind at all.
ridiculous_fish 4y ago
This idea of a separate phase modifying your input is really powerful, and I think more languages should design their syntax around that idea. A nice example comes from AppleScript of all places. You can close a block with just `end`, or by referencing the opening like `end if`. When you save a file, the compiler rewrites all the `end`s to the second form. Any other examples where the language is designed to be enriched by tooling?
- chrismorgan 4y ago
  I’ve been designing a new lightweight markup language for the past few months, and I have decided to take this approach for things like typographic punctuation: rather than the markup language engine embedding fallible heuristics (turning ' into ‘ or ’, based on the natural language’s usage) or annoying ligatures (e.g. TeX has -- → –, --- → —, ` → ‘ and ' → ’), I will provide a linter that provides flexible rules for such transformations and the ability to perform in-place replacement. This linter will also be able to perform source autoformatting of various kinds, e.g. visual alignment of list indentation and table columns, and it’ll be hooked into LSP so direct text editor integration is possible.
- danaugrs 4y ago
  I'm building a language (https://flame.run https://flame.run) and trying a similar idea for imports. In my language there is no package manager. Files just import other files, locally or from URLs (like Deno). But, unlike Deno, I'd like to store the hashes of the imported files for security. I don't want to create a secondary file a la package.json, or even two files like go.mod/go.sum. So the idea I'm probably going with is that whenever you run/compile a program the tooling warns you and asks to insert the missing hashes of the imported files for you, inline.

pvinis 4y ago

Fun! that would be cool, but I wonder how this would work if a func just returns 4 and then the number type was added, and then I change it to return "wow". Do I have a type error or does my func type updates?

nawgz 4y ago
Good point. For this case, it's easy to imagine - such a construct would infer the function's new return type, and then any call-sites which have a mismatch would require updating. But you raise the real question of how the compiler could know when types were added by the inference-er versus the programmer
gjm11 4y ago
I think that if I were building a system that worked this way, automatically-inserted type declarations would be distinguished somehow (preferably in a way that in good text editors just appears as different formatting), and then when you change the function to return "wow" the compiler/linter/magic-type-annotator will see that the only things that need updating are ones it inserted itself, and just do it. If you edit any of those automatically-inserted type declarations, though, they're fixed and doing things that violates them becomes a type error rather than an auto-rewriting opportunity.

psykotic 4y ago

> If you want to refactor, it's up to you to delete the types. The fact that f(g(x)) and { let y = g(x); f(y) } are equally robust to changes in g(x)'s type is an advantage of type inference. It doesn't seem reasonable to place an additional burden on the person who chose to assign a name to the subexpression value. > Personally I really like the spot readability of explicit types. You can use an IDE that displays inferred types as type inlays (for variables) and as sidebar info (for expressions). But I've often wanted a way to export such sideband data (including subexpression types and cross-reference links) so you could display it for code reviews, etc, without teaching those tools about your language specifically, so I'm sympathetic to the general goal. Regarding explicitness and readability, I like Rust's idea of letting you partially specify types by using _ as a placeholder to say "infer this part". For example, you can specify that something is a Vec without specifying its item type: let v: Vec<_> = iter.collect();

mike_hock 4y ago
Explicit types are a form of assertion. In the example { let y = g(x); f(y) } I do not want to assert anything on the type of y but in { let y: Foo = g(x); // Do complex stuff with y f(y) } I wrote the middle part with a specific mental model of what y is, and if that changes, I want to review that section to make sure that the semantics still match what I thought they were and does not just happen to be valid syntactically. I do not want some automated tool to either strip assertions from my code, nor do I want it to synthesize assertions from a static analysis run of a particular version of the code. If I'm just gonna mindlessly remove all assertions and re-synthesize them on every refactor, they're useless.
rektide 4y ago
> You can use an IDE that displays inferred types as type inlays This isn't captured in the code & that is a huge weakness. Being able to see the code change over time is, in my view, a huge advantage. Reliance on high-tech tools to discern meaning & do the inference for us feels far weaker than simply encoding the good information into the code. That just seems far better to me, far more robust. Some of this is that I'm a vim user and don't want to have to go lookup & configure a LSP daemon for each file I evaluate, but some of it just feels like base common sense, that the tradeoff of actually being explicit are overwhelming & clear. I think I argued against this pretty resolutely the first time around. I don't think your post adds anything or changes my mind at all.

ridiculous_fish 4y ago

This idea of a separate phase modifying your input is really powerful, and I think more languages should design their syntax around that idea. A nice example comes from AppleScript of all places. You can close a block with just `end`, or by referencing the opening like `end if`. When you save a file, the compiler rewrites all the `end`s to the second form. Any other examples where the language is designed to be enriched by tooling?

chrismorgan 4y ago
I’ve been designing a new lightweight markup language for the past few months, and I have decided to take this approach for things like typographic punctuation: rather than the markup language engine embedding fallible heuristics (turning ' into ‘ or ’, based on the natural language’s usage) or annoying ligatures (e.g. TeX has -- → –, --- → —, ` → ‘ and ' → ’), I will provide a linter that provides flexible rules for such transformations and the ability to perform in-place replacement. This linter will also be able to perform source autoformatting of various kinds, e.g. visual alignment of list indentation and table columns, and it’ll be hooked into LSP so direct text editor integration is possible.
danaugrs 4y ago
I'm building a language (https://flame.run https://flame.run) and trying a similar idea for imports. In my language there is no package manager. Files just import other files, locally or from URLs (like Deno). But, unlike Deno, I'd like to store the hashes of the imported files for security. I don't want to create a secondary file a la package.json, or even two files like go.mod/go.sum. So the idea I'm probably going with is that whenever you run/compile a program the tooling warns you and asks to insert the missing hashes of the imported files for you, inline.