-
Notifications
You must be signed in to change notification settings - Fork 17.7k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
spec: make(T) compiles even though T has no core type #51470
Comments
This code compilrs but does nothing and cannot be instantiated. That sounds more like something go vet could check in general? Uninstatiatable generics would definitely earn a vet check. |
The latest version of the spec now has a new paragraph in the section on Operands:
This gives both the compiler and the programmer more flexibility. |
Well, that's slightly annoying for some static analyses trying to reason about functions in their generic, uninstantiated form. That's especially true for my IR, which operates on generic functions, and will now have to guard against (and meaningfully translate) operations on empty type sets. I'm also worried about the "flexibility" you say this gives compilers and programmers. What happens if two compiler implementations (or static analysis tools) disagree on which operands may have empty type sets? |
I realize that for the current implementation, the issue isn't nearly as severe as I make it out to be, because the core type computation only ignores methods. That is, most empty type sets don't compile, like the following:
But the way the spec is written, if I am not mistaken, a compiler could accept that code. |
The original intention of the go-nuts thread is to improve the core type definition. The spec says:
and
If the constraint It looks the "flexibility" doesn't address this. |
Maybe the calculation of the core type of a constraint ignores all unspecific elements (method elements and empty interface type elements). |
@dominikh Correct. I am still contemplating whether it should (for 1.19). The idea is that an(y) operation is always permitted on an empty type set: there's no need to bother (or annoy, depending on perspective) with an error because the function cannot be instantiated. This may be helpful when developing code where constraints may be in flux. |
Does this rule allow inconsistency of a specified compiler: package main
func main() {}
type C interface {
map[int]int
M()
}
func foo[T C]() {
var _ = make(T) // okay
}
type C2 interface {
map[int]int;
map[int]bool;
}
func bar[T C2]() {
var _ = make(T) // invalid argument: cannot make T: no core type
} |
@griesemer I feel like that would lead to some pervasive untypedness of empty type sets. Given an interface
I don't really understand the |
My main concern in this area is that I don't want to require a compiler to determine that the type set of a generic function is empty. I suspect that computing that precisely can be rather tricky. And it's completely useless. If that type set is empty, then the function can never be instantiated. It's easy for the compiler to diagnose that the any specific instantiation is impossible. And that will lead the programmer to correct their code. |
I disagree with the premise that it is
In my opinion, one of the strengths of Go's type parameters is that generic functions can be type-checked in their generic form, without having to wait for an instantiation to tell us that the implementation is bad. In other words, Go's generics aren't C++-style templates. Quoting the type parameters proposal:
This strong form of type-checking generic functions also has advantages for tools analysing generic functions. We can report bugs in implementations of generic functions, we can create accurate (possibly type-dependent) summaries without having to look at instantiations, we can even create accurate generic IRs. All of this gets complicated if empty type sets effectively disable type checking. Furthermore, I disagree with the motivation:
This is conflating compiler design and language design. Even if we assume that determining empty type sets is difficult, it doesn't provide immediate justification for reducing the type safety of generic functions. Put differently, "we can't prevent it" isn't the same as "letting users do this is a good idea". That is, I disagree with the following idea:
for the reasons I laid out earlier. IMHO, rejecting ill-formed constraints aids development, it doesn't hinder it. I would rather know that my generic function is broken while I am writing it, not when I try to instantiate it at a later point. You can consider it a limitation of the current compiler that it isn't able to determine all empty type sets, but that shouldn't be called a feature. The current wording of the spec certainly doesn't make this a proper feature:
Instead, it's a per-compiler limitation. Which leads to an obvious problem: different compilers may reject different "subsets" of empty type sets, depending on how strong their reasoning is. I am obviously not advocating for making it a requirement that empty type sets be permitted in all operations, but as long as it is up to the compiler, users will not be able to depend on it in any manner, even during development. Staticcheck, for example, would very likely reject more code than cmd/compile, and people use Staticcheck during development. I am worried that this was a hasty spec change. Are we certain that proving all empty type sets is difficult? It's likely that I am missing some bizarre combination of types, but in my mind, all intersections of types, underlying types and method sets are straightforward to determine. It's impossible to have a type with two different specific or underlying types and we know exactly which methods specific types have. Finally, this breaks a certain monotonicity in the powerfulness of type sets: the more facts we can prove about a type set, the more we can do with it. If we know that it has a method, we can call it. If we know that it's a channel, we can send to it. If we know that it has a field, we can access it (notwithstanding that this is currently disabled.). It seems counter-intuitive that a type set we know nothing about is allowed to do everything (albeit possibly not everything, because we're not always dealing with operands; another inconsistency.) Even if we can't yet agree on how empty type sets should behave, with Go 1.18 around the corner, I'd feel a lot more comfortable if the "implementation restriction" is removed from the specification for now, and this issue is instead considered unresolved, to be revisited in 1.19. |
I agree that this is a compiler implementation restriction, not a language issue as such. And that is what the spec says. There are other compiler implementation restrictions in the spec already. I'm not arguing that an empty type set should eliminate all type checking. I'm arguing that, as an implementation restriction, it's OK if the compiler incorrectly accepts some operations even if the type set happens to be empty. Nothing says that the compiler must accept those operations. It's only permitted to fail to notice that they shouldn't be allowed because there is in fact no type in the (empty) type set that permits them. A compiler is free to not implement that restriction at all. It's fine if a tool like staticcheck can give an error if a type set is empty. There is no inconsistency there. If I write func F[T C](v T) {} and the constraint And I do claim that it can be hard to determine that the type set is empty. type EmptyConstraint interface {
~struct { M int64 }
M() int32
} |
I seem to be arguing with a combination of you and @griesemer, not so much either of you individually. In particular, my reaction was sparked by #51470 (comment), which considers making this intentional, desirable behavior, rather than merely an implementation restriction that occurs sometimes. I combined that with your assertion that I'm fine with an actual implementation restriction, I'm really just arguing against making it part of the language. |
I realize this is an issue about the spec and the compiler, but I am wondering how this manifests for go/types and whether there is a problem for cmd/vet or not. Are functions with empty type sets considered errors according to "go/types"?
|
Should this compile okay: package main
func main() {}
type C interface {
map[int]int
M()
}
var x C // x may not box any value, so it is always nil. Now, it doesn't. |
@go101 No, it should not compile ok. |
FWIW it can be argued that if we can prove that a type set is empty, disabling type checking is entirely correct. Because any statement about "every element of the empty set" is true (ex falso quodlibet). Personally, I have argued (and am still of the opinion) that the correctness of a Go program should never depend (in either direction) on exact calculation of a type set. My intuition (after thinking about it a bunch) is that doing that is at leas tricky, if not NP-complete in general (as @ianlancetaylor mentions above). Basically, constraints are a form of logical formula. The way they work, the form is conjunctive. Calculating the precise type set is determining the solutions to that formula¹. Which is NP complete, for CNF. The current approach of core types provides a heuristic to solve it and the restrictions we put on constraints (e.g. that unions over elements with method sets are disallowed) are to limit the formulas to those for which we have better heuristics. All of which is to say, I agree that it would be nice if we could nail all of this down. But to do so, someone needs to come up with a good way to do so, i.e. an algorithm to do these calculations, which a) doesn't require to solve an NP-complete problem and b) is sufficiently simple to be put into the spec. Without that, my intuition is that we just going to have to live with the restriction that we only have heuristics. i.e. I don't think it's just an implementation restriction. Personally, I'm a bit unhappy that the spec makes correctness definitions based on type sets at all. IMO it should only ever talk about core types (or whatever the heuristic is we end up using). IMO that's the solution to
That is, IMO we should prescribe a specific "strength of reasoning" (e.g. using "core types") and then use that consequently, requiring a compiler to accept any program valid based on that and reject any program invalid based on it.
I don't think we are certain, currently. I proved it for an earlier instance of the design, which might be interesting to look at for the kinds of problems that can appear. But since then, the design has changed a bit - among other things, we disallowed some constraints that I used in the proof. I believe it is possible that the changes made it possible to check if type sets are empty . But I haven't had the time to sit down and think about it. Personally, the problem is sufficiently subtle, that I wouldn't trust intuition either way - until someone either writes a proof that it's hard or writes an algorithm to show how to do it, I wouldn't commit. [1] While type-checking an instantiation is substituting in a solution and see if the formula is true, which is always cheap. |
From a golang-nuts post:
This program compiles without error even though
T
doesn't have a core type (the typeset ofC
is empty).This may require an update to the definition of core types or perhaps some other accommodation in the spec.
The text was updated successfully, but these errors were encountered: