Coerce format descriptions into representation types #355
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds implicit coercions from format descriptions into their representation types during elaboration, removing the need to explicitly call
Repr
in most cases. This would almost bring us full circle back to when I was trying to use subtyping in Fathom, but now the subtyping would be kept out of the core language, greatly reducing the confusing complications that resulted from conflating types and format descriptions.Introducing this style of coercive subtyping during elaboration is also not entirely unheard of either: it is a common addition for elaborators to type theories with Tarski-style universes, which seem to have a connection to our approach to format descriptions.
Drawbacks
By inserting calls to
Repr
implicitly, people learning Fathom could end up finding it harder to understand the difference between format descriptions and host representation types.Repr
might also show up in error messages, and this could also result in confusion if people using Fathom aren't used to being explicit about converting between them. We could try to remove the explicitRepr
calls during distillation, but would most likely be an imperfect process and could further exacerbate confusion when they do eventually appear.Introducing subtyping could also make unification more difficult. I don't think this is too much of an issue for this limited use case, but I still don't fully understand the implications or potential interactions. We also probably want to add more subtyping in the future, for example as a way make refinement types usable (coercing from refined to non-refined terms), so we’ll probably have to deal with this anyway down the line.
Resources
When implementing this, I was inspired a bit by elaboration-zoo/experiments/univ-lifts's
coe
function.