[Haskell-cafe] Re: Debugging partial functions by the rules

[oleg at pobox.com]

It must be stressed that the advocated technique for avoiding partial
function errors requires *NO* research advances, *NO* dependent types,
*NO* annotations, and *NO* tools. Everything is possible in Haskell as
it is -- actually, even in Haskell98. As a matter of fact, exactly the
same approach applies to OCaml (and even to any language with a
half-decent type system, including Java and C++). The only required
advancement is in our thinking and programming style.

First, regarding fromJust: to quote Nancy Reagan, let's `Just say
NO'. Let us assume that `fromJust' just does not exist. That does not
reduce any expressiveness, as `maybe' always suffices. The latter
function causes us to think of the boundary case, when the value is
Nothing. And if we are absolutely positive that the value is (Just x),
we can always write
	maybe (assert False undefined) id v
This is *exactly* equivalent to `fromJust v', only with a better error
message. So, no `safeFromJust' is ever necessary! The expression above
takes longer to type than `fromJust v' -- and I consider that a
feature. Whenever I am telling the compiler that I know better, I'd
rather had to type it in more words -- so I could think meanwhile if
I indeed know better. Also, such phrases should stand out in the code.
I'd be quite happy seeing fromJust removed from the standard
libraries, or at least tagged `deprecated' or with the stigma
attached that is rightfully accorded to unsafePerformIO.

Regarding head and tail. Here's the 0th approximation of the advocated
approach:

> {-# Haskell98! #-}
> -- Safe list functions
>
> module NList (FullList,
>               fromFL,
>               indeedFL,
>               decon,
>               head,
>               tail,
>               Listable (..)
>               ) where
>
> import Prelude hiding (head, tail)
>
> newtype FullList a = FullList [a]  -- data constructor is not exported!
>
> fromFL (FullList x) = x                 -- Injection into general lists
>
> -- The following is an analogue of `maybe'
> indeedFL :: [a] -> w -> (FullList a -> w) -> w
> indeedFL x on_empty on_full 
>     | null x = on_empty
>     | otherwise = on_full $ FullList x
>
> -- A possible alternative, with an extra Maybe tagging
> -- indeedFL :: [a] -> Maybe (FullList a)
>
> -- A more direct analogue of `maybe', for lists
> decon :: [a] -> w -> (a -> [a] -> w) -> w
> decon []    on_empty on_full = on_empty
> decon (h:t) on_empty on_full = on_full h t
>
>
> -- The following are _total_ functions
> -- They are guaranteed to be safe, and so we could have used
> -- unsafeHead# and unsafeTail# if GHC provides though...
>
> head :: FullList a -> a
> head (FullList (x:_)) = x
>
> tail :: FullList a -> [a]
> tail (FullList (_:x)) = x
>
> -- Mapping over a non-empty list gives a non-empty list
> instance Functor FullList where
>     fmap f (FullList x) = FullList $ map f x
>

> -- Adding something to a general list surely gives a non-empty list
> infixr 5 !:
>
> class Listable l where
>     (!:) :: a -> l a -> FullList a
>
> instance Listable [] where
>     (!:) h t = FullList (h:t)
>
> instance Listable FullList where
>     (!:) h (FullList t) = FullList (h:t)


Now we can write

> import NList
> import Prelude hiding (head, tail)
> safe_reverse l = loop l [] 
>     where
>         loop l accum = indeedFL l accum $
>                        (\l -> loop (tail l) (head l : accum))
>
> test1 = safe_reverse [1,2,3]

As we can see, the null test is algorithmic. After we've done it, head
and tail no longer need to check for null list. Those head and tail
functions are total. Thus we achieve both safety and performance.

We can also write

> -- Again, we are statically assured of no head [] error!
> test2 = head $ 1 !: 2 !: 3 !: []

This would look better had `[1,2,3]' been a rebindable syntax similar to
`do'.

I should point to
  http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html 
for further, more complex examples. We can also use the approach to
ensure various control properties, e.g., the yield property: a thread may
not invoke `yield' while holding a lock. We can assure this property
both for recursive and non-recursive locks.

If there is a surprise in this, it is in the triviality of
approach. One can't help but wonder why don't we program in this
style.

Simon Peyton-Jones wrote:

> My programs have invariants that I can't always express in
> a way that the type system can understand. E.g. I know that a variable is in
> scope, so searching for it in an environment can't fail:
>         head [ v | (n,v) <- env, n==target ]

In the 0th approximation, the above line will read as

     indeedFL [ v | (n,v) <- env, n==target ] (assert False undefined) head

Alternatively, one may write
     case [ v | (n,v) <- env, n==target ] of (h:_) -> h

with the compiler issuing a warning over the incomplete match and 
prompting us to consider the empty list case (writing assert False
undefined if we are sure it can't happen).

I have a hunch we can do better and really express our knowledge that
[ v | (n,v) <- env, n==target ] can't be empty. We don't ask the type
system to decide this for us; we only ask the type system to carry
along our decisions (and complain if we seem to be contradicting
ourselves). To test if we indeed can do better, I'd like to see the
above line in a larger context (with more code).

Incidentally, this is an open invitation. If someone has a (complex)
example with head/tail/readArray etc. partial functions and is
interested in possibly improving static assurances of that code,
Chung-chieh Shan and I would be quite interested in looking into
it. The code can be either posted here or mailed to us privately.