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. -- [EMAIL PROTECTED] The task of the academic is not to scale great intellectual mountains, but to flatten them. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe