[Haskell-cafe] Shouldnt this be lazy too?

[Philippa Cowderoy]

On Mon, 24 Sep 2007, Vimal wrote:

> Wow, half an hour, about 7 replies :) I dont know which one to quote!
> 
> Okay. So, why is GHC finding it difficult to conclude that
> length is always > 0? Suppose I define length like:
> 
> length [] = 0
> length (x:xs) = 1 + length xs
> 
> Hmm, well, I think the fact that we, as humans, expecting GHC
> to infer length (any list) > 0 is pretty unfair :)
> 
> What I had in mind was, when GHC was able to do so many things like
> pattern matching, data type inference, why not this!
> 

Pattern matching is much easier than you might think. If you'll let me 
handwave at you a little, all pattern matches can be translated into a 
series of case statements where each pattern consists of either a variable 
or a constructor with variables to bind each of the constructor's 
parameters to. This isn't actually much more complicated than an 
old-fashioned switch statement!

Type inference is a little more complicated, but largely revolves around a 
process similar to (but more powerful than) pattern-matching called 
unification. There's no magic involved, just sufficiently advanced 
technology.

That part applies especially to lazy evaluation! Every time a 
pattern-match is done, evaluation proceeds far enough to find the 
constructor involved in order to select the right branch. Conceptually, 
the Int type looks like data Int = 1 | 2 | 3 | ... which means that an Int 
is either fully evaluated or completely unevaluated - if you try to 
evaluate "just enough to know it's > 0" then you'll still fully evaluate 
it.

A good rule of thumb is to never expect (or perhaps, never require) GHC to 
do anything that requires it to prove something you're not extremely sure 
you've already written an explicit proof for in the code.

-- 
flippa at flippac.org

The task of the academic is not to scale great
intellectual mountains, but to flatten them.