> In OCaml for instance, unit corresponds to void.

It makes more sense that Void should be void of values, i.e correspond to the empty set, as it does in Haskell [1]. Does OCaml have no empty type?

[1] https://hackage.haskell.org/package/void-0.6.1/docs/Data-Voi...

▲

aiono 3 days ago | parent [-]

Void in Haskell is not the same thing as `void` in C, C++, Java or similar languages. If you return `Void` in Haskell, you will get a runtime error but `void` returning functions in C-like languages don't fail. It's not a type that doesn't have any value, rather it's a type that has a single value (normal return). Therefore it's more similar to `unit`.

▲

chuckadams 3 days ago | parent [-]

Void having no values means it's impossible to return it or call a function that accepts it, so that would make it a compile-time error as opposed to runtime, no?

▲

aiono 3 days ago | parent [-]

In practice yes, so when you try to execute the function that accepts `Void`, that will error out. But there is no reason to not compile it because it will never actually execute. This may sound unpractical but quite the contrary it's very useful. For instance, it's used to model functions that panics in Rust (https://doc.rust-lang.org/reference/types/never.html). That way you can have a function called `todo` which fails when executed, but keeps the type checker happy until you actually implement it.

	▲	chuckadams 2 days ago \| parent [-]
		Right, it's very useful for lots of reasons, one being that any construct that actually tries to use a Void return value or construct a parameter value will be rejected at compile time. What I am really curious about is whether there's any uses of `absurd :: Void -> a` in the wild. I guess it's a top type for arbitrary functions, though I'm not sure how useful that is in itself...