[Pitch] Never as a bottom type


(André Videla) #1

Hi Swift-Evolution,

At the end of SE-0102 (https://github.com/apple/swift-evolution/blob/master/proposals/0102-noreturn-bottom-type.md) it is mentioned that the Never type could be used as a universal bottom type but that is currently not the case.

As of today the Never type is used as a return type of `fatalError` and as function which do not return by the virtue of calling `fatalError`.
This allows for very useful behaviours for example:

let anything: Any = …

switch anything {
case let view as UIView: …
case let str as String: …
default: fatalError("we got an unexpected type")
}

But it has its limits, most notably, it cannot be used as an expression

let dunno: Int = fatalError("what should I put here?") // cannot convert value of type 'Never'

It makes sense because Never is not a bottom type. If it were, this statement would be absolutely valid.

Having a bottom type and a value for it has several advantages:

- More informative error messages with forced unwrap:

protocol WonkyAPI {
    func apiCall() -> Int? //this always return an Int, why is it optional?
}

func mycode() {
    let valueFromAPI = apiCall() ?? fatalError("The API used to always return a value, but now it does not!")
    …
}

It sometimes happen that some part of the code uses an optional but in your particular codepath, the optional is always containing a value (for example after an assignment).
As of today, you can write
guard let value = value else { fatalError("something terrible happened") }
for the same effect with a more verbose syntax.

- Use as a hole/placeholder during development
During development it is very likely that you will want to write a piece of functionality but be stuck on an intermediate part of the computation. Assume we have an identifier `undefined` of type `Never` which would represent an impossible value as a bottom type. We would ben able to write:

func transform(point: CGPoint) -> CGPoint {
    let translation = Matrix3D(1, 0, 2,
                                0, 1, -2,
                                0, 0, 1)
    let rotation: Matrix3D = undefined //what was it? I forgot
    return (translation * rotation * point.homogenous).toPoint()
}

We can debate on the right naming for undefined. Haskell uses 'undefined', Scala uses `???`. `unimplemented`, `impossible`, `void`are all valid contenders.

- Eliminate type annotations for generic covariant types
As of today this is not valid

struct Person {
    let name: String
}

var maybeSomeone = nil
maybeSomeone = Person(name: "Doug”)

Even though it is clear that maybeSomeone is of type Optional<Person>.
That is because the compiler cannot guess which type the Optional wraps when `maybeSomeone` is declared. But with a bottom type, a naked nil can be mapped to `Optional<Never>` until the type inference figures out from the context what is the type of Optional. If it cannot because no use or no assignment is done, the compiler could emit an “unreachable” warning just like it does for

func unreach() {
    fatalError("stop here")
    print("not printed”) // warning: will never be executed
}

Should I write a proposal?

André Videla


(Robert Widmann) #2

But it has its limits, most notably, it cannot be used as an expression

let dunno: Int = fatalError("what should I put here?") // cannot convert value of type 'Never'

Though our type lattice doesn’t necessarily have a bottom in the way you’re looking for, you can use Never-returning functions to inhabit a combinator that will do this for you.

func undefined<A>() -> A {
  fatalError("")
}

···

It makes sense because Never is not a bottom type. If it were, this statement would be absolutely valid.

Having a bottom type and a value for it has several advantages:

- More informative error messages with forced unwrap:

protocol WonkyAPI {
    func apiCall() -> Int? //this always return an Int, why is it optional?
}

func mycode() {
    let valueFromAPI = apiCall() ?? fatalError("The API used to always return a value, but now it does not!")
    …
}

It sometimes happen that some part of the code uses an optional but in your particular codepath, the optional is always containing a value (for example after an assignment).
As of today, you can write
guard let value = value else { fatalError("something terrible happened") }
for the same effect with a more verbose syntax.

- Use as a hole/placeholder during development
During development it is very likely that you will want to write a piece of functionality but be stuck on an intermediate part of the computation. Assume we have an identifier `undefined` of type `Never` which would represent an impossible value as a bottom type. We would ben able to write:

func transform(point: CGPoint) -> CGPoint {
    let translation = Matrix3D(1, 0, 2,
                                0, 1, -2,
                                0, 0, 1)
    let rotation: Matrix3D = undefined //what was it? I forgot
    return (translation * rotation * point.homogenous).toPoint()
}

We can debate on the right naming for undefined. Haskell uses 'undefined', Scala uses `???`. `unimplemented`, `impossible`, `void`are all valid contenders.

- Eliminate type annotations for generic covariant types
As of today this is not valid

struct Person {
    let name: String
}

var maybeSomeone = nil
maybeSomeone = Person(name: "Doug”)

Even though it is clear that maybeSomeone is of type Optional<Person>.
That is because the compiler cannot guess which type the Optional wraps when `maybeSomeone` is declared. But with a bottom type, a naked nil can be mapped to `Optional<Never>` until the type inference figures out from the context what is the type of Optional. If it cannot because no use or no assignment is done, the compiler could emit an “unreachable” warning just like it does for

func unreach() {
    fatalError("stop here")
    print("not printed”) // warning: will never be executed
}

Should I write a proposal?

André Videla
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Xiaodi Wu) #3

Clearly many uses for this; would like to see it some day, definitely.
However, IIRC, the last day for any _code_ to be incorporated in Swift 4 is
June 1. There's simply no chance that this can be considered for the
current phase of Swift evolution.

When it does come into scope (which will depend on the core team's
identified priorities), the one thing I would comment is that there is no
need for a name such as "undefined": we already have "fatalError()".

···

On Sun, May 14, 2017 at 17:27 André Videla via swift-evolution < swift-evolution@swift.org> wrote:

Hi Swift-Evolution,

At the end of SE-0102 (
https://github.com/apple/swift-evolution/blob/master/proposals/0102-noreturn-bottom-type.md)
it is mentioned that the Never type could be used as a universal bottom
type but that is currently not the case.

As of today the Never type is used as a return type of `fatalError` and as
function which do not return by the virtue of calling `fatalError`.
This allows for very useful behaviours for example:

let anything: Any = …

switch anything {
case let view as UIView: …
case let str as String: …
default: fatalError("we got an unexpected type")
}

But it has its limits, most notably, it cannot be used as an expression

let dunno: Int = fatalError("what should I put here?") // cannot convert
value of type 'Never'

It makes sense because Never is not a bottom type. If it were, this
statement would be absolutely valid.

Having a bottom type and a value for it has several advantages:

- More informative error messages with forced unwrap:

protocol WonkyAPI {
    func apiCall() -> Int? //this always return an Int, why is it
optional?
}

func mycode() {
    let valueFromAPI = apiCall() ?? fatalError("The API used to always
return a value, but now it does not!")
    …
}

It sometimes happen that some part of the code uses an optional but in
your particular codepath, the optional is always containing a value (for
example after an assignment).
As of today, you can write
guard let value = value else { fatalError("something terrible happened") }
for the same effect with a more verbose syntax.

- Use as a hole/placeholder during development
During development it is very likely that you will want to write a piece
of functionality but be stuck on an intermediate part of the computation.
Assume we have an identifier `undefined` of type `Never` which would
represent an impossible value as a bottom type. We would ben able to write:

func transform(point: CGPoint) -> CGPoint {
    let translation = Matrix3D(1, 0, 2,
                                0, 1, -2,
                                0, 0, 1)
    let rotation: Matrix3D = undefined //what was it? I forgot
    return (translation * rotation * point.homogenous).toPoint()
}

We can debate on the right naming for undefined. Haskell uses 'undefined',
Scala uses `???`. `unimplemented`, `impossible`, `void`are all valid
contenders.

- Eliminate type annotations for generic covariant types
As of today this is not valid

struct Person {
    let name: String
}

var maybeSomeone = nil
maybeSomeone = Person(name: "Doug”)

Even though it is clear that maybeSomeone is of type Optional<Person>.
That is because the compiler cannot guess which type the Optional wraps
when `maybeSomeone` is declared. But with a bottom type, a naked nil can be
mapped to `Optional<Never>` until the type inference figures out from the
context what is the type of Optional. If it cannot because no use or no
assignment is done, the compiler could emit an “unreachable” warning just
like it does for

func unreach() {
    fatalError("stop here")
    print("not printed”) // warning: will never be executed
}

Should I write a proposal?

André Videla
_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(Yuta Koshizawa) #4

Joe also referred to the following model in a thread about Typed Throws.

    () -> () == () throws Never -> ()
    () throws -> () == () throws Error -> ()

https://lists.swift.org/pipermail/swift-evolution/Week-of-Mon-20170213/032267.html

It means `Never` must be a subtype of `Error`. I think it is an
interesting use case of "Never as bottom type".

···

2017-05-15 7:27 GMT+09:00 André Videla via swift-evolution <swift-evolution@swift.org>:

Hi Swift-Evolution,

At the end of SE-0102
(https://github.com/apple/swift-evolution/blob/master/proposals/0102-noreturn-bottom-type.md)
it is mentioned that the Never type could be used as a universal bottom type
but that is currently not the case.

As of today the Never type is used as a return type of `fatalError` and as
function which do not return by the virtue of calling `fatalError`.
This allows for very useful behaviours for example:

let anything: Any = …

switch anything {
case let view as UIView: …
case let str as String: …
default: fatalError("we got an unexpected type")
}

But it has its limits, most notably, it cannot be used as an expression

let dunno: Int = fatalError("what should I put here?") // cannot convert
value of type 'Never'

It makes sense because Never is not a bottom type. If it were, this
statement would be absolutely valid.

Having a bottom type and a value for it has several advantages:

- More informative error messages with forced unwrap:

protocol WonkyAPI {
    func apiCall() -> Int? //this always return an Int, why is it optional?
}

func mycode() {
    let valueFromAPI = apiCall() ?? fatalError("The API used to always
return a value, but now it does not!")
    …
}

It sometimes happen that some part of the code uses an optional but in your
particular codepath, the optional is always containing a value (for example
after an assignment).
As of today, you can write
guard let value = value else { fatalError("something terrible happened") }
for the same effect with a more verbose syntax.

- Use as a hole/placeholder during development
During development it is very likely that you will want to write a piece of
functionality but be stuck on an intermediate part of the computation.
Assume we have an identifier `undefined` of type `Never` which would
represent an impossible value as a bottom type. We would ben able to write:

func transform(point: CGPoint) -> CGPoint {
    let translation = Matrix3D(1, 0, 2,
                                0, 1, -2,
                                0, 0, 1)
    let rotation: Matrix3D = undefined //what was it? I forgot
    return (translation * rotation * point.homogenous).toPoint()
}

We can debate on the right naming for undefined. Haskell uses 'undefined',
Scala uses `???`. `unimplemented`, `impossible`, `void`are all valid
contenders.

- Eliminate type annotations for generic covariant types
As of today this is not valid

struct Person {
    let name: String
}

var maybeSomeone = nil
maybeSomeone = Person(name: "Doug”)

Even though it is clear that maybeSomeone is of type Optional<Person>.
That is because the compiler cannot guess which type the Optional wraps when
`maybeSomeone` is declared. But with a bottom type, a naked nil can be
mapped to `Optional<Never>` until the type inference figures out from the
context what is the type of Optional. If it cannot because no use or no
assignment is done, the compiler could emit an “unreachable” warning just
like it does for

func unreach() {
    fatalError("stop here")
    print("not printed”) // warning: will never be executed
}

Should I write a proposal?

André Videla

_______________________________________________
swift-evolution mailing list
swift-evolution@swift.org
https://lists.swift.org/mailman/listinfo/swift-evolution


(David Waite) #5

If you mean does this currently compile:

let f:Optional<Never> = nil
let g:[Never] = []

then yes. However, “nil” and “[]” in the above are literals, not types or type instances. They only are used to initialize an instance of a type that is ExpressibleByNilLiteral / ExpressibleByArrayLiteral.

If Never becomes a bottom type, a [Never] or Never? hypothetically could be passed into any function which accepts an array or optional of any type because of covariance and value types, but would always be empty/none version of that type. I can’t think of a practical reason to do this, although I admit I’ve never used a language with a bottom type.

-DW

···

On May 14, 2017, at 11:44 PM, André Videla via swift-evolution <swift-evolution@swift.org> wrote:

Joe also referred to the following model in a thread about Typed Throws.

  () -> () == () throws Never -> ()
  () throws -> () == () throws Error -> ()

That makes sense! As a bottom type it would be perfectly fit for this.

On 15 May 2017, at 03:01, Robert Widmann <devteam.codafi@gmail.com> wrote:

Though our type lattice doesn’t necessarily have a bottom in the way you’re looking for, you can use Never-returning functions to inhabit a combinator that will do this for you.

Very useful.
What do you think of [] as [Never], or nil as Optional<Never>. Can the current inference and subtyping rules deal with that?


(André Videla) #6

Joe also referred to the following model in a thread about Typed Throws.

   () -> () == () throws Never -> ()
   () throws -> () == () throws Error -> ()

That makes sense! As a bottom type it would be perfectly fit for this.

Though our type lattice doesn’t necessarily have a bottom in the way you’re looking for, you can use Never-returning functions to inhabit a combinator that will do this for you.

Very useful.
What do you think of [] as [Never], or nil as Optional<Never>. Can the current inference and subtyping rules deal with that?
If it can there are very interesting things to be done in order to help the developper fill up those placeholders. Typically, the compiler could compute the expected type of a placeholder and IDEs could show this to the user. For example alt-click on undefined could display
`func undefined() -> Never. Expected: Int`
(Of course this get horribly complex when the compiler needs to compute the lowest upper bound of an intersection of types)

···

On 15 May 2017, at 03:01, Robert Widmann <devteam.codafi@gmail.com> wrote:

On 15 May 2017, at 02:04, Xiaodi Wu <xiaodi.wu@gmail.com> wrote:

Clearly many uses for this; would like to see it some day, definitely. However, IIRC, the last day for any _code_ to be incorporated in Swift 4 is June 1. There's simply no chance that this can be considered for the current phase of Swift evolution.

Not a problem, I do no think it is necessary to rush out this feature. But I really wanted to see if it is something that other people here consider useful. I am glad to see that it’s the case. What would be a good timing for a proposal on this matter?


(André Videla) #7

If you mean does this currently compile:

let f:Optional<Never> = nil
let g:[Never] = []

Of course it compiles, but it does not if you remove the type annotations.
My point was that, with a bit of work, you could remove those annotations
and still typecheck

If Never becomes a bottom type, a [Never] or Never? hypothetically could

be passed into any function which accepts an array or optional of any type
because of covariance and value types, but would always be empty/none
version of that type. I can’t think of a practical reason to do this
It could be useful to mitigate the absence of GADT in this simple case:

let value: Either<Int, String> = .left(3) // TypeChecks

let value: Either<Int, Never> = .left(3) // TypeChecks

let value = .left(3) // Does not typecheck

The third line could be inferred as the second. And using the property you
are mentioning (passing values with Never types parameters to functions
with covariant argument) you could very simply do

func takeEither(e: Either<Int, String>) { … }

takeEither(.left(3))

···

2017-05-15 8:44 GMT+02:00 David Waite <david@alkaline-solutions.com>:

On May 14, 2017, at 11:44 PM, André Videla via swift-evolution < > swift-evolution@swift.org> wrote:

Joe also referred to the following model in a thread about Typed Throws.

  () -> () == () throws Never -> ()
  () throws -> () == () throws Error -> ()

That makes sense! As a bottom type it would be perfectly fit for this.

On 15 May 2017, at 03:01, Robert Widmann <devteam.codafi@gmail.com> wrote:

Though our type lattice doesn’t necessarily have a bottom in the way
you’re looking for, you can use Never-returning functions to inhabit a
combinator that will do this for you.

Very useful.
What do you think of [] as [Never], or nil as Optional<Never>. Can the
current inference and subtyping rules deal with that?

If you mean does this currently compile:

let f:Optional<Never> = nil
let g:[Never] = []

then yes. However, “nil” and “[]” in the above are literals, not types or
type instances. They only are used to initialize an instance of a type that
is ExpressibleByNilLiteral / ExpressibleByArrayLiteral.

If Never becomes a bottom type, a [Never] or Never? hypothetically could
be passed into any function which accepts an array or optional of any type
because of covariance and value types, but would always be empty/none
version of that type. I can’t think of a practical reason to do this,
although I admit I’ve never used a language with a bottom type.

-DW


Philosophy of Time and Coding