ProjectHeterogeneous.md

This is an explanation of the changes introduced in pull request agda/agda#5234

Twin context infrastructure

When checking whether two well-typed terms t and u are convertible, they might not be typed in the same context.

From the example above, we have a constraint B ≈ B′ type, where Γ,A ⊢ B type and Γ,A′ ⊢ B′ type.

We can annotate terms with a phantom type to indicate on which side they live on:

data HetSide = LHS | RHS | Compat | Both

newtype Het (s :: HetSide) a = Het a

(Compat should disappear before this pull request is merged).

The HetSide annotations help both the Agda developer and the typeclass machinery perform operations in the appropriate context.

For instance, B ≈ B′ type becomes `ValueCmp_ CmpEq AsTypes (Het @'LHS "B") (Het @'RHS "B′").

To represent the type of a variable in the context, we define TwinT:

data TwinT' b a =
    SingleT { unSingleT :: Het 'Both a }
  | TwinT { twinPid    :: ISet ProblemId   
          , necessary  :: Bool             
          , direction  :: CompareDirection 
          , twinLHS    :: Het 'LHS a    
          , twinRHS    :: Het 'RHS a    
          }

type TwinT = TwinT' Type

• twinLHS and twinRHS are the left and right sides of the type. As the phantom type indicates, they are well-typed only on the left or right side of the term.

• For every twin type, there is one or more constraints which will make both sides of the twin "equal". Because Agda supports subtyping, direction indicates whether equal means that LHS is a subtype of RHS, RHS is a subtype of LHS, or that both are trully equal.

• twinPid is a set of unification problems which, when all solved, is sufficient for twinLHS and twinRHS to be "equal". ISets are functionally Sets; they are described below.

• necessary indicates whether the problems in twinPid are sufficient to This bit is currently unused, although it could be potentially used to improve performance.

(Het and TwinT' are actually type synonyms for Het and TwinT'', but bear with me).

The _α from the previous section now becomes:

TwinT { twinPid = [1],
      , necessary = True,
      , direction = DirEq,
      , twinLHS = Het @'LHS "A",
      , twinRHS = Het @'RHS "A′"
      }

A twin type is single if either its constructor is SingleT, or if its twinPid is the empty set.

Accessing sides of a twin

The overloaded function twinAt can access the different sides of a twin type. For instance:

twinAt :: forall s a. a -> TwinAt_ s a
twinAt @'LHS :: Het 'LHS a -> a
twinAt @'RHS :: Het 'RHS a -> a
twinAt @'LHS :: TwinT -> Type
twinAt @'RHS :: TwinT -> Type
twinAt @'Both :: TwinT -> Type
twinAt @'Compat :: TwinT -> Type

The last two cases are meant to be applied to single twin types. They return the smallest of twinLHS or twinRHS according to direction (twinLHS if the direction is DirEq).

The twinAt @'Both variant will crash with an __IMPOSSIBLE__ in the presence of non-single twin type.

The @'Compat variant is meant to be used for cases where the code has not been adapted yet (e.g. cubical) It will crash with an __UNIMPLEMENTED__ in the presence of a non-single twin type. It should disappear before merging this pull request.

The right-inverse of twinAt is asTwin:

asTwin :: Type -> TwinT

A twin context

The envContext in TCEnv now has the following type:

data Context_ = Empty
              | Entry (ISet ProblemId) (Dom (Name, TwinT)) Context_

twinAt @'LHS  :: Context_ -> [Dom (Name, Type)]
twinAt @'RHS  :: Context_ -> [Dom (Name, Type)]
twinAt @'Both :: Context_ -> [Dom (Name, Type)]

The last one will crash if any of the variables in the context is not of single type, as.

Given Entry pids a ctx, we have that:

• Each side of a is well typed in the corresponding side of ctx. (E.g. twinAt @'LHS ctx ⊢ twinAt @'LHS a type).

• pids contains the union of all the twinPids in both a and ctx.

This means that, once all the problems in pids are solved, the type a is equivalent to twinAt @'Both a.

Running computations under different sides of the context

With this infrastructure in place, it remains to make sure that each part of the conversion algorithm runs on the appropriate side of the context.

Ideally, we would have two different environments: one with the standard context with single-typed variables, for reduction etc, and one with twin variables, for conversion. However, the current system has a lot of interdependency between these parts: for instance, the conversion machinery is used to check type equality during reduction.

The following functions modify the envContext so that it only has the required side:

switchSide :: forall s a m. (HetSideIsType s, MonadTCEnv m) => m a -> m a
switchSide = unsafeModifyContext {- IdS -} (asTwin . twinAt @s) 

onSide :: forall s a m b. (MonadAddContext m, HetSideIsType s) => (a -> m b) -> Het s a -> m (Het s b)
onSide κ = switchSide @s . traverse κ

When using switchSide, the desired context side must be supplied explicitly (e.g. switchSide @s).

The latter uses the type annotation "s" to automatically switch to the appropriate context.

Viewing twin types

One advantage of twin types vs. replacing them by an uninterpreted constant is that one can still inspect them safely:

data TypeView_ =
    TPi (Dom TwinT) (Abs TwinT)
  | TDefRecordEta QName Defn (TwinT' Args)
  | TLam
  | TLevel
  | TOther

typeView :: TypeViewM m => TwinT' Term -> m (TypeView_)

This allows us to unify Π-types, curry context variables, eta-expand terms and more even if twin types are involved. Crucially, this doesn't require the use of anti-unification.

Instantiating metavariables

To ensure that metavariables are instantiated only with terms of the appropriate type, we check that all pertinent twins types in the context (that is, those whose

For more details of how this works, check López Juan and Danielsson (2020)