| > The fromJust and `head of empty list' errors are totally equivalent to | > the dereferencing of zero pointer in C++ or NullPointerException in | > Java. It pains me to see that exactly the same problem arises in | > Haskell -- keeping in mind that already in C++ and Java one may | > exterminate these errors given right encapsulations. Languages like | > Cyclone or Cw use the type system to eliminate such errors. Surely | > Haskell can do something about this? | | Yes, these techniques are fairly well known now, and hopefully some of | the more experienced Haskellers are using them (I certainly use the | non-empty list tricks). Any anyone with more than 6 months Haskell knows | to avoid fromJust. | | The problem I see is that head/fromJust errors are usually caused by | *beginner* Haskellers, who don't know the techniques for statically | avoiding them. I don't agree. 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 ] (Maybe if I had an Oleg implant I could express all this in the type system -- but I don't.) But yes, we should have more sophisticated techniques to express and check these invariants. With Dana Xu I'm working on this very thing (see her Haskell Workshop paper http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps); and Neil Mitchell is doing complementary work at York. So I think there is reason to be hopeful. Simon

Simon Peyton-Jones writes:

| The problem I see is that head/fromJust errors are usually |caused by *beginner* Haskellers, who don't know the |techniques for statically avoiding them.

I don't agree. 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 ] (Maybe if I had an Oleg implant I could express all this in the type system -- but I don't.)

But instead of “blah (head [ v | (n,v) <- env, n==target ]) blah”, you could write blah the_v_in_scope blah where (the_v_in_scope:_) = [ v | (n,v) <- env, n==target ] and get a source-code located error message, couldn't you? It's not very high tech, but it's what you would write if head didn't exist, and it doesn't seem /that/ great an imposition. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk

"Neil Mitchell" writes:

Hi

Haskell is great for equational reasoning.

...

blah the_v_in_scope blah where (the_v_in_scope:_) = [ v | (n,v) <- env, n==target ]

This piece of code isn't.

Strange. It's semantically the same, isn't it? Indeed, the definition of head gets you to it.

If you used head then you could trivially inline the_v_in_scope, this way is a lot harder.

I don't follow that at all. I don't do inlining, the compiler does. Or are you talking about the inlining that was originally there and my version explicitly removed?

You might spot a pointfree pattern and lift it up. You might move code around more freely. Lots of patterns like this breaks the equational reasoning in the style that most people are used to.

To convince me of that, you'd have to convince me that (head []) doesn't break the equational reasoning.

...

and it doesn't seem /that/ great an imposition.

I disagree, this is a massive imposition, and requires lots of refactoring,

"lots" is in the eye of the beholder. You only have to do this where you would have used head -- and if you can already /prove/ that head won't fail, there's no reason to replace it. So it's only necessary in cases where the proof is absent.

and is just a little bit ugly.

Sure, I don't dispute that. I was merely suggesting that one can already do this for the uncertain cases, rather than have to invoke a whole other set of new machinery just to get a line number in the error message. Your headNote is a good approach, but it strikes me that it's a bit redundant. Instead of “headNote "foo"” just use “headDef (error "foo")”. It's a wee bit longer, but having the “error” out there in the open seems more honest somehow, and there would be fewer function names to remember. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk

Robert Dockins writes:

On Nov 15, 2006, at 9:48 AM, Jón Fairbairn wrote:

...

But instead of “blah (head [ v | (n,v) <- env, n==target ]) blah”, you could write

blah the_v_in_scope blah where (the_v_in_scope:_) = [ v | (n,v) <- env, n==target ]

Or how about.... ??

lookupVarible target env = case [ v | (n,v) <- env, n==target ] of (x:_) -> x _ -> assert False $ "BUG: Unexpected variable out of scope "++ (show target)++" in environment "++(show env)

... lookupVariable target env ....

It seems to me that every possible use of a partial function has some (possibly imagined) program invariant that prevents it from failing. Otherwise it is downright wrong. 'head', 'fromJust' and friends don't do anything to put that invariant in the program text.

Hear hear. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk

Hi

Yes, these techniques are fairly well known now, and hopefully some of the more experienced Haskellers are using them (I certainly use the non-empty list tricks). Any anyone with more than 6 months Haskell knows to avoid fromJust.

I'm not, I use fromJust all the time. Ditto for head, init, maximum, foldr1...

One solution would be to deprecate fromJust (we recently decided not to add fromLeft/Right for the same reasons). Having a compiler warning is a good way to encourage good behaviour :)

We didn't decide not to add fromLeft/fromRight, Russell decided to defer it to a later patch. I am still very interested in them being put in! There seem to be two sides forming to this issue - use partial functions or don't. I don't see why we should restrict the functions available to the partial people, when the unpartial people can choose not to use them. Thanks Neil

Hi

Should Haskell also provide unrestricted side effects, setjmp/ longjmp, missile launching functions, etc? After all, people who don't want to use them can just avoid them. :)

Fair point. But if you eliminate incomplete cases, and the error function, you'd probably need to increase the power of the type checker by introducing dependant types. It's a good research avenue, and an interesting approach, but its not what Haskell is to me (but it might be to others).

Every time I read code containing these functions, I have to perform a non-local analysis to verify the invariant, or even to determine the invariant.

If you use the Programmatica annotations, the ESC/Haskell annotations or Catch then you can have these assertions checked for you, and in the case of Catch even infered for you. Admitedly ESC/Haskell and Catch aren't ready for use yet, but they will be soon! Thanks Neil

Lennart Augustsson writes:

Should Haskell also provide unrestricted side effects, setjmp/ longjmp, missile launching functions, etc? After all, people who don't want to use them can just avoid them. :)

Yes. It is indeed a common problem that programs have unintended behavior, and partial functions are only the tip of the iceberg. We can keep patching things up. For instance, 'head' can be made to never fail simply by requiring all lists to be infinite. Similarly, fromJust can be fixed by having 'data Maybe a = Just a', and doing away with 'Nothing', which is hardly useful for anything anyway. But this is only superficial patchwork that glosses over the deeper problem. I therefore propose that all functions should either be of type '() -> ()', or non-terminating. That should avoid most error messages, I think, and make it very easy to avoid any unintended consequences - and the programmer is relieved of the burden of actively avoiding dangerous stuff. Is it possible to implement this for Haskell'? -k -- If I haven't seen further, it is by standing in the footprints of giants

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.

On 16/11/06, oleg@pobox.com wrote:

And if we are absolutely positive that the value is (Just x), we can always write maybe (assert False undefined) id v

It should be pointed out that Data.Maybe does export a less well-known function, fromMaybe: fromMaybe z = maybe z id This can be used to make the 'maybe X id' case a bit tidier (although technically it's not a save on characters). -- -David House, dmhouse@gmail.com

dons:

dmhouse:

...

On 16/11/06, oleg@pobox.com wrote:

...

And if we are absolutely positive that the value is (Just x), we can always write maybe (assert False undefined) id v

It should be pointed out that Data.Maybe does export a less well-known function, fromMaybe:

fromMaybe z = maybe z id

This can be used to make the 'maybe X id' case a bit tidier (although technically it's not a save on characters).

How controversial would a proposal to {-# DEPRECATE fromJust #-} be, in favour of:

Just _ = x -- which will give you the precise line number

maybe (assert False)

maybe id

fromMaybe

It seems to me this is one cause of mysterious newbie errors we could easily discourage, with little harm.

Btw, I'm not seriously suggesting removing it ;) It could be discouraged ever so slightly in the haddocks though. I'd encourage those worried about fromJust not to use it though, and perhaps try: import Debug.Trace.Location fromMaybe (failure assert "my just was nothing") (Nothing :: Maybe ()) $ ./a.out *** Exception: A.hs:5:34-39: my just was nothing instead of: fromJust (Nothing :: Maybe ()) $ ./a.out *** Exception: Maybe.fromJust: Nothing While Dana and Neil work on more tools for spotting these for us. -- Don

On Fri, 17 Nov 2006, S. Alexander Jacobson wrote:

As long as we are doing this, perhaps we should also discourage the use of (head list)?

Is 'cycle' also bad style, because it fails on empty lists?

On Fri, 17 Nov 2006, Neil Mitchell wrote:

Hi

...

...

How controversial would a proposal to {-# DEPRECATE fromJust #-} be, in favour of:

Just _ = x -- which will give you the precise line number

...

...

It seems to me this is one cause of mysterious newbie errors we could easily discourage, with little harm.

Btw, I'm not seriously suggesting removing it ;) It could be discouraged ever so slightly in the haddocks though.

I strongly disagree. If we are removing things that confuse newbies why not start with higher rank types, MPTC's and GADT's ;)

fromJust is simple, useful and clear. What you mean is that implementations aren't very good at debugging this. It seems unfair to blame partial functions for the lack of a debugger. If a call stack was automatically output every time a fromJust failed would this even be something people complained about?

It seems to me like the discussion about static typesafety vs. no or weak typesafety. (Which still exists with respect to several Haskell libraries.) Of course, all type errors can be catched also by a debugger. So was the decision of making Haskell statically type-safe only made in order to be freed of writing a debugger? Certainly not, because type checks can catch errors early and precisely, that is, better than any debugger. That's also true for DEPRECATE fromJust. Give the user a hint early, that his decision of using fromJust is shortsighted and is possibly due to unfortunate program design.

On Fri, Nov 17, 2006 at 11:37:12AM +0000, Neil Mitchell wrote:

fromJust is simple, useful and clear. What you mean is that implementations aren't very good at debugging this. It seems unfair to blame partial functions for the lack of a debugger. If a call stack was automatically output every time a fromJust failed would this even be something people complained about?

indeed. jhc debugs this quite fine. when you use it the wrong way you get Main.hs:23:33:fromJust Nothing as your error message. or you should at least. likewise for head, tail, undefined, etc.. actually any function including ones you write yourself for which you give the SRCLOC_ANNOTATE pragma. boy I want to have the time to port that to ghc... a six pack of beer for whoever does :) John -- John Meacham - ⑆repetae.net⑆john⑈

Daniel, you wrote:

I suspect I would be classified as a newbie relative to most posters on this list but here's my thoughts anyway... [...] One of my initial responses to haskell was disappointment upon seeing head, fromJust and the like. 'Those look nasty', I sez to meself. From day one I've tried to avoid using them. Very occasionally I do use them in the heat of the moment, but it makes me feel unclean and I end up having to take my keyboard into the bathroom for a good scrubbing with the sandsoap.

I completely agree and couldn't have said it in any better way (including the relative newbie part). Ben