I came into this book with one fairly straightforward goal for furthering my understanding: how can pushing logic into the types be safer than just getting it right at value-level? Who checks the checkers?
I had heard about vectors keeping their lengths in the type as the prototypical example of dependent types, so was curious how more-advanced logic would be handled. Turns out that there actually isn’t too much calculation going on in types. The most advanced dependent types the book gets into are state machines, which while possibly interesting for certain kinds of low-level programming (imagine programming an elevator such that it can’t open the doors when in-between floors, or something) didn’t seem like they’d add too much to my everyday programming practice unless developed further.
Views are an interesting concept: instead of deconstructing some
value based on the shape of its constructors, we can deconstruct it
based on an additional “view”. The example given is that instead of
separating a list into the first element and the rest of the list, we
can view it as a last element along with the rest of the list.
We can also use recursive views for fancier manipulation: for example,
the splitting step of mergesort can be handled by
SplitRec.
One good little insight is that Lazy and
Inf are the same thing, except for some typechecking
quirks. Relatedly, you only need one function (forever) to
sneak in non-totality to your infinitely-processing programs. Other than
that, everything can be total (and Idris is nice enough to check that
for us, although I’m surprised it’s not the default).
Idris is also a pretty good theorem-proving language, given all its other properties. While it wasn’t as ergonomic as, say, Agda for proving various theorems, it gives you things like reflexivity and congruence, and you can use them mixed in with code that’s otherwise reasonable for doing Real Things like running a webserver or whatever.
This snippet demonstrates what I’m talking about. Refl
is a constructor stating that two types are equal, there’s no way to
have a Refl without the same thing on both sides. We can
then use this in cong. It takes an (implicit) function
f from t to u and a proof that
a equals b, allowing us to prove that applying
a function to each side of a (type) equality doesn’t change the
equality. The definition may look trivial, but that’s because the
typechecker is doing all the work.
data (=) : a -> b -> Type where
Refl : x = x
cong : {f : t -> u} -> (a = b) -> f a = f b
cong Refl = ReflI liked this book and think Idris gets quite a bit right, even if automatic code generation lets programmers ignore much-needed cleanup. Dependent typing still doesn’t seem incredibly useful, but that impression is based on what amounts to a handful of toy examples. I’m sure that given time to develop, dependent typing can eventually become the type of thing you can depend on.