Антон Жилин antonyzhilin at gmail.com
Wed Jun 8 03:46:43 CDT 2016

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

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 at gmail.com>:

> I'll talk about how "bottom" mechanic works there. (I'm not a Haskell
> expert, but I'll at least try ;) )
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-evolution/attachments/20160608/c6cbc936/attachment.html>