Maybe vs. Dec

If you’ve seen algebraic types at all, you’ve probably run into Maybe. It provides an optional over any other type a—either we have Just an a, or we have Nothing. Examples here are in Idris.

data Maybe : (a : Type) -> Type where
  Nothing : Maybe a
  Just : (x : a) -> Maybe a

It’s important to note here that Just and Nothing are constructors of values. If we see the type Maybe a somewhere, we have no information about whether we’re going to get a Just value or a Nothing value.

There are ways to move this kind of thing from values into types. For example, Idris provides the decidability type Dec which takes either a proof or contradiction type, and provides information in the type about which branch was taken. It looks like this:

data Dec : Type -> Type where
  Yes : (prf : prop) -> Dec prop
  No : (contra : prop -> Void) -> Dec prop

data Dec : Type -> Type where means that Dec is a type that takes another type (it’s a dependent type, since its constructors depend on what the other type passed in happened to be). In the Yes case, we take a proof of type prop which allows us to make the new Dec prop type, basically encoding decidability of a proposition. Alternatively, in the No case, we get a contradiction of prop -> Void, which we can loosely read as an implication that a proposition leads to invalidity.

As a contrast to Maybe, note that Dec handles more at the type level. The proofs it takes are present in types whereas Maybe is dealing with values. This means it’s now harder for the programmer to “cheat”, which is a good thing when we’re going off in search of correct programs!

For example, say we’re writing a function to detect whether a natural number is zero and provide a proof if so. Fascinating stuff, I know. A Maybe-based implementation might look like this:

isZeroMaybe : (n: Nat) -> Maybe (n = Z)
isZeroMaybe Z = Just Refl
isZeroMaybe (S k) = Nothing

The = in the type signature’s (n = z) comes from

data (=) : a -> b -> Type where
   Refl : x = x

Basically, two things can be proven to be equal if, reflexively, the two things are the same thing. In the Z case of isZeroMaybe, we can construct Refl since (Z = Z) and we provide a proof. However, in the (S k) case, there is no such proof, so we give back Nothing.

Watch out though! What’s stopping us from writing this instead, accidentally returning Nothing all the time?

badIsZeroMaybe : (n: Nat) -> Maybe (n = Z)
badIsZeroMaybe Z = Nothing
badIsZeroMaybe (S k) = Nothing

The answer is “not much”. This code compiles just fine, although the logic behind it doesn’t make sense. We want this to not compile, because we shouldn’t have to worry about making silly mistakes like this. What we can do is use Dec instead.

isZeroDec : (n: Nat) -> Dec (n = Z)
isZeroDec Z = Yes Refl
isZeroDec (S k) = No contradiction

The type signature is the exact same except that we’ve replaced Maybe with Dec. In the Yes case, we can pass back our reflexivity proof in the exact same way. However, the No case now requires that we provide something called contradiction. Our contradiction could look like this:

contradiction : (S k = Z) -> Void
contradiction Refl impossible

We now have a proof that zero equals zero and a proof by contradiction that other numbers do not equal zero. What if we were to attempt to make the same mistake as before?

isZeroDec : (n: Nat) -> Dec (n = Z)
isZeroDec Z = No badContradiction
isZeroDec (S k) = No contradiction

We’re now left with the impossible task of proving that zero does not equal itself. This is completely futile—the compiler will reject all such attempts. We can get as far as this:

badContradiction : (Z = Z) -> Void
badContradiction Refl impossible

But the compiler knows that Refl is valid for Z = Z.

Type checking ./IsZero.idr
IsZero.idr:
   |
   | badContradiction Refl impossible
   |                       ~~~~~~~~~~
badContradiction Refl is a valid case

As you can see, while Maybe is nice to use, Dec provides a stronger boundary—it’s not even possible to run functions that require a proof if you don’t have a proof. However, Maybe is easier to pipe through to any function. Although any total function taking a maybe has to deal with the Nothing case, sometimes that kind of flexibility is what we want.

In general, type-level programming feels to me like a way to get much stronger, although somewhat more rigid constraints. In this case, types dependent on having a proof provide much stronger protection for the “pure core” of your programs, rendering them literally unrunnable without proofs. The tradeoff here is in some amount of flexibility, extra verbosity, and ease of handling values as they come. I expect that as we see dependent types continue to become somewhat more mainstream, the ease of use will continue to be improved, especially the automaticity of finding such proofs during the process of programming.