hydra icon indicating copy to clipboard operation
hydra copied to clipboard

Incorrect encoding of universal types in showTerm

Open joshsh opened this issue 1 year ago • 2 comments

showTerm for a "\x.x" term after type inference currently looks as below. The top-level type annotation is wrong; it is missing the "lambda" variant name which indicates a universal type. The implementation of showTerm is in the Hydra kernel, so I won't touch it until I am done revising type inference. But TODO: fix it.

{
  "annotated": {
    "annotation": {
      "type": {
        "body": {
          "function": {
            "codomain": "?tv_1",
            "domain": "?tv_1"
          }
        },
        "variable": "tv_1"
      }
    },
    "subject": {
      "function": {
        "lambda": {
          "body": {
            "annotated": {
              "annotation": {
                "type": "?tv_1"
              },
              "subject": {
                "variable": "x"
              }
            }
          },
          "parameter": "x"
        }
      }
    }
  }
}

joshsh avatar Feb 13 '24 19:02 joshsh

Note: the "subject" and "annotation" fields are also backwards in the serialized JSON. Although order of JSON attributes is not supposed to be significant, we can choose to serialize the fields in a canonical order.

joshsh avatar Feb 14 '24 00:02 joshsh

Also, the ? convention, as in "?tv_1", is convenient but not helpful in the long run, as it is an obstacle to deserialization. Instead of "?tv_1", we should use {"variable": "tv_1"}.

joshsh avatar Feb 14 '24 01:02 joshsh

Both fixed.

joshsh avatar Aug 13 '24 14:08 joshsh