Statically Checking for NULL

Lambda the Ultimate has some pretty interesting discussion about compile-time checking for taking the tail of an empty list, which is generalisable to compile-time checking of any partial function (functions which are not defined for their domain, i.e. their input values). Some particularly interesting comments I found in that thread:

  • “I see the empty list as being like null, which Nice has static checking for”. Wow, impressive (probably not impressive from the type theory angle, but particularly impressive from a practical viewpoint: all NullPointerException exceptions detected at compile-time? Cool indeed. Something tells me I should have a closer look at Nice. Maybe for my Ph.D, I can write a type inference engine for Objective-C. Nehhh …
  • [On modifying the tail function to return Maybe [a] instead of just [a]]: “Using Maybe for this is like saying - let’s turn this partial function into a total one by lifting its range to include Nothing. It became total by obtaining permission to return something I have no use of.”
  • “My point is that [the] Hindley-Milner type system is not expressive enough to allow two (or more) consent programmers to state their mutual expectations. As an author of tail function I can’t promise to always return list given non-empty list and expect the compiler to reject all programs that try to call tail on empty list. I suspect it’s possible to stretch Haskell a bit to encode this particular constraint, but as you said, dependent types are way to go for those who seek more static expressiveness.”
  • “In Epigram type checking is decidable, because all functions are total. Conor McBride plans to add general recursion, but its use would be tracked by the system so that types can only depend on terms from the total fragment.”

And of course, the obligatory type wizardry post from Oleg:

  • “I’d like to point out that it is possible in Haskell98 to write non-trivial list-processing programs that are statically assured of never throwing a `null list’ exception. That is, tail and head are guaranteed by the type system to be applied only to non-empty lists. Again, the guarantee is static, and it is available in Haskell98. Because of that guarantee, one may use implementations of head and tail that don’t do any checks. Therefore, it is possible to achieve both safety and efficiency. Please see the second half of the following message:”.
blog comments powered by Disqus