pure
pure copied to clipboard
Top-level proofs for TypeClassLang
The top-level result for TypeClassLang should state:
- given a well-annotated TypeClassLang program
- there should be a valid translation to a PureLang program
- which is itself well-typed (and therefore safe)
Though prior work has considered Core-like/System-F like languages with higher-rank polymorphism, we should hopefully be able to show type preservation for simple types - but this remains to be seen.