Hi Ok, I'm not quite under my rock yet,,, On 25 Jul 2007, at 10:28, apfelmus wrote:
Jules Bean wrote:
Have you tried using pattern guards for views?
f s | y :< ys <- viewl s = .... | EmptyL <- viewl s = ....
This is annoying because the intermediate computation gets repeated. I don't think view patterns fix this even if they sometimes hide it. I worry that the good behaviour of this feature depends on a compiler noticing that a repetition can be shared: this design makes the sharing harder to express. Of course,
Hm, I'd simply use a plain old case-expression here
f s = case viewl s of y :< ys -> ... EmptyL -> ...
which is fine if you're ready to commit to the right-hand side at this point, but what if the result of the intermediate computation tells you what patterns to look for next? Epigram's "with"-notation was never implemented in Epigram, but it has been implemented in Agda 2. At the moment, we'd write f s with viewl s -- adds a new column to the left f s | y :< ys = ... -- so you can now match whatever you like f s | EmptyL = ... Inside a "with-block", the patterns left of | must refine the original patterns left of the "with". When you're fed up looking at the new information, you can exit the block, drop the column and carry on as normal (see zip, below). I'd hope that we might ultimately be able to elide the repeated lefts if they are unchanged, but that's not implemented at the moment. f s with viewl s -- adds a new column to the left | y :< ys = ... | EmptyL = ... So zip might become zip xs ys with viewl xs | x :< xt with viewl ys | y :< yt = (x, y) <| zip xt yt zip _ _ = empty or even zip xs ys with viewl xs with viewl ys | x :< xt | y :< yt = (x, y) <| zip xt yt zip _ _ = empty For more entertainment, a padding zip pzip x' xs y' ys with viewl xs with viewl ys | x :< xt | y :< yt = (x, y) <| pzip x xt y yt | x :< xt | EmptyL = fmap (flip (,) y') xs | EmptyL | y :< yt = fmap ((,) x') ys pzip _ _ _ _ = empty Pattern matching is much weirder in a dependently typed setting, but also a lot more powerful. Inspecting the value of a pattern variable or of an intermediate computation can leave us knowing more about (and hence instantiate) other pattern variables. We get stuff like this gcd :: Positive -> Positive -> Positive gcd x y with trichotomy x y gcd x (x + y) | LT x y = gcd x y gcd x x | EQ x = x gcd (y + x) y | GT x y = gcd x y Here, matching on the result of trichotomy (with constructor patterns, see?) causes the original argument patterns to become more informative (with non-linear non-constructor forms which are *guaranteed* to match at no run time cost). For us, it's a bad idea to try to think of analysing one scrutinee independently of the other data we have to hand. We're naturally pushed towards thinking about the left-hand side as a whole, to which information can be added, supporting further refinement. This is part of what James McKinna and I were on about in "The view from the left", and it's happening on real computers now. To sum up, one-shot matching on intermediate computations, as provided by pattern guards or view-patterns, is conspicuously nasty in a dependently typed language, but for reasons which make it sometimes merely annoying in Haskell. I'm disinclined to argue thus: "don't do your thing (which probably will happen) because it messes up my thing (which probably won't, at least in Haskell)". I'll just chuck these observations in the air and see what happens. All the best Conor PS Please may I have pattern synonyms anyway? They're cheap and they serve a different purpose. Maybe I should say more about how their absence is seriously nasty for the way I work, another time.