return type inference #10

New Issue

sb10q · 2021-04-30T17:24:28+08:00

sb10q commented

2021-04-30 17:24:28 +08:00

Comments from Lionel Parreaux:

Following Sébastien's talk, there was a question on return-type inference, which at least some people seem to want.

David (who I just tried to add to the recipients of this email, before noticing he's been there the whole time – hi David!) said it wouldn't be hard to do with a work-stealing algorithm. That's correct, you can just yield back whenever you try to use something whose type has not yet been inferred, and bail on unannotated mutually-recursive definitions. But that does come at a certain performance cost. The Scala compiler does a single-threaded version of that and I remember Martin Odersky raising doubts about the performance of putting a multi-threaded infrastructure on top of it. But Scala is a very complicated language with an even more complicated implementation, so a lot of the insight there probably does not translate well to ARTIQ.

In any case, what I was really curious about was the kind of problems that people faced with the old HM-based system. From the presentation, I understood that it was one of the slow parts of the old compiler, and that it apparently did some backtracking (which I inferred from Sébastien's specifically mentioning "no backtracking" as a goal of the new engine). I think none of that is necessarily true of an HM implementation, which can be made extremely fast. We certainly can avoid backtracking if we're careful enough.

As for raising confusing errors to users, I think there's a lot that can be done (efficiently) that could actually make the problem moot. (Note: no need to go all the way to the fine-grained provenance-tracking algorithm I shoed you guys earlier!) Moreover, HM type inference can actually be parallelized in a very straightforward way, as each function's type can be computed separately and then mutual assumptions about other functions' types can be checked in a merge ("reduce") phase after the gist of type inference is done.

The reason I'm raising these questions is not because I am obsessed with type inference on an academic level (although that also happens to be true :^P), but mostly because it could make the transition a lot less painful to users who already have significant code bases written in the old language. I'm still fine with going with a more conservative local type inference approach first, and seeing whether we can make it better later on. But doing so would actually push us into technical and architectural choices which we may not otherwise want to commit to, so we should at least be cognizant of that.

Comments from Lionel Parreaux: > Following Sébastien's talk, there was a question on return-type inference, which at least some people seem to want. > > > David (who I just tried to add to the recipients of this email, before noticing he's been there the whole time – hi David!) said it wouldn't be hard to do with a work-stealing algorithm. That's correct, you can just yield back whenever you try to use something whose type has not yet been inferred, and bail on unannotated mutually-recursive definitions. But that does come at a certain performance cost. The Scala compiler does a single-threaded version of that and I remember Martin Odersky raising doubts about the performance of putting a multi-threaded infrastructure on top of it. But Scala is a very complicated language with an even more complicated implementation, so a lot of the insight there probably does not translate well to ARTIQ. > > >In any case, what I was really curious about was the kind of problems that people faced with the old HM-based system. From the presentation, I understood that it was one of the slow parts of the old compiler, and that it apparently did some backtracking (which I inferred from Sébastien's specifically mentioning "no backtracking" as a goal of the new engine). I think none of that is necessarily true of an HM implementation, which can be made extremely fast. We certainly can avoid backtracking if we're careful enough. > > >As for raising confusing errors to users, I think there's a lot that can be done (efficiently) that could actually make the problem moot. (Note: no need to go all the way to the fine-grained provenance-tracking algorithm I shoed you guys earlier!) Moreover, HM type inference can actually be parallelized in a very straightforward way, as each function's type can be computed separately and then mutual assumptions about other functions' types can be checked in a merge ("reduce") phase after the gist of type inference is done. > > >The reason I'm raising these questions is not because I am obsessed with type inference on an academic level (although that also happens to be true :^P), but mostly because it could make the transition a lot less painful to users who already have significant code bases written in the old language. I'm still fine with going with a more conservative local type inference approach first, and seeing whether we can make it better later on. But doing so would actually push us into technical and architectural choices which we may not otherwise want to commit to, so we should at least be cognizant of that.

Sign in to join this conversation.

No Label

No Milestone

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: M-Labs/nac3-spec#10