[Haskell] Re: Context of a pattern variable

[kahl at cas.mcmaster.ca]

Tomasz Zielonka <tomasz.zielonka at gmail.com>
proposed an interesting kind of ``second-order as-patterns''
that are ``safe'' from the usual problems of second-order matching
by virtue of fixing (at least) the spine
of the images of the second-order variables.

Tomasz' first example (incorporating Stefan Holdermans' correction) is:

 | before:
 | 
 |   case t of
 |       (x, y, z) -> (x, y, z+1)
 | 
 | after:
 | 
 |   case t of
 |       (_, _, ctx @> z) -> ctx (z + 1)

Stefan Monnier <monnier at iro.umontreal.ca>
generalised to contexts with arbitrarily many holes:

 > >   case t of
 > >       (x, y, z) -> (x, y, z+1)
 > 
 > How would you do:
 > 
 >     case t of
 >         (x, y, z, a, b, c) -> (x+1, y, z, a, b, c+2)
 > 
 > would you allow:
 > 
 >     case t of
 >         (ctx @> x, _, _, _, _, ctx @> c) -> ctx (x+1) (c+2)

First a minor point of ``getting the names right'':

In either case ``ctx'' is a second-order variable,
or a metavariable in the sense of Klop's Combinatory Rewriting Systems
(CRSs, [Klop-1980]), and not a variable for a ``context''
in the technical sense of ``term with a hole''.
Even if patterns in Haskell included variable binders,
we would want to avoid the variable capture allowed by instantiating the
hole of a context containing variable binders on its spine.
(In the context of first-order patterns this distinction is not
 so relevant, but I still believe that it makes sense to be careful.)

Already in his original message, Tomasz identifies the following problem:

 >   case t of
 >       (x, y, (a, ctx @> Just z)) -> ctx z
 > 
 > wouldn't be equivalent to this one
 > 
 >   case t of
 >       (x, y, v) -> 
 >           case v of 
 >               (a, ctx @> Just z) -> ctx z

[ The last line contains my interpretation of Tomasz' intention. ]

This could be alleviated by making the character of the intended binding
as a second-order binding more explicit
by allowing as-patterns to bind against function left-hand sides,
where variables occurring in patterns may be ``co-bound''
in the pattern part of the as-pattern
by a SINGLE occurrence of the ``co-as''
for which I continue to use Tomasz' symbol ``@>''.

The first example would then be written:

   case t of
      (ctx zH) @ (_, _, zH @> z) -> ctx (z + 1)

I continue to use the variable name ``ctx'' to better exhibit the
relation with the original notation.
``zH'' stands for ``z-hole'' for lack of a better naming convention.
The first occurrence of zH is a binding occurrence,
and the second occurrence is co-bound by the ``@>''.
(Replacing ``@>'' with ``@'' could give rise to confusing errors,
 no matter which way the binding of its left argument is resolved.)

The first version of Tomasz' counterexample
is treated in the same way as the first example:

  case t of
    (ctx zH) @ (x, y, (a, zH @> Just z)) -> ctx z

The expression corresponding to the ``broken'' context
then exhibits a composed context:

  case t of
    (ctx1 vH) @ (x, y, vH @> v) ->
        case v of
           (ctx2 zH) @ (a, zH @> Just z) -> ctx1 (ctx2 z)


Allowing arbitrary function left-hand sides
(non-terminal ``funlhs'' from the Haskell98 report)
is probably not useful, but should be otherwise unproblematic ;-)

As an example,

  case q1 of
    (f (xH, yH)) @ ((xH @> x, yH @> y) : _) -> f p

would be equivalent to:

  case q1 of
    (f pH) @ (pH @> (x, y) : _) -> f p


Essentially the same holds for admitting ``hole variables''
that are not bound by a @>, since they will just be ignored arguments
of the ``context'' function.

   case q2 of
     (f xH yH) @ (xH @> x, Nothing) -> f (x+1) (Right 2)

would be equivalent to:

   case q2 of
     (f xH) @ (xH @> x, Nothing) -> f (x+1)


(The restriction to only single occurrences to the left of @>
 corresponds directly to the linearity requirement for Haskell patterns.)


I think that this way we have the concepts right ---
how useful this feature would be
is probably going to be mostly a question of programming style.
For very deep pattern matching in, for example, XSLT-like applications
it could probably be quite convenient.



Best regards,

Wolfram



@TechReport{Klop-1980,
  author = {Jan Willem Klop},
  title = {Combinatory Reduction Systems},
  year = 1980,
  type = {Mathematical Centre Tracts},
  number = 127,
  note = {PhD thesis},
  institution = {Centre for Mathematics and Computer Science},
  address = {Amsterdam},
}