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
a, or we have
Nothing. Examples here are in Idris.
It’s important to note here that
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
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:
= 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
(Z = Z) and we provide a proof. However, in the
(S k) case, there is no such proof, so we give back
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
The type signature is the exact same except that we’ve replaced
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.