Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Type Inference That Sticks

jaredforsyth.com

Post reply on HN
Print view View original

11–20 of 38 posts

Re: Type Inference That Sticks

#11

Post by tel »

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.

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.

Re: Type Inference That Sticks

#12

Post by dangoor »

jaredly wrote: post #8
rom-antics wrote: post #4

I'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.

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

I 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!

Re: Type Inference That Sticks

#13

Post by brundolf »

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

Re: Type Inference That Sticks

#14

Post by brundolf »

jbandela1 wrote: post #2

I 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).

Lots 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

Re: Type Inference That Sticks

#15

Post by IshKebab »

brundolf wrote: post #14
jbandela1 wrote: post #2

I 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).

Lots 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

Yeah 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!

Re: Type Inference That Sticks

#16

Post by lambdaxymox »

brundolf wrote: post #13

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 go…

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!

Re: Type Inference That Sticks

#17

Post by jaredly »

brundolf wrote: post #13

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 go…

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

Re: Type Inference That Sticks

#18

Post by majewsky »

jaredly wrote: post #8
rom-antics wrote: post #4

I'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.

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

> bypassing git entirely. I imagine I'll do something similar.

So I'm assuming your language will have some sort of custom source code management system? If so, what do you do when a user wants to store a non-code file together with the source code, e.g. how web applications might have CSS files, fonts and image assets in the repo?

Re: Type Inference That Sticks

#20

Post by brundolf »

jaredly wrote: post #17
brundolf wrote: post #13

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 go…

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 hidd…

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

Post reply on HN