-
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
proposal: Go 2: sigma types #52096
Comments
Seems related to the long discussion at #19412. What is the zero value of a switch type? I couldn't see that in a quick read. |
I must have forgotten to include it. The zero value of a switch type is the value having the zero value of the discriminator and the dependent type corresponding to it. This is the reason the discriminator's zero value must appear in the discriminant set. I've updated the proposal to mention this. |
So ', for your example, the zero value of type Sum is Sum{false, struct{}}? |
Correct. Though, to be pedantic, the zero value of Sum is |
This may be an ignorant question, so please excuse me if I just don't fully understand, but: In the "before" version of the Madoka/Homura example, It's unclear to me how the "after" version actually makes those fields accessible. The |
The switch type Sum doesn't have a field named err, but it does have error as a dependent type. To access the error in the "before" variant, one can do |
Are you allowed to define methods on these types? |
I don't know what to believe today, and the anime-themed examples are throwing me off. Just to be clear: This is a serious proposal, despite it being April Fool's? It sure looks like it's serious, minus the examples. |
@zeebo It would be legal to define methods on a named switch type, with the usual semantics. Somewhat related, it would also be legal to define a named switch type with type parameters. E.g., const Just = true
type Maybe[T any] switch bool {
case Just: T
default: struct{}
}
func (m Maybe[T]) String() string {
switch t := m.(case) {
case Just:
return fmt.Sprintf("Just(%v)", t)
default:
return "Nothing"
}
} Perhaps I should add this as an example in the proposal. |
@DeedleFake There is some history to using Madoka and Homura in place of foo and bar. |
More directly, I think this proposal would be a beneficial change for Go's type system, but I don't really think it is a feasible change to make to Go. I originally drafted it a few months ago, fully intending to submit it seriously, but it felt increasingly silly in its scope as I wrote it. So, I would describe this as an April Fools' joke hatched from the shell of a real proposal. Maybe it was hasty to conclude the proposal was too much! To me, it feels like the switch types I've described have just the wrong amount of overlap with interface types. The semantics are similar enough to copy many of the same syntactic elements, but different enough that borrowing those things would mostly be confusing. Perhaps a substantial part of that is the name: I hear "switch type" and immediately think of "type switch." Another awkward part is that interfaces can now have type elements to describe a union of some set of types, although I don't believe there has been a proposal to allow values of such interface types yet. I do think that dependent types are good, and I think it's productive to think about how something like sigma types would fit in Go. I especially feel the lack of sum types quite often in the kinds of code I write, so I think it is productive to think about things like sigma types which would fill those gaps. Hopefully there is some value in this proposal beyond a rather high-effort prank. At the very least, I think it accurately demonstrates the scope of changes that a concrete proposal stemming from #19412 is likely to require. And, for what it's worth, the anime references are just the example names I like to use – they weren't intended to be part of the joke. :) |
Amusingly, in that case, a number of people on the slack commented approvingly about how through and well-considered this proposal was! |
Even if it is intended as a joke, I still think it is interesting. The good point of this "sum type" or union type proposal is that it is a tagged union with an explicitly typed tag, and a well defined zero value. Those are two benefits other similar proposals did not have. Maybe you should reconsider and simplify your proposal to these two points, and then we might get to something that does fit well with Go, and that can be considered seriously. |
Closing as dup of #19813. |
For those who expressed interest in this proposal: I filed #54685 as a serious proposal which refines the ideas here and avoids their most egregious problems. In particular, the name is more reasonable, and it integrates the type element syntax currently used in generic interfaces. |
Author background
Related proposals
Proposal
Introduce a restricted version of sigma types into Go. Formally, sigma types are pairs
(a: T, b: B(a))
wherea
is a value of typeT
andB
is a function that constructs the type ofb
from the value ofa
. Less formally, they can be considered tagged unions where the tag is an accessible value of a type the programmer can select.Sigma types are a central feature of dependent type systems, which make it possible to statically prove many facts about the safety of programs. Such systems allow type metaprogramming, which allows the type constructor
B
to depend on variable values ofa
. Because Go does not have metaprogramming, I propose the restriction thata
must be one of a list of constants. I believe that sigma types will be useful despite that restriction.To avoid an unhelpfully mathematical name, I propose to name these types "switch types." A switch type has a discriminator, which is a variable of any type that can represent constants. It also has a discriminant set, which is a fixed set of constant values of the same type as the discriminator. Each value in the discriminant set maps statically to a dependent type. A value of a switch type has its discriminator equal to one of the values in the discriminant set and a dependent value of the type to which that value maps.
The syntax I propose is as follows. We add a new kind of type literal,
SwitchType
, with the following EBNF:The
Type
followingswitch
specifies the type of the discriminator. Eachcase
gives a list of values of the discriminator and the type corresponding to those values. The values in thecase
clauses must be constants representable by the discriminator type. These form the discriminant set. It is an error to specify the same value multiple times within a switch type definition. Thedefault
clause specifies the type when the discriminator is equal to the zero value; it is an error to both specify the zero value in acase
clause and to use adefault
clause in the same switch type definition. It is additionally an error to specify neither adefault
clause nor the zero value in acase
clause, which is to say that the zero value must appear exactly once in the discriminant set.The zero value of a switch type is the zero value of the discriminator type and the zero value of the dependent type thereof. This is the reason the zero value must appear in the discriminant set.
Switch type literals are composite literals containing zero or one keyed elements. If a keyed element appears, the key must be a constant equal to a member of the discriminant set of the switch type, and the element must be a value of the type to which the switch type maps the key.
In order to inspect the dynamic state of a switch-typed value, we use syntax analogous to the same operations on interface types. These come in two flavors. First, we can use switch assertions, a primary expression:
The expression in a SwitchAssertion must be a constant in the discriminant set of the switch type. Like type assertions on interfaces, switch assertions can be used in contexts expecting one or two values. When there is only one result, the assertion panics if the discriminator is not equal to the expression. When there are two, the first is the zero value of the corresponding dynamic type, and the second is a bool indicating whether the assertion succeeded.
Second, we can use switches that mirror type switches, which I will call discriminator switches:
The expressions in the case clauses in a discriminator switch must each be in the discriminant set of the switch type of the primary expression of the switch switch guard. Analogous to type switches on interfaces, if an assignment appears in the switch guard and all expressions in the case which matches the discriminator appear in the same case of the switch type definition, then the assigned variable has the type to which that case maps; otherwise, it has the switch type.
Lastly, specific to switch types, the special form
x.(switch)
for switch-typedx
evaluates to the current value of the discriminator.Two switch types are identical if their discriminant sets are equal and both map each discriminator value to identical types. Neither the discriminator nor the dependent value of a switch value is addressable. Switch types are comparable when each dependent type of the switch type is comparable (all types which can represent constants are comparable, so the discriminator implicitly is as well) and are equal when their discriminators and dependent values are respectively equal.
A minor syntactic ambiguity arises with this definition of switch types. This occurs where a switch type literal without a type name is written in a statement context. Because Go requires that every literal must be used, the only otherwise valid use of a switch type literal in statement context is, ostensibly, to call a method or perform a channel send on a value of one of the dependent types:
Considering the awkwardness and uselessness of this expression, it is unlikely that it would ever arise in practice. Therefore, the parser assumes a switch statement when encountering the
switch
keyword in statement context. If it is necessary to write such an expression, the workaround is to wrap at least the type in parentheses.The alignment requirement of a switch type is the maximum of the alignments of the discriminator type and all dependent types. No guarantees are made about the maximum size or layout of a switch type; a compiler may choose to put the discriminator first, last, in the middle, or spread across bits of the dependent types' storage, and it may or may not choose to rearrange or share storage for different dependent types.
In order to handle switch types dynamically, reflection requires a new Switch value of reflect.Kind. On reflect.Type, a Discriminants method returns a
map[any]reflect.Type
enumerating the discriminant set as keys and the dependent types to which they map as values. Lastly, a Discriminator method on reflect.Value returns the current value of the discriminator as a reflect.Value. (The existing Elem method returns the dependent value.)Packages go/ast and go/types will need new types to describe switch types.
{madoka: "homura", kyuubei: 9}
or{error: "anime"}
from a single endpoint. This is in addition to the benefits of sum types, such as making applications like parsers much simpler to describe in types.Costs
The text was updated successfully, but these errors were encountered: