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

[oleg at pobox.com]

Jan-Willem Maessen wrote:
> In addition, we have this rather nice assembly of functions which  
> work on ordinary lists.  Sadly, rewriting them all to also work on  
> NonEmptyList or MySpecialInvariantList is a nontrivial task.

That's an excellent question. Indeed, let us assume we have a function
	foo:: [a] -> [a]
(whose code, if available, we'd rather not change) and we want to
write something like
	\l -> [head l, head (foo l)]

To use the safe `head' from NList.hs , we should write
	\l -> indeedFL l onempty (\l -> [head l, head (foo l)])

But that doesn't type: first of all, foo applies to [a] rather than
FullList a, and second, the result of foo is not FullList a, required
by our |head|. The first problem is easy to solve: we can always
inject FullList a into the general list: fromFL. We insist on writing
the latter function explicitly, which keeps the typesystem simple,
free of subtyping and implicit coercions. One may regard fromFL as an
analogue of fromIntegral -- which, too, we have to write explicitly, in
any code with more than one sort of integral numbers (e.g., Int and
Integer, or Int and CInt).

	If we are not sure if our function foo maps non-empty lists
to non-empty lists, we really should handle the empty list case:

	\l -> indeedFL l onempty $
	       \l -> [head l, indeedFL (foo $ fromFL l) onempty' head]

If we have a hunch that foo maps non-empty lists to non-empty lists,
but we are too busy to verify it, we can write

	\l -> indeedFL l onempty $
	       \l -> [head l, indeedFL (foo $ fromFL l) 
				(assert (const False msg) undefined)
			         head]
	  where msg = "I'm quite sure foo maps non-empty lists to " ++
	              "non-empty lists. I'll be darned if it doesn't."

That would get the code running. Possibly at some future date (during
the code review?) I'll be called to justify my hunch, to whatever
degree of formality (informal argument, formal proof) required by the
policies in effect. If I fail at this justification, I'd better think
what to do if the result of foo is really the empty list. If I
succeed, I'd be given permission to update the module NList with the
following definition
	nfoo (FullList x) = FullList $ foo x

after which I could write
	\l -> indeedFL l onempty (\l -> [head l, head (nfoo l)])
with no extra empty list checks.


It goes without saying that it would save a lot of typing if 
List were a typeclass (like Num) rather than a datatype...