🚀 go-pugleaf

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