4 ms·

Imagine 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

Imagine 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 ago
Type 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 ago
  Yeah, 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 ago
So 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 :)
- brundolf 4y ago
  > 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 So there are two possible reasons I can see for automatically "annotating" all the types: - Caching that info to easily show in the editor (which is a good feature, but many editors already do this without having to modify the source; it happens entirely editor-side) - Using the "current" inferred type as a jumping-off point for determining the "next" inferred type The second was my original interpretation, and what sounded so distressing as a user Consider this situation: 1. Your program and the inferred types are in one state 2. You modify some code which changes an inferred type 3. You change the (visible) code back to what it was previously, but now the inferred type is different because it was partially based on the previous inferred type This is what sounds like a nightmare, assuming I understand correctly that it's possible on the described system. The inferred types are now a state machine, where it matters not just what code is on screen, but how it got there.
  - jaredly 4y ago
    Hm so it is a state machine, but (my hope is that) all state transitions are simple and direct (and observable!) outcomes of user action. If the transitions get at all complex or unobservable, I'll probably call it a failed experiment. It might also end up being the case that users keep types "visible" at all times, only turning them off in certain situations. I can also imagine a flag to "only hide inferred types that are primitives" or something similar.
    - brundolf 4y ago
      Fair enough, and it's certainly an interesting experiment, don't want to discourage experimentation But I will say I think the desire to show the inferred types is orthogonal to the desire to persist them on disk, in the source-of-truth code files. If the state machine really is what you want to experiment with then have fun, but if your desire is just to give the user more visibility into inference, I think there are simpler ways to go about that
- 4y ago

lambdaxymox 4y ago

Type 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 ago
Yeah, 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 ago

So 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 :)

brundolf 4y ago
> 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 So there are two possible reasons I can see for automatically "annotating" all the types: - Caching that info to easily show in the editor (which is a good feature, but many editors already do this without having to modify the source; it happens entirely editor-side) - Using the "current" inferred type as a jumping-off point for determining the "next" inferred type The second was my original interpretation, and what sounded so distressing as a user Consider this situation: 1. Your program and the inferred types are in one state 2. You modify some code which changes an inferred type 3. You change the (visible) code back to what it was previously, but now the inferred type is different because it was partially based on the previous inferred type This is what sounds like a nightmare, assuming I understand correctly that it's possible on the described system. The inferred types are now a state machine, where it matters not just what code is on screen, but how it got there.
- jaredly 4y ago
  Hm so it is a state machine, but (my hope is that) all state transitions are simple and direct (and observable!) outcomes of user action. If the transitions get at all complex or unobservable, I'll probably call it a failed experiment. It might also end up being the case that users keep types "visible" at all times, only turning them off in certain situations. I can also imagine a flag to "only hide inferred types that are primitives" or something similar.
  - brundolf 4y ago
    Fair enough, and it's certainly an interesting experiment, don't want to discourage experimentation But I will say I think the desire to show the inferred types is orthogonal to the desire to persist them on disk, in the source-of-truth code files. If the state machine really is what you want to experiment with then have fun, but if your desire is just to give the user more visibility into inference, I think there are simpler ways to go about that
4y ago