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.
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:
The =
in the type signature’s (n = z)
comes from
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.
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:
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:
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.