Can `Never` be extended to mark parameters, stored properties etc. as not existing?

Evolution Discussion
1

With this discussion thread I would like to discuss one idea about the possible behaviors when using Never. I'm not a compiler developer and have really limited knowledge so please bear with me.

As for today the compiler is smart enough to undestand a function that returns Never when called will trap (fatalError), as that function really never returns. It is also able to make enum cases with a single associated value unavailable this way (e.g. Result<_, Never>.failure).

  • Would it be possible to make stored Never properties be unavailable as well?

If the user happens to call them, well the application will trap just like with a fatalError or a computed Never property.

Since Never has literally no value and is impossible to be instantiated, we will run into a small issue when we would want to initialize a type with stored Never properties. To solve this puzzle here's the follow up question:

  • Would it be possible to make Never parameters be omittable?

Here are a few snippets that shows this in action:

struct S<Result, PartialResult> {
  var result: Result
  var partialResult: PartialResult

  init(result: Result, partialResult: PartialResult) { … }
}

// today
S<Int, Never>(result: 42, partialResult: fatalError())
                          ^~~~~~~~~~~~~ required 😕
// new
// `partialResult` can be omitted as it's `Never`
// `result` is initialized with 42, `partialResult` is not initialized
let s = S<Int, Never>(result: 42)

s.result // 42
s.partialResult // traps like `fatalError`

func someFunction(_: Never) { print("swift is great") }

// today
someFunction(fatalError()) // can never be called and it will trap

// new
// `Never` parameter omitted 
// prints "swift is great"
someFunction()

enum E<Context> {
  case something(value: Int, context: Context)
  ...
}

// today
let e1 = E<Never>.something(value: 42, context: fatalError()) // will trap

// pattern matching
if case .something(let value, _) = e1 { ... } // not possible, will trap

// new
// successfully instantiates a new value of type `E`
// `context` associated value does not exist
let e2 = E<Never>.something(value: 42)

// pattern matching can be extended as well
// `context` associated value can be omitted
if case .something(let value) = e2 { ... }

Would that be actually possible? I think this could be a very useful feature and it would make strange workaround that use a single value type like Void fade away and make such structures and functions more ergonomic.

2 Likes
2

There's a very intriguing example from @Joe_Groff in regards to typed throws and Never. Basically every function and accessor always has an Error type it throws, but the omission of such basically means that it throws Never.

With that spirit, could we potentially generalized function parameters with variadic packs and the idea from the original post?

// straw man syntax
func f<T..., F, R>(T...) throws F -> R where F: Error

f() // (Never) throws Never -> Void

Each function would always have at least one parameter. The omission of such basically means that its single parameter is Never.

However I hope that this particular extension, isn't too far fetched.

In my mind this also seems to provide a good explanation to what a generic type with variadic generic type parameter could mean when it's empty. It will basically also be Never as a single type parameter.

Borrowing the following example from the variadic packs thread:

Here's why I personally imagine we could eventually achieve:

// today
typealias Void = () // empty tuple as type

// purely hypothetical 
typealias Void = Tuple<>
typealias Void = Tuple<Never> // the pack is not existing as it's `Never`

One of the missing puzzles in the area of variadic packs is the missing ability to add labels to each pack element, within the value pack and the generic type parameter list pack.

All this means that Never would be extended in many more corners of the language, but it seems to me that it would enable lots of ergonomics when writing generic code with it.

3

I think that if stored property has type Never, it should not be allowed to be called at compile-time, not produce fatalError at runtime.

2 Likes
4

It would be no different statically when you call into fatalError manually. Depending on the code, if that property is never algorithmically accessed there won't be any runtime traps. Such a hypothetical extension could provide such statical guarantees though, which is what this thread all about. :)

I'm not a compiler developer, so I don't know how groundbreaking this all is or would be. I'm keen to read what John is going to share with us though.

5

