SoundX, introduced in "Sound type-dependent syntactic language extension", uses a model of language extension where extension modules build on a host language, defining new typing rules and rule for desugaring new syntax. Evaluation is defined only for the host language. Programs are type checked using the extended language, but then desugared before being evaluated.
SoundX has one property, that if a term t with
type ty desugars to t',
then t' has type ty',
where ty desugars to ty'. This property
is proven automatically by the SoundX system. Because the
desugared program is the version that is run and we know it is
well-typed, we then get the benefits of typing, such as type
preservation and progress, from a proof for the host language
alone.
In this example, we emulate SoundX by defining typing over
extensions, but evaluation only over the host language. SoundX's
property is proven by each extension
(desugar_ty_rel), along with some other properties of
typing. The host language proves properties about evaluation for
itself alone. Unlike in SoundX, the proof of SoundX's property is
not automatic. However, also unlike SoundX, Extensibella can
support extending the definitions of more relations than typing.
Compare the language here
to our other version of the
language where we define evaluation and substitution for the
extensions as well, and prove the properties of evaluation for
them directly instead of through desugaring.