Improvement to 'Embeddable' typeclass through 'Embedding' GADT - #21
Merged
Conversation
Closed
… We have yet to resolve the term embeddings. The fresh variable generation probably also needs to be changed afterwards.
…imply expand. Makes the declarations a lot easier, as everything is now Haskell and we just pass in a Template Haskell name. Implemented the term embeddings. TODO: Propagate the usage of these new embeddings to the symbolic evaluator!
…ixed the 'Embedding' datatype instance, which got the wrong coercion.
…ug in generate Embedding instance where we used the wrong destination type. Added functional dependency on 'Embeddable', locking in to the class being non-symmetric. Though the coercion is symmetric, the direction of the embedding is not!
RobinWebbers
force-pushed
the
hetero-embed
branch
from
July 31, 2026 08:16
a8a05cd to
0a83fe0
Compare
This was referenced Jul 31, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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 pull request closes #4. This leaves open the kindedness check of the two types. That is, we may embed two types that have different runtime representations. It is unclear whether two kinds that have type arguments with different runtime reps should also allow for embeddings. My intuition says yes. This check is a little bit annoying to perform however. I will open a new issue to tackle this so we can pull this in for the time being!
To list the changes we made:
PluginAxiomtoEmbeddings,typeAxiomstotypeEmbeddings, etc.InstEnvfor more robust instance lookups.Embeddabletypeclass that wraps aEmbeddingGADT which carries a coercion equality between the heterogenous kinds, as well as the original coercion.Embeddableonly. Note thatEmbeddableis unidirectional, so we only support instances one way.Embeddablehas a functional dependency where the lhs type decides the rhs.InstEnvsnow.InstEnvsnow. It is a little bit limited in that it doesn't work with type variables. This is consistent with the old behaviour. We will not work on fixing this directly, instead doing so via Fresh variable generation API #3.