<div dir="ltr"><div>By Void I meant Haskell's Void, or Swift's Never type. Swift's Void is Haskell's ().<br></div><div><br></div><div>And I had an error there. <span style="font-size:12.8px">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.</span><br></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">- Anton</span></div></div><div class="gmail_extra"><br><div class="gmail_quote">2016-06-08 11:28 GMT+03:00 Антон Жилин <span dir="ltr"><<a href="mailto:antonyzhilin@gmail.com" target="_blank">antonyzhilin@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I'll talk about how "bottom" mechanic works there. (I'm not a Haskell expert, but I'll at least try ;) )<div><br></div><div>Firstly, there is a Void type in standard library, which is exactly what enum Never {} in Swift is.</div><div>Pretty trivial: it is useful as a parameter of higher kinded types, e.g. Either.</div><div><br></div><div>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.</div><div><br></div><div>Example 1: Integer -> Integer function can either return a Z number, or be undefined at that input (return bottom)</div><div>Example 2: () type actually contains two elements: () and _|_</div><div>Example 3: Void contains one element: _|_</div><div><br></div><div>Bottom value results in an error on most occasions.</div><div><br></div><div>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.</div><div><br></div><div>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).</div><div><br></div><div>There is also such a function in Haskell: absurd :: forall a. Void -> a</div><div>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".</div><div>Based on this, we can implement conversions from Void to any type in Swift. It would look like:</div><div><br></div><div>func implementContract() -> Int {</div><div> return fatalError("unimplemented")</div><div>}</div><div><br></div><div>`return` is crucial here.</div><div>This is what I suggest to change in the proposal.</div><div><br></div><div>- Anton</div></div>
</blockquote></div><br></div>