CategoricalData / hydra

Transformations transformed
Apache License 2.0
64 stars 9 forks source link

Incorrect encoding of universal types in showTerm #117

Open joshsh opened 5 months ago

joshsh commented 5 months ago

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 commented 5 months ago

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 commented 5 months ago

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"}.