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

31–38 of 38 posts

Re: Type Inference That Sticks

#31

Post by SloopJon »

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…

Although I personally think type inference is the killer feature that makes static typing accessible (almost always auto), I've seen hostility to it, in particular among C++ and C# programmers. The point of this project, as you say, is to be as explicit as possible in the code, while at the same time presenting a view of the code that is less cluttered.

My initial impression is that if I were to use a system like this, I would want any type annotation that differs from the default inference to be visible. The only choice left, then, is when to display redundant annotations, which is where a lot of the disagreement around type inference is, even without this scheme.

Re: Type Inference That Sticks

#32

Post by mpweiher »

layer8 wrote: post #27
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…

> In my IDE...

Sounds great! And very close to what I was thinking about.

What's your IDE?

> The type information is simply “stored” in the plain-text source code itself, as type declarations/annotations.

Yes, I think that's the right way to do it. I do believe that there needs to be some way to tell the difference between these three cases:

1. I put the type information there, that's really what I intended

2. The system put the type information there and I okayed it

3. This is what the system currently thinks, no human interaction

However, I believe this just from thinking about it, without having used such a system, so I may be completely wrong.

My background is also dynamically typed systems like Smalltalk, so the state of having no static type information available is also acceptable.

Re: Type Inference That Sticks

#33

Post by layer8 »

mpweiher wrote: post #32
layer8 wrote: post #27

Earlier quoted context omitted.

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…

> In my IDE... Sounds great! And very close to what I was thinking about. What's your IDE? > The type information is simply “stored” in the plain-text source code itself, as type declarations/annotations. Yes, I think that's the right way to do it. I do believe that there needs to be some way to tell the difference between these three cases: 1. I put the type information there, that's really what I intended 2. The sy…

> What's your IDE?

NetBeans. Since Oracle dropped it to Apache, not a lot of work is done on it anymore, but I still cling to it due to a couple of things that IMO it does better than IntelliJ or Eclipse.

Regarding type inference, I prefer to be able to see the types of all variables right away, in all contexts, and therefore I’m not a fan of inferred variable types. It seems to me that those who favor inferred types mostly want to avoid typing (as in “pressing keys”) and problems with refactoring, as opposed to not wanting the types to be visible at all (because they are mostly fine when IDEs do display them). But I believe that can be adequately addressed by appropriate IDE support for inserting/updating type information in the source code itself.

Re: Type Inference That Sticks

#34

Post by gnulinux »

tel wrote: post #11

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

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

Re: Type Inference That Sticks

#35

Post by jaredly »

dangoor wrote: post #12
jaredly wrote: post #8

Earlier quoted context omitted.

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…

Oh hi kevin! So if there's a possibility that the "extra data" would get out of sync with the "source code" (e.g. via a git merge, or someone just editing the source code as plain text), then it unfortunately breaks the guarantees that this system needs :( I guess I could store a sha of each and fail loudly if I detect that one was edited "outside of the IDE" but again I think that would break the assumptions that git makes about diffs &c. I've tried to go down the "text but nicer" route before, and it always comes up short; so now I'm trying "text is not a supported representation" we'll see how far I get.

Re: Type Inference That Sticks

#36

Post by jaredly »

majewsky wrote: post #18
jaredly wrote: post #8

Earlier quoted context omitted.

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?

So the "repo" in this case is a database, where currently the only things stored are denormalized source tree nodes. I could imagine extending the database to support arbitrary assets, probably also addressed by the hash of their contents (same as top-level language definitions are).

Re: Type Inference That Sticks

#37

Post by dangoor »

jaredly wrote: post #35
dangoor wrote: post #12

Earlier quoted context omitted.

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…

Oh hi kevin! So if there's a possibility that the "extra data" would get out of sync with the "source code" (e.g. via a git merge, or someone just editing the source code as plain text), then it unfortunately breaks the guarantees that this system needs :( I guess I could store a sha of each and fail loudly if I detect that one was edited "outside of the IDE" but again I think that would break the assumptions that gi…

Hey Jared :)

Yeah, good point that text is a potentially fragile approach when combined with git. I think the Squeak Smalltalk folks figured out a way to retrofit git support, so maybe it's possible to go all-in on the representation you want and work out git support later if it seems useful enough.

Re: Type Inference That Sticks

#38

Post by tel »

gnulinux wrote: post #34
tel wrote: post #11

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

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

Sorry, not referring to the whole post wrt Agda, just the vision of interactivity that proof search and tactics give you.
Post reply on HN