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)
Z = Just Refl
isZeroMaybe S k) = Nothing isZeroMaybe (
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)
Z = Nothing
badIsZeroMaybe S k) = Nothing badIsZeroMaybe (
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)
Z = Yes Refl
isZeroDec S k) = No contradiction isZeroDec (
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
Refl impossible contradiction
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)
Z = No badContradiction
isZeroDec S k) = No contradiction isZeroDec (
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
Refl impossible badContradiction
But the compiler knows that Refl
is valid for
Z = Z
.
Type checking ./IsZero.idr
IsZero.idr:

 badContradiction Refl impossible
 ~~~~~~~~~~
Refl is a valid case badContradiction
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, typelevel 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.