2018-08-21-bottom.md 1.8 KB
layout: post title: "One more use for The Dreadful Bottom" date: 2018-08-21 01:13:02
categories: programming
Everyone knows that Haskell's bottom (commonly referred to as undefined) is
responsible for nearly all possible failures (including so-called Hask not being
real category). Still, it is known to be useful sometimes: for example, when you
want to make things compile before you finished coding.
But what if we look at it from propositional point of view? Plugging undefined
somewhere essentially means "hey, i've a got a proof! but i can't show it you :(
so please just believe me and don't look at it.." Indeed, if you don't care
about (and don't inspect) the proof itself and just want to know that
proposition is "true" (in whatever sense), your program won't explode (however,
it may start misbehaving). E.g.
four_is_five : 4 = 5
four_is_five := undefined
divide_by_self : (x : Nat) -> (y : Nat) -> {x = y} -> Nat
divide_by_self _ _ _ := 1
wrong : Nat
wrong := divide_by_self 4 5 four_is_five
Now you might be wondering why would you want to break your program like that. And indeed, in general you probably wouldn't. But what if you're calling some external code to do some dirty jobs for you? It can surely become handy to be able to make compiler assume things that you know to be true, but can't prove inside language. Usual application of such knowledge is to let compiler make optimization, but in the context of dependent type programming it can actually be a matter of being able to use desired interface (more on that later).
That said, there still should be strict distinguishing between total parts of program which can't go wrong and those relying on external promises. And perhaps a few compiler switches to control whether promises should be checked in runtime (slow, but safe) or blindly trusted (optimized).