Typespace::is_nominal_normal_form

[kazimuth]

Description of Changes

Introduces a notion of "nominal normal form" for Typespaces, which requires that Sum and Product types always be referred to via Refs. The intention is that this lets us validate that the Typespace is in a format that makes sense for performing codegen in a nominal language, where each Ref corresponds to a fresh type. (Or type alias, if the Ref points to a Ref.)

This is used in my upcoming module validation PR. Note that in a module, we also have names attached to these slots via MiscModuleExport, but this code doesn't care about that.

The module bindings should automatically produce Typespaces satisfying this requirement.

We could strengthen this in various ways:

• Require that all types be referred to via Refs.
  • We could additionally require that each Builtin is referred to by at most one ref.
  • AlgebraicType::unit and AlgebraicType::never would then be in a slightly odd place, because they are rep'd as the empty product/sum. I guess you could say that exactly one empty product should have no type alias, and that one will be treated as the "true" unit type.
  • We could introduce new enums for this, possibly in a crate outside sats since most users won't care.
• Forbid Ref chains, or introduce a method to collapse them. This allows generating code for languages without type aliases.

(Please bikeshed the name. Is there a type theory name for this?)

Expected complexity level and risk

1, I mainly just wanna validate that I am checking the right things.

Testing

Added proptests.

[gefjon]

Why do we have both "nominal" and "normal" in the same name?

[kazimuth]

nominal refers to being a normal form that allows codegen for nominal languages. It doesn't mean "all systems nominal".

...except it would be funnier if it did. I'm going to change this to is_nominal.