[swift-evolution] [Draft] Change @noreturn to unconstructible return type

[Thorsten Seitz]

> Am 07.06.2016 um 23:32 schrieb Michael Peternell via swift-evolution <swift-evolution at swift.org>:
> 
> Ok, one last thing, then I go to sleep for today...
> 
> Basic Definition of a "Type":
> I learned in university that a type is a "set of values".

Yep. And because sets can be empty there is a type with an empty set, the bottom type.

> When a function has a return type of R, it means that it does return a value of type R.

From this follows naturally that a function with return type Never cannot return, because there is no such value in Never's empty set.

> 
> On the other hand, a @noreturn function doesn't return any value, so it doesn't really have a return type. The whole concept of a "bottom type" was made to create a model where every function can be specified as having a return type. This isn't really a useful concept outside of the Haskell language [1].

Actually Haskell does not have an explicit bottom type (which is not needed because there is no subtyping in Haskell) but other languages have like Scala and Ceylon. And Ceylon does very elegant things with its bottom type in conjunction with union types, e.g. discerning in the type system between Iterables statically known to be empty or non-empty. And Ceylon certainly is not an academic language as they have always strived (quite successful IMO) to be a language with easily understandable concepts. For example, they did introduce union and intersection types not for their theoretical power but to make all types representable as normal types of the language, even such types that have been inferred by the type system when dealing with generics, so that error messages from the compiler would be easily understandable. Only later they discovered how useful type unions and intersections are and how natural many things can be solved with them.

> 
> I like the "Basic Definition of a Type": while it does not generalize to non-returning functions,

But it does if you include the empty set.

-Thorsten 


> it includes all functions in the mathematical sense; it includes all functions that are meant to return a value. It includes all functions that terminate and that neither crash nor throw. This "basic definition" is the reason why we have functions at all. We don't have functions in order to build an academic model where we can study denotational semantics [2] in, and that is super-consistent. We have them to calculate things. And we don't calculate values of type `NoReturn` or `Nothing`.


> 
> If I haven't convinced you yet => we'll meet again when casting votes for the proposal (if it will ever go into formal review)
> 
> -Michael
> 
> [1] Yes, someone will find another language where it is useful too, but anyhow, it's not useful for Swift, Java, Obj-C or C++.
> [2] https://en.wikibooks.org/wiki/Haskell/Denotational_semantics
> 
> _______________________________________________
> swift-evolution mailing list
> swift-evolution at swift.org
> https://lists.swift.org/mailman/listinfo/swift-evolution