On 7/8/2017 9:32 PM, Meta wrote:
On Sunday, 9 July 2017 at 04:23:15 UTC, Meta wrote:
On Sunday, 9 July 2017 at 02:25:50 UTC, Walter Bright wrote:
(D already has a `void` type, so can't use Haskell's word.)

Just so we are all on the same page, from a type-theory perspective void is a unit type (it has 1 value), not an uninhabited type (it has no values, i.e. Haskell's _|_ (bottom) type).

I read that a Void function in Haskell does not return. Is that incorrect? I'm not sure how Void relates to _|_

  https://en.wikipedia.org/wiki/Bottom_type#In_programming_languages

says Haskell does not support empty (i.e. bottom) types.

A function with a return type of unit means "this function returns no useful information", because the type only has one possible value anyway. A function with a return type of bottom means "this function can never return", because there is no value of type bottom that could be returned. All that can be done is for the function to diverge (throwing an exception, ending the program, looping forever, etc.).

We sort of have this already with `assert(0)`. The compiler knows that no execution can take place after an `assert(0)` is encountered (in other words, it knows that the function diverges). We just don't have a corresponding type to represent this (Rust uses ! but if I remember correctly it's not quite a first class type).

If we wanted to be cute we could use `typeof()` to represent this type as there is no value you can give to typeof such that it returns the bottom type. It also avoids having to come up with some special symbol or name for it.

In C++/D terms, the unit type could be expressed as `enum Unit { unit }` while the bottom type would be `enum Bottom {}` (although only conceptually because in C++/D you can still do `Bottom b;`).

In D, void is used to signify a function doesn't return a value, but it still returns. It also means untyped data, and no initializer.

Reply via email to