December 14, 2025
Say you're implementing an interpreter for arithmetical expressions in Haskell. You define the following data type:
data Expr
= Literal Double
| Plus Expr Expr
| Minus Expr Expr
| Times Expr Expr
| Div Expr Expr
Now you and I know that allowing division is a little risky, because your user might attempt to divide by zero at some point, which is totally forbidden. There are plenty of ways to deal with this at evaluation time; typically, you'll wrap the result of the computation in a Maybe or some other type constructor that encodes the fact that an error was encountered.
But say you really want a way to prevent divisions by zero at compile time. Of course you won't know if a value is zero until you've evaluated it, so there's no perfect solution. But you might decide to define another data type which forbids divisions:
data SafeExpr
= SafeLiteral Double
| SafePlus SafeExpr SafeExpr
| SafeMinus SafeExpr SafeExpr
| SafeTimes SafeExpr SafeExpr
This works, and now you don't have to worry about divisions by zero anymore. Even better, you can introduce unsafety in your codebase in a controlled way, by using SafeExpr when you want a strict guarantee that no division by zero will occur, and Expr when you're ok with dealing with division-by-zero errors. For instance, you may make an "unsafe" toggle available to your user. When the toggle is off, your code uses SafeExpr, and when it's on, it uses Expr.
The issue with this is... you now have two data types! This means you have to duplicate code: not only the above data declarations, but also any function that produces or consumes an expression tree will need to be written twice. We don't want that. How can we avoid it?
Some ideas (which I haven't all explored fully, so some might not actually work!) might include:
'Bool/'False), and make sure that the Div constructor never gets used when your type is tagged with 'False.All but the last of those solutions add complexity to your program, if only by requiring the use of compiler extensions. But what if I told you there's a much simpler solution that doesn't add any complexity? No code duplication, no boilerplate, no compiler extensions, no loss of portability!
We'll make use of the type Void, so here's a refresher. If you're familiar with Void, you may skip this section :)
Void (from the module Data.Void) is a very simple type: it has no constructor, and only one destructor absurd :: Void -> a. You may think of it as the empty type, the type that has no values.
Think about how weird the fact that it has no constructor is: though you may use Void in your type signatures, your program will never actually hold a value of type Void!
The destructor is also weird: look at how a is a free type variable --- it may stand for any type you like! Consider, for instance, the type Reason of strings that explain why your ex left you, or the type WorldPeace of IO actions that achieve world peace. With a value v of type Void, all you'd have to do is write main = putStrLn (absurd v :: Reason) >> (absurd v :: WorldPeace) in Main.hs, and get both the reason why your ex left, and world peace, at the same time! The catch, obviously, is that you will never get hold of a value of type Void like v.
(Note that this does not mean we can't achieve world peace! I'm just saying if we can, it's not as easy as that. And we should not be deterred by the fact that it does look very difficult. Regarding your ex, though, you should probably just move on)
In a way, Void is like the reverse (or dual) of (): just like you can't construct a value of Void unless you already essentially have a value of Void, you can't consume a value of (), that is, write a function that has () as an input, unless your function essentially outputs (). So Void is just as trivial as (), but it has that touch of magic that () lacks.
Now we're good to go on with our solution!
Consider the following type class (TFlag stands for "type flag"):
class TFlag b where
whenFlag :: b -> f b -> f ()
Notice how the f type parameter does not have any constraints (except for it being of kind * -> *): it does not need to be a functor or anything of the like. Let's not dwell on the meaning of this class and its method whenFlag, though, before looking at its instances. Actually, there are only two! The two types that implement TFlag are the unit type () and the void type Void.
instance TFlag () where
whenFlag w x = x
instance TFlag Void where
whenFlag w x = absurd w
Both instances are trivial, but each is trivial in a different way. To implement whenFlag, we need to construct a value of type f (). Let's see how it's done in each case:
(), b happens to be () already. So the second argument (which has type f b) actually has type f (), exactly what we need. How lucky! Surely we won't be as lucky in the other instance?Void, the second argument has type f Void, which is indeed not what we need. Again, f is not a functor or anything like that, so we don't have anything to work with it. We need to turn to the first argument w... its type, Void, has nothing to do with f (), but since Void is this magical type, all we need is to apply absurd and we get a value of whatever type we want! Of course this was all just a dream, we never had a value of type Void in the first place.Note: if you allow the use of compiler extensions, the EmptyCase extension allows you to pattern match on Void, by writing:
instance TFlag Void where
whenFlag w x = case w of {}
What whenFlag is doing is basically telling you "give me a proof, or a witness w, that the value x has type f (), and I'll let you use it". This is trivial! But it lets us write code that only works when b is () in contexts when b is Void. Let's see how to use it in practice!
Here's how we can use the TFlag class to implement a type-safe optional type constructor:
data Expr unsafeFlag
= Literal Double
| Plus (Expr unsafeFlag) (Expr unsafeFlag)
| Minus (Expr unsafeFlag) (Expr unsafeFlag)
| Times (Expr unsafeFlag) (Expr unsafeFlag)
| Div unsafeFlag Expr Expr
What's changed?
unsafeFlag. unsafeFlag stands for a type subject to TFlag, that is, it is either () or Void. () stands for a type-level "true" of sorts, and Void stands for a type-level "false" --- you'll see why in a minute.Div has been tagged with unsafeFlag. As a result, it may only be used when unsafeFlag is ()! If it were Void, you wouldn't be able to produce the required argument of type unsafeFlag.How would we write a function that deals with expressions?
Functions that produce expressions are easy to write. Either your function may produce an expression that involves divisions, and you need to be explicit about it by setting unsafeFlag to be ():
divExpr :: Double -> Double -> Expr ()
divExpr x y = Div () (Literal x) (Literal y)
Or it can't, and you can get away with a generic unsafeFlag:
plusExpr :: TFlag unsafeFlag => Double -> Double -> Expr unsafeFlag
plusExpr x y = Plus (Literal x) (Literal y)
Functions that consume expressions are where it gets interesting. Either your function needs the safe version, and you need to be explicit about it by setting unsafeFlag. You can discard the unsafe branch Div by using the magical function absurd:
safeEval :: Expr Void -> Double
safeEval (Literal x) = x
safeEval (Plus x y) = safeEval x + safeEval y
...
safeEval (Div w x y) = absurd w
Or your function is able to deal with the unsafe version, in which case you will need to specify how to deal with the unsafe case. But thanks to the whenFlag method, your code will also work in the safe case:
eval :: TFlag unsafeFlag => Expr unsafeFlag -> Maybe Double
eval (Literal x) = Just x
eval (Plus x y) = (+) <$> eval x <*> eval y
...
eval (Div w x y) = whenFlag w $
if eval y == Just 0.0
then Nothing
else (/) <$> eval x <*> eval y
-- Note that testing equality between floating-point values
-- is generally not a great idea.
-- This here is just for exposition purposes :)
That's it, we've found a way to portably exclude some constructor at compile-time without any boilerplate, and write functions that work with either or both of the versions!