SE-0215 - Conform Never to Equatable and Hashable

Evolution Proposal Reviews
22

If the initializer or static method takes a Self parameter, conforming would also be safe. This would allow us to support protocols with operators, for example.

23

There is no problem with conformance to protocols that only have instance member requirements as we know the members can never be used. Protocols with static requirements require more care, but could also be synthesized in some cases such as Equatable where an instance of Self must already exist in order to invoke the static member (thus making it uncallable).

Protocols with other static, initializer or associated type requirements should probably manual consideration for conformance. However, as was stated upthread it is only these requirements that should have to be met by Never for a complete conformance. This would reduce the boilerplate burden while still ensuring that thought was given to how Never should fulfill protocol requirements (including semantic requirements) that can actually be used.

1 Like
24

It is a logical error which is easy enough to avoid altogether by not allowing code that attempts to do this to compile. If we synthesize conformances with trapping implementations generic code will end up calling them in ways that are not immediately obvious. I don't object to someone writing a trapping implementation themselves if desired, but I do not think these belong in the language or standard library.

Not that I know of but soundness is entirely besides the point. The point is that as far as I am aware formal type theory says nothing about protocols and conformances (or substitute any other name such as type classes and instances here). The definition of bottom type only involves subtype relationships. This means that type theory does not say that a true bottom type must conform to all protocols (please correct me if I am wrong about this and point me to material where I can learn the details).

If type theory has nothing to say about this then it is an open design decision as to how a bottom type in Swift should relate to them. Just because normal types must conform to a protocol in order to be considered a subtype of an existential does not mean the same must be true for a bottom type. Synthesizing trapping implementations of protocol requirements that may actually be used is introducing a potential landmine for generic code.

5 Likes
25

Downloadable Toolchains Available for this Proposal

We have downloadable toolchains/binaries of Swift that contains an implementation of this proposal available for download:

Follow the instructions on Swift.org for using built Swift binaries/toolchains.

3 Likes
26

What is your evaluation of the proposal?

I do not disapprove of conforming Never to Equatable or Hashable. I think what is outlined in the proposal makes sense. One thing that does have me curious though is if Never not conforming to Equatable and Hashable represents a large enough issue at this time to take on this proposal.

Is the problem being addressed significant enough to warrant a change to Swift?

I feel that I have never seen a specific use cases for this change and I do not know how wide spread the use of Never conforming to Equatable or Hashable could be adopted once the change is made so I have to so no at this time.

Does this proposal fit well with the feel and direction of Swift?

In regards to providing support for Equatable and Hashable I feel that proposal 215 does fit with direction of the language.

If you have used other languages or libraries with a similar feature, how do you feel that this proposal compares to those?

N/A

How much effort did you put into your review? A glance, a quick reading, or an in-depth study?

I read the full proposal, read through the comments on this thread, and also looked for other Never implementations being used in the Swift source now.

27

Not sure it is really worth the trouble.

28

What is your evaluation of the proposal?
+1

Is the problem being addressed significant enough to warrant a change to Swift?
Yes

Does this proposal fit well with the feel and direction of Swift?
I'm not completely sure. Conformance to just these protocols seems fairly reasonable as a minimum but not terribly principled. Short of making never an inhabitant of every type (protocols included), I think that it will always feel arbitrary. Acceptable, but arbitrary.

If you have used other languages or libraries with a similar feature, how do you feel that this proposal compares to those? Never in Haskell is useful but it is an inhabitant of every type.

How much effort did you put into your review? A glance, a quick reading, or an in-depth study?
I've followed the various discussions

1 Like
29

Questions about future plans making Never the bottom type:

Judging by the history, AnyObject was a magical protocol which created a lot of issues has now become a keyword. In That sense Never is an empty enum for now as a reserved type.

  • If we're ever going to make it the bottom type (which I personally would love to see), any chance that we would need to abandon the enum then and make it a keyword like Any, AnyObject etc.?
  • If so, would such extensions like proposed be troublesome to remove from the language in the future?
1 Like
30

Is it an instance of every typeclass? That would be the equivalent of conforming to every protocol.

1 Like
31

