`[ (X Y) -> X ] (T b)` should reduce to `T` for any term `T`.

[jamestmartin]

Context: [ (X Y) -> Y ] (a T) reduces to T for any term T. This is expected behavior.

Expected behavior: Similarly, [ (X Y) -> X ] (T b) should reduce to T for any term T.

Actual behavior: [ (X Y) -> X ] ((a b) c) does not reduce at all, because ((a b) c) expands to (a b c) and we can't match against a 3-application term with a 2-application pattern.

We can write the pattern [ ((X Y) Z -> (X Y) ], but as far as I know, it isn't possible to match against an arbitrary n-application. In my opinion, the current behavior is unexpected and unhelpful.

Use case: I'm trying to implement delimited continuations, and I need to be able to match against terms which look like (shift E) X..., but this expands to (shift E X...), so the pattern match fails. I can implement ((X Y) Z) patterns as a special case, but this results in code duplication and prevents shift from returning variadic functions.

using System
def double = \X -> 2 * X

data shift
def reset = resetK (\X -> X)
# accumulates the continuation in an extra argument K
def resetK = \K -> [ (shift E) -> E (\X -> reset (K X))
                   | (X Y) -> resetK (\Y2 -> resetK (\X2 -> K (X2 Y2)) X) Y
                   # | ((X Y) Z) -> resetK (\Z2 -> resetK (\XY2 -> K (XY2 Z2)) (X Y)) Z
                   | X -> K X ]

# works
def test1 = reset (double (shift (\K -> K (K 2))))
# requires the extra `((X Y) Z)` pattern
def test2 = reset ((shift (\K -> K (\X -> X + 2))) 6)
# doesn't work without adding yet another `(((W X) Y) Z)` pattern
def test3 = reset ((shift (\K -> K (\X Y -> X + Y)) 3 4))

[egel-lang]

Oh hi James, nice to see you've taken an interest, I didn't notice so far. You are correct, according to Egel's (operational) semantics (a b) c equals a b c. As I've been busy writing a new emitter, this could be important. I will get back to you in some days.

[egel-lang]

Off the cuff, I haven't looked at your example in detail. You did notice that you can write [X Y -> X] a b c and that does rewrite to a c?

[egel-lang]

I rewrote your example as

using System
def double = \X -> 2 * X

data shift
def reset = resetK [X -> X]
def resetK =
    [ K (shift E) -> E K
    | K F -> resetK [X -> F (K X)] ]

def test1 = reset double (shift (\K -> K (K 2)))
def test2 = reset (shift (\K -> K (\X -> X + 2))) 6
def test3 = reset id(shift (\K -> K (\X Y -> X + Y))) 3 4

def main = (test1, test2, test3)