Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automatic derivation of instances #1293

Open
wants to merge 15 commits into
base: main
Choose a base branch
from

Commits on Apr 12, 2023

  1. [WIP] Add automatic deriving of instances.

    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
    normanrink committed Apr 12, 2023
    Configuration menu
    Copy the full SHA
    1e166ce View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    dfa00ee View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2023

  1. Configuration menu
    Copy the full SHA
    cf1e0b0 View commit details
    Browse the repository at this point in the history

Commits on May 10, 2023

  1. Construct methods for instanced defined with deriving instance ....

    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.
    normanrink committed May 10, 2023
    Configuration menu
    Copy the full SHA
    ec53819 View commit details
    Browse the repository at this point in the history
  2. Remove constructor NewtypeDict.

    This constructor was introduced for automatic derivation of
    instances. This constructor is no longer needed.
    normanrink committed May 10, 2023
    Configuration menu
    Copy the full SHA
    cb628ef View commit details
    Browse the repository at this point in the history
  3. Remove constructor DerivingDef.

    This constructor was introduced for automatic derivation of
    instances. This constructor is no longer needed.
    normanrink committed May 10, 2023
    Configuration menu
    Copy the full SHA
    6f295d9 View commit details
    Browse the repository at this point in the history

Commits on May 11, 2023

  1. Simplify the conversion of methods needed for deriving instance ....

    Specifically, by representing isomorphisms as abstractions (`Abs`) we
    avoid the need for evidence of `Emits`.
    normanrink committed May 11, 2023
    Configuration menu
    Copy the full SHA
    012e84b View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    45b91fd View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    be5de03 View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2023

  1. Configuration menu
    Copy the full SHA
    bf47cd8 View commit details
    Browse the repository at this point in the history
  2. Simplify method conversion.

    Also fix the type of an `App` expression that is constructed
    during method conversion.
    normanrink committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    03ae76e View commit details
    Browse the repository at this point in the history
  3. Simplify dictionary synthesis in automatic instance derivation.

    This simplification has led to the removal of an unsafe coercion.
    normanrink committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    04fb3cc View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2023

  1. Detect method types that are disallowed for automatic instance deriva…

    …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.
    normanrink committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    9fe2576 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    cb1de48 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    b11948f View commit details
    Browse the repository at this point in the history