Never can be substituted for any generic type A because you can't create instances of it - so you will be forced to deal with optionals to account for values not being occupied. But Never.Type cannot be substituted for any metatype A.Type, because you do have an "instance" of it - Never.self.

32

If you allow substituting Never for any generic type parameter regardless of the constraints on that type then you will have cases where static, initializer and associated type requirements are used by that generic code. in some cases such as == we still have a static proof that the member cannot be used (because using it would require an existing instance of Never). However, that will often not be the case. Deciding how to handle this is one of the most important design decisions involved in making Never a true bottom type IMO.

33

yeah, what I mean is that those all come from the metatype. Once you, say, look up an associated type, you're performing operations meant for an A.Type on Never.Type (which, unlike instances of Never, is a real thing). It's different than just marking a value of type A as uninhabitable.

34

Gotcha, yeah. I think a good way to summarize the design problem is that in order to be a true bottom type Never must be a subtype of all types including existentials of protocols which place requirements on the metatype. The options appear to be:

  1. Make an exception for Never in the subtyping rules for existentials.
  2. Synthesize trapping implementations on Never for all static and initializer requirements of all protocols as well as a type alias equal to Never for all associated type requirements on all protocols.
  3. Don't make Never a true bottom type.

#1 seems like the least bad option to me right now but there could well be edge cases I haven't thought of. #2 is obviously what I am arguing against. :slight_smile:

1 Like
35

It is but I am pretty sure that type classes are a bit more than protocols.

36

Really? What happens when generic code uses mempty?

37

A runtime exception.

38

A few more questions about the future of Never:

  • If Never is a subtype of everything it will technically inherit every possible API?

  • protocol A {
  static var foo: Int { get }
}

protocol B {
  static var foo: Bool { get }
}

Never.foo // how would this collision be resolved?

  • How would autocompletion be affected on Never? If we type Never. in Xcode it will show all public API including colliding API?

  • Shouldn't Never become a keyword like AnyObject so that no one would be able to extend it on it's own?

  • Were these issues considered in regard of extending Never now?

39

No, I'm not well versed in type theory at all, hence the question to the community. However, I am of the understanding that this poses some problems for internal consistency of Swift:

  • In Swift, if C1 is a subtype of C0, then C1 inherits the protocol conformances of C0.
  • If Never is a true bottom type, it is a subtype of all types.
  • Therefore, if a protocol P has at least one non-uninhabited conforming type T, then it follows that (in Swift) Never, being a subtype of T, conforms to P. I suppose Never doesn't need to conform to a protocol P0 with no other conforming types, but I'm not certain how that would interact with private types, for example.

To be clear, my concern is not about Never being the subtype of the protocol existential (which indeed doesn't even conform to the protocol), but about its being a subtype of conforming types, which everywhere in Swift have available the extension methods and non-overridden default implementations of protocols to which they conform.

I don't see a reason why the compiler shouldn't reject any actual attempted initialization of Never at compile time, but if Never doesn't conform to protocols with initializer requirements at all, you're prohibiting useful generic uses that have nothing to do with the initializer or the protocol existential. In other words, I don't think it's a binary choice between avoiding "landmines" and having a true bottom type that follows the same rules as all other subtyping relationships in the language.

1 Like
40

Really? I looked into this and I don't see an instance of Data.Monoid for Data.Void listed here: Data.Void or here Data.Monoid. What am I missing? Where is the instance declared?

41

Ahh, I see what you're getting at. I think the point @beccadax made upthread is relevant here:

This interpretation implies that Never would have all instance members but not all static members. Must a subtype relationship of T: U always imply a subtype relationship T.Type: U.Type? The distinction is subtle but extremely important. I don't believe the notion of "bottom type" requires this to be the case. However, if this is currently always the case then you are right that breaking that relationship for Never would be an inconsistency with the rest of the language. It may still be better than the alternatives.

I'm not suggesting that the compiler should reject all attempts or that Never shouldn't be prohibited from conforming to protocols with initializer requirements. But I am arguing that the compiler and standard library should not provide any trapping initializers for Never. I am also arguing the language and standard library should not provide conformances to protocols with members that may actually be used except where those conformances have received direct human consideration and the conformance is understood to correctly meet the semantic requirements of the protocol.

1 Like