You’ve already noticed that this isn’t how the type algebra works out — products of uninhabited types should be uninhabited, not just silently drop the member / parameter / whatever. Singleton types like Void are the multiplicative identity, not empty types like Never. This is trying to make Never into something quite odd and foundationally wrong.

If I substitute Void for Never in your post, it becomes much more reasonable. Implicitly defaulting Void parameters is an interesting idea, although I definitely worry about that having a lot of unintended effects. At a minimum, we’d need to not “volunteer” that in the type-checker; it seems really bad if a user forgetting an argument could lead to everything just silently type-checking by way of inferring that a type argument was Void.

19 Likes
6

Thank you for shining some technical light on these ideas John.

Defaulting to Void feels a bit strange to me. :thinking: My mental model goes more like this:

  • Never - does not have a value, not existing, unavailable, not reachable, uninhabited
  • Void - has a single (singleton) value, nothing (that can be returned without a trap)
  • Optional<T> - an Either like type where nil aka case none is a returnable value that equals "T is currently not stored" (this could be typealias Optional<T> = Either<T, Void> but it would be a bit less fluent to use)

The whole point was that the compiler would permit the omission of a parameter when it's statically known to be of type Never, very similar to what Joe said about non throwing functions, they could in theory be implicitly expressed as something like throws Never. In that sense if a particular function parameter is known to be of type Never it can be safely statically be omitted. Sure if the generic function then tries to call it, it will trap, but that's all reasonable and intentional, I would say.

If the above was actually possible then it seems trivial to extend it further and introduce uninhabited stored properties:

struct Single<Value> {
  let value: Value
  init(value: Value) { self.value = value }
}

typealias Empty = Single<Never>

// new
// `value` from the `init` can be omitted
// `value` stored property is uninhabited as it results into `Never`
let empty = Empty() 

empty.value // possible to call, but it will trap as it's `Never` and uninhabited
7

One very strange possible effect of this would apply to enum case. Today it's not possible to declare case something() as enum cases with associated values require a single value. This should stay and in case of Result<..., Never>.failure() shouldn't be permitted either, otherwise this would defeat the whole purpose of it.

Another example are all current ***[Throwing]*** types the we keep introducing. Those are really just duplicates because we want to express the non-throwingness with the current lack of precise errors which could be propagated through a generic type parameter. All that wouldn't be needed with Never and types throws.

