I am trying to understand https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Void.html and having the following example:
let x :: Either Void Int; x = Left Void
The code does not get compiled. How to make it run?
2 Answers
The point of the Void type is that it has no inhabitants (other than "bottom" values like exceptions and infinite loops). You could write
x, y, z :: Either Void Int
x = undefined
y = Left $ error "Whoops"
z = Left $ let q = q in q
but all of these violate the essential concept of Void.
The only "legitimate" values of type Either Void Int are of the form Right i, where i :: Int.
Indeed, you can write the following:
unEither :: Either Void a -> a
unEither (Left v) = absurd v
unEither (Right a) = a
Since it is impossible to ever create a value of type Void, every value of type Either Void Int must have a Right constructor (or else a bottom in its Left constructor, which is not very useful). e.g., Right 1 would be a valid value of this type.
Related