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

21–30 of 38 posts

Re: Type Inference That Sticks

#21

Post by brundolf »

lambdaxymox wrote: post #16
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 in…

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)

Re: Type Inference That Sticks

#22

Post by mpweiher »

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

Re: Type Inference That Sticks

#24

Post by foota »

mpweiher wrote: post #22

This 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 visibl…

An editor can allow seeing types without having them in the code.

Re: Type Inference That Sticks

#25

Post by [deleted] »

mpweiher wrote: post #22

This 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 visibl…

[deleted]

Re: Type Inference That Sticks

#26

Post by jaredly »

brundolf wrote: post #20
jaredly wrote: post #17

Earlier quoted context omitted.

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

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.

Re: Type Inference That Sticks

#27

Post by layer8 »

mpweiher wrote: post #22

This 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 visibl…

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

Re: Type Inference That Sticks

#28

Post by rictic »

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.

This hits on the biggest problem with projectional languages, and why text has dominated: they don't interoperate well with any existing developer tooling.

So the language implementors have to write everything the developer needs: code editor, source control, code review, code browser, etc

You're completely isolated from the wider ecosystem of development, and the benefits so far don't seem worth it. As described here, you save on the reference resolution phase of linking, which is nice, it should be faster and eliminate some classes of error.

The nice part about text as a common format is that it's common. If every language has to implement every tool then it's an N * M problem. When tools can be reused across languages they become N + M.

A user of a projectional language is giving up git, Github, their favorite code editor, and depending on language-specific tooling to replace all of that. And even when the lang-specific tooling is sufficient, it needs to be relearned and recustomized (think all the configuration just in a code editor: prefs, theme, extensions like VIM keybinds and Copilot, etc).

Is the benefit worth the cost?

Re: Type Inference That Sticks

#29

Post by Someone »

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…

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

How much state gets hidden is 100% on the quality of the implementation, isn’t it? There’s nothing that forbids an implementation from dumping that hidden state in whatever form it wants to (as an example, compare C++ diagnostics of different compilers or different versions of a compiler)

> The "algorithm" becomes extremely simple, with almost no intermediate steps.

I don’t see how it can become simple merely be the way things are presented. If you write f(foo,qbar,baz,quux) in a language where overload resolution is complex and the compiler has 20 overloads to pick from, but can’t find a ‘best’ one, it still has to show you what overloads it considered, how it ranked them and why, and which ones were left.

So, if you want type errors to be extremely simple, I think you need a simple language (type-wise)

Re: Type Inference That Sticks

#30

Post by brundolf »

jaredly wrote: post #26
brundolf wrote: post #20

Earlier quoted context omitted.

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

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

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

Post reply on HN