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

[Dan Licata]

Hi Conor,

This is a really good point, especially in the presence of GADTs and
type-level functions and so on, which introduce aspects of dependency.

Why are you so fatalistic about "with" in Haskell?  Is it harder to
implement than it looks? It seems to be roughly in the same category as
our view pattern proposal, in that it's just an addition to the syntax
of pattern matching, and it has a straightforward elaboration into the
internal language.  (Well, for Haskell it's more straightforward than
for Epigram, because we don't need to construct the evidence for ruling
out contradictory branches, etc., necessary to translate to inductive
family elims.)

-Dan

On Jul25, Conor McBride wrote:
> 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.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>