CODEWITHSUNDEEP
haskellcategory-theory
softshipper
softshipper

Reputation: 34099

How to do Left Void?

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?

Upvotes: 2

Views: 188

Answers (2)

dfeuer
dfeuer

Reputation: 48611

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

Upvotes: 11

amalloy
amalloy

Reputation: 92057

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.

Upvotes: 6

Related Questions