In the same spirit the original example of S<Result, PartialResult> is trying to merge two types (one that has contains a partial result and one that doesn't) into a single one to enable a more generic use of it.

Similarly if function parameters were modeled as labeled variadic packs of 0 to n elements, then the whole pack could evaluate to Never when it supposed to be 0 and therefore the parameter list would default to func name(Never) ... which can be simply written as func name(). Yes this would also ultimately permit us to write name(fatalError()), but this discussion isn't about the usefulness of that tiny possibility.

// straw man syntax
pack T... = Never | {T1, T2, ... Tn}

If all of these ideas are too much non-sense then it's okay. At least I brought this topic up for consideration and to gather some feedback. :slightly_smiling_face:

8

Structs and tuples are so-called "product" types. Enums are "sum" types. That is:

struct Product {
  var a: Int8
  var b: Int8
}

enum Sum {
  case a(Int8)
  case b(Int8)
}

Here, Product can take on 256 x 256 = 65,536 possible values. For each value of a , there's 256 possible values of b. However, Sum can take on 256 + 256 = 512 different values. All possible as plus all possible bs.

If you substitute inn Never for one of these, the sum types becomes just the other case, but the product types becomes the empty type. 256 + 0 = 256, but 256 x 0 = 0.

Edit: Fixed number typos

12 Likes
9

That is a very interesting way on explaining it. Thank you.

@Ian_Keen actually presented an interesting solution using optionals.

struct S<A, B> {
  private var _a: A?
  private var _b: B?

  var a: A { _a! }
  var b: B { _b! }
}
extension S where B == Never {
  init(a: A) {
    self.init(_a: a, _b: nil)
  }
}

let s = S<Int, Never>(a: 42)
s.a // 42
s.b // traps

So it's not technically impossible to pull off. You could even use IUOs for this.

Is there a reason why product types can't be partially uninhabited though?

A somewhat bizarre idea would be treating the omitted Never parameter implicitly as Never! and assigning nil to it (e.g. foo(_ param: Never) becomes foo(_ param: Never! = nil) and permits to call it as foo()). Same could implicitly apply to Never as stored properties.

func foo<T>(_ t: T!) {
  print(type(of: T.self)) // Never.Type
  t as T // expected Fatal error: Unexpectedly found nil while implicitly unwrapping an Optional value
}
foo(Never?.none)
10

This is isomorphic to implicitly turning Never into Void, and I think it’s unclear why you’d want to do this instead of just using Void. Multiplicative and additive identities are different, and so are Void and Never; I don’t agree with the premise that conflating them would be “more ergonomic”.

In the algebraic interpretation of types that @sveinhal alluded to above, Optional<T> is equivalent to T + 1. Since Never is 0, Optional<Never> is 1 and thus isomorphic to Void.

Similarly, Bool has 2 values, and Optional<Void> (or Optional<Optional<Never>>) is isomorphic to Bool. If you’ve used generics enough to make suggestions like this, you’ve probably hit cases where a generic T? starts looking like a simple predicate when T is Void, and the algebraic interpretation shows that there’s a fundamental truth to this.

Nevertheless, Swift doesn’t implicitly convert Void? to Bool, which would be a smaller change than converting Never (0) to Never! (1).

9 Likes
11

"Uninhabited" in this sense should not be understood like a nil/empty value. We're talking about uninhabited types, which means the set of possible values of that type is the empty set.

So if a type can be "partially uninhabited", it is not uninhabited. You've just imposed a constraint that one field always has a single value, meaning it carries no useful information. In that case, you're looking for the unit type, Void, as others have mentioned.

4 Likes
12

Thank you for these great additional details you just shared. Again I don't have much experience in compiler development or the pure type theory so I might talk lots of nonsense here. I'm for sure straight ignore all these fine details.

Let me change the original example a tiny bit into an enum with several different associated types:

enum Transfer<Result, PartialResult, Failure: Error> {
  case progress(Double, partialResult: PartialResult)
  case result(Result)
  case failure(Failure)
}

If we were able to omit a stored property initialization or an init / function parameter that is of type Never then the type Transfer<Int, Never, Never> can produce a .progress(0.5) case and successfully pattern match as such by also omitting partialResult associated value as it's statically known to be of type Never. This type can also not have the failure case as we're already used to and expecting.

On the flip side using Transfer<Result, Void, Never> is a bit strange as partialResult now has a single value. It's somewhat useless and during pattern matching it cannot be fully omitted as "non existing", which is what I would have thought Never could potentially be used for.

When PartialResult == Never it can not have any value, compared to Void where it has a single value. However it's impossible to instantiate such a type due to the inability to "omit" Never parameters.

To put this a bit differently, I'm more or less asking if the compiler could treat a type like Transfer<Int, Never, Never> as following:

enum Transfer<Result> {
  case progress(Double)
  case result(Result)
}

If you happen to access the partialResult explicitly, the program will trap as you're trying to access an entity of type Never.

13

Let's start over differently just with stored properties:

struct S1 {
  let never: Never // allow pseudo stored `Never` constant 

  // de-sugare it to
  var never: Never { fatalError() }

  init() {}
}

let s1 = S1() // would compile
s1.never // would trap

struct S2 {
  var never: Never // allow pseudo stored `Never` variable 
  // de-sugare it to
  var never: Never { get { fatalError() } set {} }

  let number: Int
  init() {
    self.number = 42 // fully initialized 
  }
}

let s2 = S2()
s2.number // 42
s2.never // trap

In other words, allow the omission of the need to initialize a Never property. A Never stored property could be automatically converted into a computed property wrapping fatalError().

  • Then we can extend the omission of Never parameters, possibly by converting from Never to @autoclosure () -> Never and implicitly passing and capturing fatalError().
  • And we can also treat enum's associated values which are Never similar to computed Never properties.

Generically this will fall out very naturally in the end.

So technically all that can be pure syntactic sugar, probably without breaking all the type theory laws. :thinking:

14

[citation needed]

7 Likes
15

I think other folks have given good reasons why you wouldn’t want to do this from a type system perspective, but I think there’s good practical reasons to not do this as well. With the current meaning of Never, your proposed Transfer<Int, Never, Never> expresses a version of the type which does not have partial progress or failure states. I.e. the only valid value is Transfer.result(Int). That’s a very useful thing to express! The property of “values of Never do not exist” is what allows Joe’s suggestion of treating non-throwing types as implicitly throwing Never to work as a formalism.

Further, if we admitted product types with some sort of lazy-fail Never like you’re suggesting, it would become much more difficult to work with them without risking crashing your entire program. Today, if I pass a Transfer<Int, Never, Never> to a function that operates on it generically, I don’t have to worry about what happens in the partial result or failure cases because I know those cases will not exist. If they were permitted to exist and error at runtime, I would have to be very sure that any function I pass my Transfer value to won’t try to access the booby-trapped cases. And even worse, I have to be sure that the function I’m passing it to will never be updated to do so. That seems like a pretty big loss in terms of predictability about crashes.

I know others have already said it, but it really seems like what you want here is Void which can exist but is an entirely useless value. The ergonomic difficulties are something that are conceivably solvable, as John notes, by perhaps allowing the implicit omission of Void values in various places. But using Never for this purpose loses us many desirable properties from a type system perspective that make it easier to reason about code interacting with Never.

10 Likes
16

Those are very good points and this feedback is very valuable for me and everyone reading along or in the future.

I mean if this discussion could have sparked the desire to add more ergonomics to Void as a parameter or a stored property, that might be a good enough solution in the end.

17

Haha :nerd_face:

Hopefully, the point got through.

4 Likes
18

what? no explanation of exponentiation? :grinning:

19

If I understand the proposal correctly, what you want is to avoid dealing with generic properties whose specialized type happens to be "something that is not there". I can understand the need, but maybe you misunderstand what's the point of Never and Void.

A minimal example would be the following:

/// You're requesting something like this

struct Product<A, B> {
  var a: A
  var b: B
}

typealias MyProduct = Product<Int, Never>

let x = MyProduct(a: 42) // `b` is omitted because `Never`.

_ = x.a // ok
_ = x.b // traps

Putting aside the fact that a type system feature that can easily produce trapping code is probably a bad idea in itself, what you're expressing with MyProduct(a: 42) is "create an instance of MyProduct whose a value is 42 and b value is a default one", in fact it has the exact same syntax as a regular initializer with a default value associated to a parameter.

What you want is a default value, not "no value": but the initializer must be able to "pluck the default value out of thin air" and this is exactly the purpose of Void.Void has single instance () that can always be produced no matter what, out of thin air.

The case is different with an enum:

enum Sum<A, B> {
  case a(A)
  case b(B)
}

typealias MySum = Sum<Int, Never>

let x = MySum.b(???) /// cannot be produced, it makes no sense

In fact, the post you mentioned from @Joe_Groff talks about throws, which is modeled with a sum type.

A function like

func foo() throws -> Int

is isomorphic to

func foo() -> Result<Int, Error>

in the same way a function like

func bar() -> Int

is isomorphic to

func bar() -> Result<Int, Never>

While throws is great and I use it all the time, I think it's still important to understand the underlying type algebra.

3 Likes
20

Perhaps I'm misinterpreting that sentence, but “a function that returns Never when called will trap” is false.

A function that returns Never never returns a value, and if it isn't declared throwing, it never returns at all. But that doesn't mean it traps. Consider dispatchMain for example. It doesn't return, doesn't throw, and doesn't trap.

10 Likes