[Haskell-cafe] Re: [Haskell] View patterns in GHC: Request for feedback

[Conor McBride]

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.