Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Generalize

Description

This module implements the type checking part of generalisable variables. When we get here we have a type checking problem for a type (or telescope) containing a known set of generalisable variables and we need to produce a well typed type (or telescope) with the correct generalisations. For instance, given

    variable
      A  : Set
      n  : Nat
      xs : Vec A n

    foo : SomeType xs

generalisation should produce `{A : Set} {n : Nat} {xs : Vec A n} → SomeType xs` for the type of `foo`.

The functions `generalizeType` and `generalizeTelescope` don't have access to the abstract syntax to be type checked (`SomeType xs` in the example). Instead they are provided a type checking action that delivers a `Type` or a `Telescope`. The challenge is setting up a context in which `SomeType xs` can be type checked successfully by this action, without knowing what the telescope of generalised variables will be. Once we have computed this telescope the result needs to be transformed into a well typed type abstracted over it.

At no point are we allowed to cheat! Any transformation between well typed terms needs to be done by well typed substitutions.

The key idea is to run the type checking action in the context of a single variable of an unknown type. Once we know what variables to generalise over this type is instantiated to a fresh record type with a field for each generalised variable. Turning the result of action into something valid in the context of the generalised variables is then a simple substitution unpacking the record variable.

In more detail, generalisation proceeds as follows:

- Add a variable `genTel` of an unknown type to the context (`withGenRecVar`).

      (genTel : _GenTel)

- Create metavariables for the generalisable variables appearing in the problem and their dependencies (`createGenValues`). In the example this would be

      (genTel : _GenTel) ⊢
        _A  : Set
        _n  : Nat
        _xs : Vec _A _n

- Run the type checking action (`createMetasAndTypeCheck`), binding the mentioned generalisable variables to the corresponding newly created metavariables. This binding is stored in `eGeneralizedVars` and picked up in `inferDef`

      (genTel : _GenTel) ⊢ SomeType (_xs genTel)

- Compute the telescope of generalised variables (`computeGeneralization`). This is done by taking the unconstrained metavariables created by `createGenValues` or created during the type checking action and sorting them into a well formed telescope.

      {A : Set} {n : Nat} {xs : Vec A n}

- Create a record type `GeneralizeTel` whose fields are the generalised variables and instantiate the type of `genTel` to it (`createGenRecordType`).

      record GeneralizeTel : Set₁ where
        constructor mkGeneralizeTel
        field
          A  : Set
          n  : Nat
          xs : Vec A n

- Solve the metavariables with their corresponding projections from `genTel`.

      _A  := λ genTel → genTel .A
      _n  := λ genTel → genTel .n
      _xs := λ genTel → genTel .xs

- Build the unpacking substitution (`unpackSub`) that maps terms in `(genTel : GeneralizeTel)` to terms in the context of the generalised variables by substituting a record value for `genTel`.

      {A : Set} {n : Nat} {xs : Vec A n} ⊢ [mkGeneralizeTel A n xs / genTel] : (genTel : GeneralizeTel)

- Build the final result by applying the unpacking substitution to the result of the type checking action and abstracting over the generalised telescope.

      {A : Set} {n : Nat} {xs : Vec A n} → SomeType (_xs (mkGeneralizeTel A n xs)) ==
      {A : Set} {n : Nat} {xs : Vec A n} → SomeType xs

- In case of `generalizeType` return the resulting pi type.
- In case of `generalizeTelescope` enter the resulting context, applying the unpacking substitution to let bindings (TODO #6916: and also module applications!) created in the telescope, and call the continuation.

Synopsis

- generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
- generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
- generalizeTelescope :: Map QName Name -> (forall a1. (Telescope -> TCM a1) -> TCM a1) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a

# Documentation

generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type) Source #

Generalize a type over a set of (used) generalizable variables.

generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a) Source #

Allow returning additional information from the type checking action.

generalizeTelescope :: Map QName Name -> (forall a1. (Telescope -> TCM a1) -> TCM a1) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a Source #

Generalize a telescope over a set of generalizable variables.