Try to fix bug demonstrated in commit fbebfeb

[davidweichiang]

by undoing an optimization in AffLin. I think this is progress (it fixes a simplified version of the bug), but it is still not working on the new test cases.

[davidweichiang]

95

[ccshan]

This optimization in fact seems superfluous when ProgFun and TmVarG have params, right?

[ccshan]

This optimization in fact seems superfluous when ProgFun and TmVarG have params, right?

If you agree with this statement and with my commits, please merge; thanks.

[davidweichiang]

It looked to me like the optimization was similar to what was done with ProgFun/TmVarG but when a local variable is bound to a curried lambda expression.

[davidweichiang]

I agree with your commits, but I'm still getting test failures...

[ccshan]

I agree with your commits, but I'm still getting test failures...

Ok I think I see the/one problem in Argify, and how to fix it (but I am first going to sleep). Basically it's using the number of arrows in the type of a global definition to decide how many params it takes, and using eta-expansion to match that number if there are too few lambdas (in argifyProg (ProgFun x [] tm tp)) or too few arguments (in argify tm@(TmApp _ _ _ _)). But the former eta-expansion is unsound (factor 2 in ... is different from \x. factor 2 in ... x), so it should use the number of lambdas, not the number of arrows.

• argifyProg (ProgFun x [] tm tp) should not splitArrows tp and should not eta-expand.
• argify tm@(TmApp _ _ _ _) should not splitArrows tp and should instead look up the number of params from some kind of context, but Ctxt doesn't store the number of params so we'll use something else. If there are too few arguments, eta-expansion is sound and what it should do; if there are too many arguments, the remainder should go in TmApps rather than the TmVarG.

(Speaking of Ctxt though, would you please clarify the comment -- tags, params in Scope/Ctxt.hs (three occurrences), to something like -- tags, type params, if you can confirm my guess that the params [Var] there is not what we're talking about here?)

[davidweichiang]

The errors were caused by a bug totally unrelated to affine-to-linear (my fault, I think), but the weights are still not coming out right, and the reason is finally what you were apparently going for when you wrote these test cases.

[davidweichiang]

Oh, wow. I am not quite understanding yet why it makes such a big speed difference.

[davidweichiang]

I see, is it that eta-reduction creates factors for packing and unpacking pairs? We can make a separate issue for that.

[ccshan]

I see, is it that eta-reduction creates factors for packing and unpacking pairs? We can make a separate issue for that.

Yeah, if by "pairs" you mean additive pairs with unit. Eta-expansion is kind of a way in impure functional programming to declare an expression pure, so I feel this is a reasonable thing to ask the programmer of reverse.ppl to do.

[davidweichiang]

By “pairs” I mean the multiplicative pairs we use for representing lambdas. It seems like eta reduction changes a rule with two external nodes (argument and return value) into a rule with one (a lambda) and along with this change adds a factor which is very very large.

On Mon, Aug 1, 2022 at 22:06 Chung-chieh Shan @.***> wrote:

I see, is it that eta-reduction creates factors for packing and unpacking pairs? We can make a separate issue for that.

Yeah, if by "pairs" you mean additive pairs with unit. Eta-expansion is kind of a way in impure functional programming to declare an expression pure, so I feel this is a reasonable thing to ask the programmer of reverse.ppl to do.

— Reply to this email directly, view it on GitHub https://github.com/diprism/perpl/pull/96#issuecomment-1201932063, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKVY2OIRTOOTLFTA7UQBTLVXB7CLANCNFSM55FVZRXA . You are receiving this because you authored the thread.Message ID: @.***>

[ccshan]

By “pairs” I mean the multiplicative pairs we use for representing lambdas. It seems like eta reduction changes a rule with two external nodes (argument and return value) into a rule with one (a lambda) and along with this change adds a factor which is very very large.

I see: you're saying that let <f,()> = f' in is much more expensive than fnot just because of the unpacking of <,()> but also because f is now a single internal node rather than two external nodes. So "much more" might be reduced by #97.

[davidweichiang]

OK to merge this?

[davidweichiang]

Oh, I didn't see your approval. Merging.