Wrong reduction

[notoria]

Reproducing the behavior

I tried to reduce the Main and got an unexpected result, there is no error or warning:

Main = λa λb (((λc a) a) b)  |  Expected: λa λb (a b)  |  Result: λa a
Main = λa (a λb ((λc c) b))  |  Expected: λa (a λb b)  |  Result: λa (a λa (λb b a))
Main = λa (a λb ((λc b) b))  |  Expected: λa (a λb b)  |  Result: λa (a λa let {b c} = a; (λ* b c))

But it worked for other like:

Main = λa (a λb ((λc b) a))  |  Expected: λa (a λb b)  |  Result: λa (a λb b)

It isn't clear what is wrong with the Main.

System Settings

Example:

• HVM: 2.0.17
• Bend: 0.2.21
• uname -srvmo: Linux 6.8.9-arch1-2 #1 SMP PREEMPT_DYNAMIC Tue, 07 May 2024 21:35:54 +0000 x86_64 GNU/Linux

Additional context

No response

[developedby]

1: The result is the eta-reduced form of the expected.

2 and 3: The inner lambdas are combinators, which are converted into lazy references to top-level functions and so didn't get executed. I understand that for the main function this is generally not what users want. This is being tracked here https://github.com/HigherOrderCO/Bend/issues/424

[developedby]

Note that all the reductions are correct, just not in the form that you expected

[notoria]

Sometimes eta-reduction isn't done:

Main = λa λb (a ((λc c b)))  |  Result: λa λb (a b)

and:

Main = λa λb (a b)  |  Result: λa a

Which one would be the right answer?

[developedby]

We eta-reduce the input but not the output. But they're equivalent in effect so both are correct

[notoria]

Missing some beta-reduction:

Main = (λa a λa (λb b a))  |  Result: λa (λb b a)

and:

Main = λa (λb b a)  |  Result: λa a

It's not clear why the reduction is missing.

[developedby]

2 and 3: The inner lambdas are combinators, which are converted into lazy references to top-level functions and so didn't get executed. I understand that for the main function this is generally not what users want. This is being tracked here #424

[notoria]

I have an unexpected result:

Main = λa (λb (λc b b) λb (b (a b)))  |  Result: λa λb (b (a *))

While I expected something like λa λb (b (a b)).

Is this the same issue?

[developedby]

No, thats a different problem. Your program duplicates a function that duplicates a value, which is currently not valid in Bend. In some cases this is caught during runtime and the program panics, but we don't know of any way to detect all cases besides type checking.

[developedby]

With #548, it should be much rarer to trigger the second and third cases of your original comment

[notoria]

Indeed it seems to be gone.

Without duplication:

Main = λa λb (λc b (a λc c))  |  Result: ((λa a, *), λb b)  |  Expected: λa λb b

[developedby]

Indeed it seems to be gone.

Without duplication:

Main = λa λb (λc b (a λc c))  |  Result: ((λa a, *), λb b)  |  Expected: λa λb b

Conversion from HVM to Bend can have more than one possible interpretation. The resulting net, in HVM syntax is (((a a) *) (b b)) ((λa a, *), λb b) is one valid form of the result. Another equally valid result would be let * = (a λc c); λa λb b, which is the one you're expecting.

Currently the heuristic for deciding if a node is a lambda or a tuple is very simplistic and will give some unexpected results.