hazel icon indicating copy to clipboard operation
hazel copied to clipboard

polymorphic equality and inequality

Open disconcision opened this issue 4 months ago • 3 comments

@cyrus- are you still okay making the equality operator polymorphic? I've done this on the LLM branch for convenience, so I'll copy-paste some code here to accelerate someone doing it for real.

  1. Add case to statics.re:
| BinOp(Int(Equals | NotEquals), e1, e2) =>
  let (e1, m) = go(~mode=Syn, e1, m);
  let (e2, m) = go(~mode=Ana(e1.ty), e2, m);
  add(~self=Just(Bool), ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]), m);
  1. Add cases to dynamics
    | BinIntOp(Equals, d1, d2) =>
      let* r1 = evaluate(env, d1);
      let* r2 = evaluate(env, d2);
      switch (r1, r2) {
      | (BoxedValue(d1'), BoxedValue(d2')) =>
        let b =
          DHExp.fast_equal(DHExp.strip_casts(d1'), DHExp.strip_casts(d2'));
        return(BoxedValue(BoolLit(b)));
      | (BoxedValue(d1'), Indet(d2'))
      | (Indet(d1'), BoxedValue(d2'))
      | (Indet(d1'), Indet(d2')) =>
        return(Indet(BinIntOp(Equals, d1', d2')))
      };

    | BinIntOp(NotEquals, d1, d2) =>
      let* r1 = evaluate(env, d1);
      let* r2 = evaluate(env, d2);
      switch (r1, r2) {
      | (BoxedValue(d1'), BoxedValue(d2')) =>
        let b =
          !DHExp.fast_equal(DHExp.strip_casts(d1'), DHExp.strip_casts(d2'));
        return(BoxedValue(BoolLit(b)));
      | (BoxedValue(d1'), Indet(d2'))
      | (Indet(d1'), BoxedValue(d2'))
      | (Indet(d1'), Indet(d2')) =>
        return(Indet(BinIntOp(Equals, d1', d2')))
      };
  1. Fix #1243 to prevent above from crashing

The above is sufficient to get it basically working. Remaining issues:

  1. Decide on behavior on edge cases, in particular function values. We could prohibit comparisons of types (which contain) arrow types at the static level, or just always return false at the dynamic level. The latter is simpler, but can be confusing, especially if you have a large type that you've forgotten has an arrow somewhere in it (this happens in the Hazel model type not infrequently...). The above code currently just compares for structural equality of function implementations, including closed over values
  2. Data structures cleanup and backcompat: Remove operators from Int BinOp subtype, remove float and string specific operators (maybe? backwards compatibility is starting to become a concern)
  3. Update langdocs

disconcision avatar Mar 19 '24 19:03 disconcision