Debugging a lambda-lifting related bug

[elegios]

This is a summary of the current status of investigating a bug that appears to be strongly connected to the lambda-lifting pass in Miking, which is used in Miking-dppl, which treeppl uses under the hood.

Originally this took the shape of a limitation: we couldn't use polymorphic values at multiple types in a program, e.g., using length on both a list of Int and a list of Real. The one exception of this appears to be if the polymorphic value is let-bound and its body is a lambda, since that means that lambda-lifting won't add a parameter for that value.

This implies a possible workaround: eta-expand all definitions a treeppl program might potentially use.

This is presumably fixed by https://github.com/miking-lang/miking/pull/793 (with follow-up https://github.com/miking-lang/miking-dppl/pull/143 in miking-dppl), which allows lambda-lifting to insert parameters with a polymorphic type (e.g., length would be passed via lam length : all a. [a] -> Int. <...> instead of as lam length : [Int] -> Int).

Unfortunately this appears to expose two new issues (the following text assumes both PRs mentioned above are in use):

Type annotations disappear

Minimal example:

model function myModel(data: ()) : Int
{
    return length([-1.0]);
}

Here lambda-lifting will add a parameter lam length : all a. [a] ->Int . <...>, but at some point during compilation it is changed to lam length : all a. Unknown. <...>, which gives an error along the lines of "you're using a monomorphic value in a polymorphic context".

Pretty-printing the AST in cppl right after lambda-lifting (here) shows that the parameter is correctly annotated at that point, so the annotation disappears/is changed some time later.

Parameter ordering is changed

Minimal example:

model function myModel(data: ()) : Tensor[Real]
{
    return mtxCreate(addi(1,1),1,[-1.0]);
}

I think the reason this is minimal is because it uses more than one value that is bound in such a way that lambda-lifting will add an parameter for both (mtxCreate is let-bound with a right-hand side that is a function application, and addi is bound via let addi = addi, i.e., not a lambda on the right-hand side).

What happens here is that the generated code will contain a definition like let myModel = lam a. lam b. lam c. = <...>[^1], where a, b, and c are the parameters to myModel (i.e., data) and its free variables (mtxCreate and addi). Unfortunately the final code has the arguments at the call-site in one order, and the parameters at the definition in another order. I have yet to figure out the pattern for the reordering.

Once again pretty-printing the AST in cppl right after lambda-lifting shows an AST with arguments/parameters in sync, so the order is changed at some later point.

[^1]: It's possible that this issue appears for some intermediate binding inserted by the ANF transformation rather than directly for myModel, so it might look more like let t42 = lam a. lam b. lam c. <...>, I don't quite remember.

[vsenderov]

@elegios Is the following an example of the same bug, or is it a different bug?

type MyTree =  MyTree { 
    age: Real,
    left: MyTree,
    right: MyTree
  }

model function qtbirds(tree: MyTree): Real 
{
  let result = tree.left.age; // doesn't work
  return result;
}

Here the error is

$ tpplc vartype-err.tppl

ERROR <vartype-err.tppl 9:15-9:24>:
Could not infer this to be a variant type (found a)
  let result = tree.left.age; // doesn't work

[vsenderov]

The workaround being

  ...
  let leftTree = tree.left;
  let result = getAge(leftTree);
  ...

function getAge(tree: MyTree): Real
{
    return tree.age;
}

[elegios]

Different bug, more related to how we handle projection (so #36). The key drawback of it right now is that it doesn't check field accesses until after typechecking has already happened (significantly easier to do, so seemed a reasonable first version), which means that the typechecker has no information for the value returned from tree.left (which is why it says found a, where a is an unknown type variable).

[vsenderov]

@elegios do you mind if I "assign" you for this bug? I am reorganizing things and this is more for that, rather than for prioritization. Actually I am not putting this in the TPPL 2023 release milestone.

[elegios]

Go for it.

On Fri, 15 Dec 2023 at 17:32, Viktor Senderov @.***> wrote:

@elegios https://github.com/elegios do you mind if I "assign" you for this bug? I am reorganizing things and this is more for that, rather than for prioritization. Actually I am not putting this in the TPPL 2023 release milestone.

— Reply to this email directly, view it on GitHub https://github.com/treeppl/treeppl/issues/29#issuecomment-1858152069, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGFZYQO4HY6MJLTCLKCIALYJR3R3AVCNFSM6AAAAAA6MIE46SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNJYGE2TEMBWHE . You are receiving this because you were mentioned.Message ID: @.***>