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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe