[Draft] Change @noreturn to unconstructible return type


(Anton Zhilin) #1

I'll talk about how "bottom" mechanic works there. (I'm not a Haskell
expert, but I'll at least try :wink: )

Firstly, there is a Void type in standard library, which is exactly what
enum Never {} in Swift is.
Pretty trivial: it is useful as a parameter of higher kinded types, e.g.
Either.

Then, there is bottom. Long story short, each type in Haskell includes an
undefined (bottom, _|_) value. That corresponds to partially defined
functions in set theory.

Example 1: Integer -> Integer function can either return a Z number, or be
undefined at that input (return bottom)
Example 2: () type actually contains two elements: () and _|_
Example 3: Void contains one element: _|_

Bottom value results in an error on most occasions.

What does returning Void mean? In set theory, set of Integer -> Void is
an empty set. In type theory, Integer -> Void can contain a single
element that returns bottom.

Applying that to Swift, we express bottom value by not returning on a
particular input (due to a crash or an infinite loop). We are going to
express bottom type by Never (or aliases). The only way to return bottom
type is as well going to be returning bottom value (in Swift meaning).

There is also such a function in Haskell: absurd :: forall a. Void -> a
Of course, it just returns bottom value of type a. The philosophy of this
is "from false follows anything" or like, "if we are going to crash, then
we can do anything".
Based on this, we can implement conversions from Void to any type in Swift.
It would look like:

func implementContract() -> Int {
    return fatalError("unimplemented")
}

`return` is crucial here.
This is what I suggest to change in the proposal.

- Anton


(Charlie Monroe) #2

I'll talk about how "bottom" mechanic works there. (I'm not a Haskell expert, but I'll at least try :wink: )

Firstly, there is a Void type in standard library, which is exactly what enum Never {} in Swift is.
Pretty trivial: it is useful as a parameter of higher kinded types, e.g. Either.

Not really. Void is a "Unit" type - it's not an empty enum, it's an enum with exactly one value. The set of values for the Void type contains exactly one possible value.

···

On Jun 8, 2016, at 10:28 AM, Антон Жилин via swift-evolution <swift-evolution@swift.org> wrote:

Then, there is bottom. Long story short, each type in Haskell includes an undefined (bottom, _|_) value. That corresponds to partially defined functions in set theory.

Example 1: Integer -> Integer function can either return a Z number, or be undefined at that input (return bottom)
Example 2: () type actually contains two elements: () and _|_
Example 3: Void contains one element: _|_

Bottom value results in an error on most occasions.

What does returning Void mean? In set theory, set of Integer -> Void is an empty set. In type theory, Integer -> Void can contain a single element that returns bottom.

Applying that to Swift, we express bottom value by not returning on a particular input (due to a crash or an infinite loop). We are going to express bottom type by Never (or aliases). The only way to return bottom type is as well going to be returning bottom value (in Swift meaning).

There is also such a function in Haskell: absurd :: forall a. Void -> a
Of course, it just returns bottom value of type a. The philosophy of this is "from false follows anything" or like, "if we are going to crash, then we can do anything".
Based on this, we can implement conversions from Void to any type in Swift. It would look like:

func implementContract() -> Int {
    return fatalError("unimplemented")
}

`return` is crucial here.
This is what I suggest to change in the proposal.

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


(Anton Zhilin) #3

By Void I meant Haskell's Void, or Swift's Never type. Swift's Void is
Haskell's ().

And I had an error there. Integer -> Void contains two elements: a
function that always returns _|_, and an _|_. In Swift, the first case
corresponds to crash while executing function, and second case corresponds
to crash while computing a result of function type.

- Anton

···

2016-06-08 11:28 GMT+03:00 Антон Жилин <antonyzhilin@gmail.com>:

I'll talk about how "bottom" mechanic works there. (I'm not a Haskell
expert, but I'll at least try :wink: )

Firstly, there is a Void type in standard library, which is exactly what
enum Never {} in Swift is.
Pretty trivial: it is useful as a parameter of higher kinded types, e.g.
Either.

Then, there is bottom. Long story short, each type in Haskell includes an
undefined (bottom, _|_) value. That corresponds to partially defined
functions in set theory.

Example 1: Integer -> Integer function can either return a Z number, or
be undefined at that input (return bottom)
Example 2: () type actually contains two elements: () and _|_
Example 3: Void contains one element: _|_

Bottom value results in an error on most occasions.

What does returning Void mean? In set theory, set of Integer -> Void is
an empty set. In type theory, Integer -> Void can contain a single
element that returns bottom.

Applying that to Swift, we express bottom value by not returning on a
particular input (due to a crash or an infinite loop). We are going to
express bottom type by Never (or aliases). The only way to return bottom
type is as well going to be returning bottom value (in Swift meaning).

There is also such a function in Haskell: absurd :: forall a. Void -> a
Of course, it just returns bottom value of type a. The philosophy of this
is "from false follows anything" or like, "if we are going to crash, then
we can do anything".
Based on this, we can implement conversions from Void to any type in
Swift. It would look like:

func implementContract() -> Int {
    return fatalError("unimplemented")
}

`return` is crucial here.
This is what I suggest to change in the proposal.

- Anton