[comp.lang.functional] pattern abstraction

sra@ecs.soton.ac.uk (Stephen Adams) (08/31/90)

Does anyone know of a language that supports what I call
`pattern abstraction'.  Maybe I should called it something
else.  I will explain what I mean just now.  What I want to
know is
  (a) has this been done before
  (b) if not why?
  (c) if it has did it give rise to any special problems?

Some languages allow an identifier to be repeated in a
pattern.  The usual meaning to to constrain these parts of
the input value to be equal.  For example, the Miranda
function `after' something from the head of a list but only
if it is the specified value.

	after x (x:rest) = rest
	after x other    = other

This function is equivalent to

	after' x (x':rest) = rest, if x=x'
	after' x other     = other

If you explicitly curry the first function you break it, but
you can do this to the second version.

	after'' x = f where  f (x:rest) = rest
			     f other    = other

	after''' x = f where  f (x':rest) = rest, if x=x'
			      f other    = other

This loss of equivalence under a simple transformation could
be used as a reason to prohibit repeated identifiers in
patterns.  Alternatively, the equivalence could be enforced
by a rule requiring that pattern identifiers that are bound
in the (same|enclosing) scope mean an equality check.
Have any languages taken this route?

chl@cs.man.ac.uk (Charles Lindsey) (09/05/90)

In <3685@ecs.soton.ac.uk> sra@ecs.soton.ac.uk (Stephen Adams) writes:

>	after x (x:rest) = rest
>	after x other    = other

>This function is equivalent to

>	after' x (x':rest) = rest, if x=x'
>	after' x other     = other

>If you explicitly curry the first function you break it, but
>you can do this to the second version.

>	after'' x = f where  f (x:rest) = rest
>			     f other    = other

>	after''' x = f where  f (x':rest) = rest, if x=x'
>			      f other    = other

My knowledge of Miranda syntax is weak, but this does seem to exhibit a
failing I have noticed in the pattern matching syntax of several languages.
The problem is that any identifier appearing in a pattern is thereby assumed
to be a defining occurrence thereof, which prevents me from using previously
declared identifiers in a pattern.

If :: is the cons operator, then

	foo 9 :: x = ...

would be a function expecting a list of integers where the first element was
9, but

	LET nine = 9;
	foo nine :: x = ...

would not be the same thing at all.

My view is that, for avoidance of all confusion, defining occurrences of
identifiers should always be readily identifiable as such. In the language I
am playing with, every defining occurrence is followed by a ':' (which leaves
a nice place to put a type, if you want) so I would put something like

	foo (nine:'int' :: x:'int list') = ...

to expect an 'int list' with at least one 'int' at the start, to be known as
"nine", and

	foo (nine :: x:'int list') =

to expect an 'int list' starting with the value of the already declared
identifier "nine".

With a decent polymorphic typechecker, the first version could be reduced to

	foo (nine: :: x: )

and the second to

	foo (nine :: x: )


Stephen Adams example would then be written

	after (x: :: x :: rest: ) = rest
	after (x: :: other: ) = other

and it would curry to

	after'' (x: ) = f where f (x :: rest: ) = rest
                                f (other: ) = other

gudeman@cs.arizona.edu (David Gudeman) (09/06/90)

In article  <3685@ecs.soton.ac.uk> sra@ecs.soton.ac.uk (Stephen Adams) writes:
]
]If you explicitly curry the first function you break it, but
]you can do this to the second version...
]
]This loss of equivalence under a simple transformation could
]be used as a reason to prohibit repeated identifiers in
]patterns...

Aternatively, you could say that the transformation was done
incorrectly.  If the correct rules were applied for currying, then the
transformation would lead to an equivalent program.
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman