RoundTrip tests need a stronger equality

[yuriy0]

As of 21774d0e, at least five of the tests in RoundTrip.hs fail because the equality test is too weak.

It is unclear if this should be implemented as a new equality predicate, or a change to alphaEq, or a normalization which makes the expressions in question alpha-equivalent.

5:RoundTrip:0:7:t44Add

expected:
fn x1 real:
 fn x0 real: weight(real2prob(((x1 ^ 2) + (x0 ^ 2))), return ())
but got:
fn x1 real:
 fn x0 real: weight(real2prob(((x0 ^ 2) + (x1 ^ 2))), return ())

operator associativity

5:RoundTrip:0:13:t57

expected:
fn x0 real:
 (match ((x0 < 1) && (0 < x0)):
   true: weight(2, return ())
   false: return ())
but got:
fn x0 real:
 (match ((0 < x0) && (x0 < 1)):
   true: weight(2, return ())
   false: return ())

operator associativity

5:RoundTrip:3:0:t4

expected:
x0 <~ uniform(0, 1)
weight(real2prob(x0), return (real2prob(x0), true)) <|>
weight(real2prob((1 - x0)), return (real2prob(x0), false))
but got:
x0 <~ uniform(0, 1)
weight(real2prob(x0), return (real2prob(x0), true)) <|>
weight(real2prob((1 + (x0 * (-1)))),
       return (real2prob(x0), false))

ring algebra

5:RoundTrip:1:5:t35

expected:
fn x0 real:
 (match (x0 < 4):
   true: return 3
   false: return 5)
but got:
fn x0 real:
 return (match (x0 < 4):
          true: 3
          false: 5)

return distributes over match

5:RoundTrip:2:16:t45

expected:
x0 <~ normal(4, 5)
(match (x0 < 3):
  true: return (x0 ^ 2)
  false: return (x0 - 1))
but got:
x0 <~ normal(4, 5)
return (match (x0 < 3):
         true: (x0 ^ 2)
         false: (x0 - 1))

return distributes over match

[JacquesCarette]

From a CAS perspective, tests t44Add and t57 should be fixed by having an Ord instance for most parts of abt, and 'sorting' commutative terms. The Ord instance could be obtained via hash-consing. [Note that I am not necessarily suggesting we do this - there might be very good reasons not to!].

t4 is trickier, as it would need a 'polynomial normal form'. Maple does have this. But in Haskell-Hakaru, we don't really have 'polynomials'. So I am not sure how feasible this is.

t35 and t45 feel different: we should agree on where we expect the return to be (based on the input), and make sure that that is what we get. Note that in both cases a "control flow" piecewise was expected, but a dataflow one was received instead. The question is: given the actual input in each case, what should we be expecting? Simplify is now quite careful about that [unlike the previous code, which wasn't], and these tests were written for the old behaviour.

[yuriy0]

From a CAS perspective, tests t44Add and t57 should be fixed by having an Ord instance for most parts of abt, and 'sorting' commutative terms. The Ord instance could be obtained via hash-consing. [Note that I am not necessarily suggesting we do this - there might be very good reasons not to!].

t4 is trickier, as it would need a 'polynomial normal form'. Maple does have this. But in Haskell-Hakaru, we don't really have 'polynomials'. So I am not sure how feasible this is.

I agree both these problems may be entirely non-trivial.

t35 and t45 may be outdated test cases.

t35 tests that both programs (return (match ..) and match( .. : return .. )) to simplify to the latter, but they both simplify to themselves. I think this is what we want. It should be two test cases with each program simplifying to itself.

t45 does the same thing, and additionally tests that a third program which currently (genuinely) doesn't simplify (although I don't think it gets to that test).

[JacquesCarette]

So I think that t35 and t45 might be outdated. @ccshan ? I think they should indeed simplify to themselves.

For the 3rd program in t45, that might be worth separating out in a different issue.

[ccshan]

Regarding hakaru/tests/RoundTrip/t[34]5.* nowadays:

• It's ok if each of them simplifies to itself.
• It's kind of better to avoid control piecewise in favor of data piecewise, so both for simplifying t35.0.hk and for simplifying t35.expected.hk, the better result to produce is t35.0.hk, but it is acceptable to produce t35.expected.hk too. And for simplifying t45.0.hk and t45.1.hk and t45.expected.hk, the better result to produce is t45.0.hk, but it is acceptable to produce t45.expected.hk too.
• It's alright if t45.1.hk simplifies to itself, but it shouldn't be the result of simplifying t45.0.hk or t45.expected.hk. I hope this helps.

[JacquesCarette]

Making sure that @GenevaS sees this too.

[yuriy0]

At least for testing purposes, this is fixed by changing the expected outputs. Maple reliably produces x^2 instead of x*x so that should be fine. The literal-related issues are fixed by the recent changes to parser/pretty printer.