Safe Haskell | None |
---|---|
Language | Haskell2010 |
Unification algorithm for specializing datatype indices, as described in "Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2016).
This is the unification algorithm used for checking the left-hand side
of clauses (see Agda.TypeChecking.Rules.LHS
), coverage checking (see
Agda.TypeChecking.Coverage
) and indirectly also for interactive case
splitting (see Agda.Interaction.MakeCase
).
A unification problem (of type UnifyState
) consists of:
- A telescope
varTel
of free variables, some or all of which are flexible (as indicated byflexVars
). - A telescope
eqTel
containing the types of the equations. - Left- and right-hand sides for each equation:
varTel ⊢ eqLHS : eqTel
andvarTel ⊢ eqRHS : eqTel
.
The unification algorithm can end in three different ways:
(type UnificationResult
):
- A *positive success*
Unifies (tel, sigma, ps)
withtel ⊢ sigma : varTel
,tel ⊢ eqLHS [ varTel ↦ sigma ] ≡ eqRHS [ varTel ↦ sigma ] : eqTel
, andtel ⊢ ps : eqTel
. In this case,sigma;ps
is an *equivalence* between the telescopestel
andvarTel(eqLHS ≡ eqRHS)
. - A *negative success*
NoUnify err
means that a conflicting equation was found (e.g an equation between two distinct constructors or a cycle). - A *failure*
UnifyStuck err
means that the unifier got stuck.
The unification algorithm itself consists of two parts:
- A *unification strategy* takes a unification problem and produces a
list of suggested unification rules (of type
UnifyStep
). Strategies can be constructed by composing simpler strategies (see for example the definition ofcompleteStrategyAt
). - The *unification engine*
unifyStep
takes a unification rule and tries to apply it to the given state, writing the result to the UnifyOutput on a success.
The unification steps (of type UnifyStep
) are the following:
- *Deletion* removes a reflexive equation
u =?= v : a
if the left- and right-hand sideu
andv
are (definitionally) equal. This rule results in a failure if --without-K is enabled (see "Pattern Matching Without K" by Jesper Cockx, Dominique Devriese, and Frank Piessens (ICFP 2014). - *Solution* solves an equation if one side is (eta-equivalent to) a
flexible variable. In case both sides are flexible variables, the
unification strategy makes a choice according to the
chooseFlex
function inAgda.TypeChecking.Rules.LHS.Problem
. - *Injectivity* decomposes an equation of the form
c us =?= c vs : D pars is
wherec : Δc → D pars js
is a constructor of the inductive datatypeD
into a sequence of equationsus =?= vs : delta
. In caseD
is an indexed datatype, - higher-dimensional unification* is applied (see below).
- *Conflict* detects absurd equations of the form
c₁ us =?= c₂ vs : D pars is
wherec₁
andc₂
are two distinct constructors of the datatypeD
. - *Cycle* detects absurd equations of the form
x =?= v : D pars is
wherex
is a variable of the datatypeD
that occurs strongly rigid inv
. - *EtaExpandVar* eta-expands a single flexible variable
x : R
whereR
is a (eta-expandable) record type, replacing it by one variable for each field ofR
. - *EtaExpandEquation* eta-expands an equation
u =?= v : R
whereR
is a (eta-expandable) record type, replacing it by one equation for each field ofR
. The left- and right-hand sides of these equations are the projections ofu
andv
. - *LitConflict* detects absurd equations of the form
l₁ =?= l₂ : A
wherel₁
andl₂
are distinct literal terms. - *StripSizeSuc* simplifies an equation of the form
sizeSuc x =?= sizeSuc y : Size
tox =?= y : Size
. - *SkipIrrelevantEquation@ removes an equation between irrelevant terms.
- *TypeConInjectivity* decomposes an equation of the form
D us =?= D vs : Set i
whereD
is a datatype. This rule is only used if --injective-type-constructors is enabled.
Higher-dimensional unification (new, does not yet appear in any paper):
If an equation of the form c us =?= c vs : D pars is
is encountered where
c : Δc → D pars js
is a constructor of an indexed datatype
D pars : Φ → Set ℓ
, it is in general unsound to just simplify this
equation to us =?= vs : Δc
. For this reason, the injectivity rule in the
paper restricts the indices is
to be distinct variables that are bound in
the telescope eqTel
. But we can be more general by introducing new
variables ks
to the telescope eqTel
and equating these to is
:
Δ₁(x : D pars is)Δ₂
≃
Δ₁(ks : Φ)(x : D pars ks)(ps : is ≡Φ ks)Δ₂
Since ks
are distinct variables, it's now possible to apply injectivity
to the equation x
, resulting in the following new equation telescope:
Δ₁(ys : Δc)(ps : is ≡Φ js[Δc ↦ ys])Δ₂
Now we can solve the equations ps
by recursively calling the unification
algorithm with flexible variables Δ₁(ys : Δc)
. This is called
*higher-dimensional unification* since we are unifying equality proofs
rather than terms. If the higher-dimensional unification succeeds, the
resulting telescope serves as the new equation telescope for the original
unification problem.
Synopsis
- type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern])
- data UnificationResult' a
- data NoLeftInv
- = UnsupportedYet { }
- | Illegal { }
- | NoCubical
- | WithKEnabled
- | SplitOnStrict
- | SplitOnFlat
- | UnsupportedCxt
- unifyIndices' :: (PureTCM m, MonadError TCErr m) => Maybe NoLeftInv -> Telescope -> FlexibleVars -> Type -> Args -> Args -> m FullUnificationResult
- unifyIndices :: (PureTCM m, MonadBench m, BenchPhase m ~ Phase, MonadError TCErr m) => Maybe NoLeftInv -> Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnificationResult
Documentation
type UnificationResult = UnificationResult' (Telescope, PatternSubstitution, [NamedArg DeBruijnPattern]) Source #
Result of unifyIndices
.
data UnificationResult' a Source #
Unifies a | Unification succeeded. |
NoUnify NegativeUnification | Terms are not unifiable. |
UnifyBlocked Blocker | Unification got blocked on a metavariable |
UnifyStuck [UnificationFailure] | Some other error happened, unification got stuck. |
Instances
UnsupportedYet | |
Illegal | |
NoCubical | |
WithKEnabled | |
SplitOnStrict | splitting on a Strict Set. |
SplitOnFlat | splitting on a @♭ argument |
UnsupportedCxt |
:: (PureTCM m, MonadBench m, BenchPhase m ~ Phase, MonadError TCErr m) | |
=> Maybe NoLeftInv | Do we have a reason for not computing a left inverse? |
-> Telescope | gamma |
-> FlexibleVars | flex |
-> Type | a |
-> Args | us |
-> Args | vs |
-> m UnificationResult |
Unify indices.
In unifyIndices gamma flex a us vs
,
us
andvs
are the argument lists to unify, eliminating typea
.gamma
is the telescope of free variables inus
andvs
.flex
is the set of flexible (instantiable) variabes inus
andvs
.
The result is the most general unifier of us
and vs
.