Automatic derivation of instances #1293
Open
Conversation
This file contains 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
This change adds the following: - syntax `deriving instance ...` for automatic derivation of instances/dictionaries - constructor `NewtypeDict` for dictionary expressions - synthesis of `NewtypeDict` dictionaries - (currently incorrect) simplification of method applications on `NewtypeDict dictionaries
Methods are constructed by first synthesizing a dictionary for the instance that is derived from. Those methods are then converted to methods suitable for the derived instance by using an isomorphism between types.
This constructor was introduced for automatic derivation of instances. This constructor is no longer needed.
This constructor was introduced for automatic derivation of instances. This constructor is no longer needed.
Specifically, by representing isomorphisms as abstractions (`Abs`) we avoid the need for evidence of `Emits`.
Also fix the type of an `App` expression that is constructed during method conversion.
This simplification has led to the removal of an unsafe coercion.
…tion. The current implementation of automatic instance derivation synthesizes methods (for the derived instance) in a way that is guided by the method types in the instance that we are deriving _from_. For the method synthesis to work correctly certain types (i.e. the type we are deriving _from_ and the type we are deriving an instance _for_) must not be mentioned in the type of the class method that corresponds to the instance method that is being synthesized.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
For types of the form
if there is an
instance Class(WrappedTy(<params>)), aClassinstance forNewTy(<params>)can be automatically derived. This PR implements automatic instance derivation with the syntaxNote that automatic instance derivation is asked for in issue #945, but the approach taken in this PR differs from extending
DictExpr nwith a new contructorNewtypeDict (DictType n) (DictExpr n), as suggested in issue #945. Instead, this PR synthesises anInstanceDefforClass(NewTy(<params>))from the definition ofinstance Class(WrappedTy(<params>)).The main difficulty in synthesising the
InstanceDefforClass(NewTy(<params>))is converting the methods ofinstance Class(WrappedTy(<params>)), which operate onWrappedTy(<params>), to methods that work withNewTy(<params>). Since the typesWrappedTy(<params>)andNewTy(<params>)are isomorphic, this conversion is generally possible. Note that in order to facilitate this conversion, an isomorphism betweenWrappedTy(<params>)andNewTy(<params>)must be exhibited, consisting of a pair of maps, namely of a (forward-directed) isomorphism and its (backward-directed) inverse.