6 ms·
Type Inference That Sticks
- jbandela1 4y agoI think JetBrains actually does something like this. When writing Rust or Kotlin or C++ (these are the ones I have used) the editor will annotate the inferred types with the actual type and you can see it in the editor (with a slightly different font to differentiate).
- realharo 4y agoVS Code also supports inlay hints for both inferred types, and parameter names https://code.visualstudio.com/docs/typescript/typescript-editing#_inlay-hints https://code.visualstudio.com/docs/typescript/typescript-edi... I think it's turned off by default for most languages though - probably considered unnecessary, as you can always just hover over the variable. Also, unlike the JetBrains IDEs, I don't think you can Ctrl+Click on such a hint to navigate to its definition in VS Code (like you can in normal code).
- jaredly 4y agoYeah, it is definitely nice to have inferred types surfaced to you, but in these systems they are still re-computed on every textual edit, as opposed to being "sticky" (persisted in the source tree).
- brundolf 4y agoLots of IDEs do that for lots of languages these days, and it's wonderful, but I don't think that's the kind of thing they're talking about here in the article
- IshKebab 4y agoYeah they're talking about recording the type inferences in the source code. Interesting idea but I feel like it might fall down the same way all "not just text" ideas fall down - the whole coding world is built around plain text. Git, diff, GitHub, IDEs, etc. Some inferred types in Rust can be pages long. Have fun with those merge conflicts!
- rom-antics 4y agoI've seen a few experiments like this that store extra information behind the scenes. My first question is always how does it work with source control? Dealing with diffs/merges of that underlying serialization format would get fatiguing quick. I don't think the world will move over to something like this until there's a good answer there.
- mteam88 4y agoWhat about actual comments in the source code? Or type annotations if the language supports them...
- jaredly 4y agoSource control does look very different in a projectional language, as git diffs no longer make much sense (viewing a pull-request with the source tree's JSON blob is essentially useless). Unison is the language that's gone farthest with this, as far as I know; their solution to diffs & merges is to handle everything from within their CLI, bypassing git entirely. I imagine I'll do something similar.
- CamJN 4y agoIf I may, I’d suggest instead of shunning git, which is widely preferred as people’s revision control, perhaps consider writing a diff plugin for git to render out the diffs nicely, and include that tool with the compiler/interpreter install.
- dangoor 4y agoI don't know anything about how you're storing the source, but if the data elided from view could be stored in files next to the source that were more readable than JSON, you could potentially take advantage of the whole git ecosystem still. People could put code up for review and the reviewers could even confirm if the additional (normally out of sight) information made sense to them. FWIW, I'm totally on board with the idea of focusing on the interactive experience, but history has shown it to be very difficult for language environments not based on files to cross the chasm into more common use. (If you don't care about lots of users, then ignore this entire comment! Plus, it's always _possible_ that something will cross over, but we've got decades of people trying...) Anyhow, I'm really excited to see where you go with this!
- tel 4y agoWhile I can imagine worlds which improve upon this (working in Agda and Coq is a great way to see a glimpse of it) I honestly feel like my dominant way of working is conversational with the compiler. I tend to write code for a bit, and then ask it one of two questions (1) what is the type of this thing or (2) is there any part of this that looks wrong? In particular (2) is obviously type checking (which is great to run in a fast background loop like `cargo watch -x check`) and (1) is some system for "please insert an annotation on this variable with your current inferred type". This happens near constantly, and a very common "move" I make typing is to isolate some section and give it a temporary variable name just so I can receive that annotation. The flow there could be better, to be sure. The proposal here is kind of fascinating with regard to question (1), making it less interactive and more reactive. It reminds me of, say, working with Observable, where you make edits throughout your document and watch the dependents react. To that end, being able to draw circles around fragments of code and have a persistent monitor that reactively outputs either "error: [reason]" or the type of that variable as I edit the code seems great. Though I do feel a little uncomfortable with that being literally embedded in the code. Code being reactively edited by a program makes me itch with fear of file corruption.
- gnulinux 4y ago> While I can imagine worlds which improve upon this (working in Agda and Coq is a great way to see a glimpse of it) I honestly feel like my dominant way of working is conversational with the compiler. Agda programmer here. Not sure what you mean here. Although Agda does save a binary cache file to minimize type-checking latency (.agdai, "agda interface") with compressed type information, it does not have any kind of hidden state. This is very different than what the OP suggests. Other than this, I agree with you. When I write code in a typed language I have a conversation with the compiler. I keep asking, is this ok, what do you think about this, what type is this... Which is why I find OP misguided. You can have a conversation with the compiler without hidden state.
- tel 4y agoSorry, not referring to the whole post wrt Agda, just the vision of interactivity that proof search and tactics give you.
- brundolf 4y agoImagine debugging a type inference problem when there's all this hidden state No, I'm sorry, but type annotations are where the conversation happens. It's very very important in my view that type inference is a pure - ideally easy to mentally model - function of the source code you're looking at. Type annotations let you negotiate with and probe that function, and then once you understand what it's doing and have gotten it in a good place you can remove all the ones that aren't needed Adding (hidden!) state to that process sounds like my worst nightmare as a programmer
- lambdaxymox 4y agoType inference occasionally bites one's hand when pushing data across an FFI boundary. In one instance I was writing some graphics code for a project and for some reason the colors in the rendering model were coming out all wrong on the screen (TL;DR it ended up looking like two of the color channels were missing from some texture maps) and it turns out that Rust inferred the type of the buffer as a vector of f64s instead of a vector of f32s. Putting the type in specifically fixed the problem promptly. Lesson learned: Sometimes type inference fails, and always annotate your types at FFI boundaries!
- brundolf 4y agoYeah, it's important to annotate anything that interacts with the outside world, because that code/API isn't available for the compiler to reason about before run-time. Same goes with HTTP endpoints (on both the client and the server)
- jaredly 4y agoSo I think "easy to mentally model" gets harder and harder to achieve as the type system becomes more powerful. If your conclusion is that we keep the type system limited in power, that's valid! but not what I'm exploring. Another point that I failed to make in the post (thanks for the pushback!) is that type inference algorithms leave you high & dry in the presence of a type error. Then you're left with lots of hidden state (the internal steps the algorithm took before arriving at the error) and the final conclusion, which, if you're lucky, points you to two places in the code where the inferred types are in disagreement. With my proposed system, all types are annotated all the time (to be shown or hidden via editor flag, or on hover), and the annotations are updated in response to actions taken within the editor. The "algorithm" becomes extremely simple, with almost no intermediate steps. Of course, proof will be in the pudding, if I can actually achieve a pleasant editing experience :)
- mountainriver 4y agoThis is really awesome, such a useful direction to pursue. Look forward to seeing where you take things
- mpweiher 4y agoThis goes directly at one of the paradoxes of typing. On the one hand, one of the main benefits of types, and the only one for which there is empirical evidence, is the (automatically checked) documentation effect. For this, the types have to be visible. On the other hand, not having to type in the types all the time and having them inferred instead seems like a major convenience. For this type types cannot be visible. Compared to that, the inefficiency of having to do the work over and over seems like a relatively minor issue, though compile times are getting ever more problematic. So I really like the idea of having types that can be inferred and persisted, though I'd prefer the language to make some room for having "provisional" type annotations, so basically using all sources for getting the types: the user, inference, the running program (dynamic languages can find out about actual types at runtime).
- foota 4y agoAn editor can allow seeing types without having them in the code.
- deleted 4y ago[deleted]
- layer8 4y agoYou already can have both, at least in certain contexts: In my IDE, when I write a function call, I can press Alt+Return to have the IDE assign the return value to a new explicitly-typed variable, with the type inferred from the call. Likewise, when for example the return type of the function changes, so that the type of the variable doesn’t match anymore, the IDE highlights that, and again I can press Alt+Return to have the declared type of the variable be updated to match. The point is, in those contexts I never have to actually type the variable type myself. This is similar to what TFA proposes, and it doesn’t require storage of type information separately from the source code, or in some AST representation. The type information is simply “stored” in the plain-text source code itself, as type declarations/annotations. I like this approach better than having the IDE merely render inferred type information alongside the source code, because (a) when the type information is part of the actual source code, then it is always visible, e.g. in diffs and source control tools, and (b) like TFA suggests it gives opportunity to interactively resolve type conflicts, and making those decisions “sticky”. With the right IDE tooling, you still wouldn’t need to type the types yourself mist of the time.
- revskill 4y agoIf i got a weird typing issue and i have no clue about it, then i know my design is mostly wrong. That's one of usefulness of a static type checker for me.