"Neil Mitchell"
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