hazelgrove / hazel

Hazel, a live functional programming environment with typed holes
http://hazel.org/
MIT License
805 stars 52 forks source link

polymorphic equality and inequality #1252

Open disconcision opened 8 months ago

disconcision commented 8 months ago

@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);
  2. 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')))
      };
  3. 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
cyrus- commented 8 months ago

Yeah, I'm okay with adding this for now with the plan to rip it out down the line when we have implicits. I'll mark it as a possible starter project.

cyrus- commented 7 months ago

@disconcision @GuoDCZ is planning to take a look at this as a starter project. is the relevant code in this PR? https://github.com/hazelgrove/hazel/pull/1148 (or is it in the plus branch?)

disconcision commented 7 months ago

neither. it's in llama-lsp-lookahead (something something hardest problem in computer science). note that literally all the relevant code written so far is reproduced above though