Some notes on inductive families
--------------------------------
** Syntax
The syntax for patterns which are instantiated by type checking (instantiated
or dot patterns) is ".p". For instance,
subst .x x refl px = px
or
map .zero f [] = []
map .(suc n) f (x :: xs) = f x :: map n f xs
In the second example there's some subtle things. The n looks as though it's
bound in the dot pattern. This is impossible since the dot patterns will be
thrown away after type checking. What should happen is that the hidden argument
to _::_ gets the name n and that's where the binding happens.
This poses a problem for scope checking. The dot pattern can be an arbitrary
term, but it might contain unbound variables. The scope checker will have to
bind unbound variables. Maybe that's not a problem?
The problem is: how to implement scope checking without copy-pasting between the
ToAbstract instance and the BindToAbstract instance for expressions?
Generalising a bit does the trick.
Come to think of it, binding variables in dot patterns is a bad idea. It makes
the type checking much harder: how to type check a dot pattern (in which
context). So the cons case above will have to be one of these two:
map .(suc _) f (x :: xs) = f x :: map _ f xs
map .(suc n) f (_::_ {n} x xs) = f x :: map n f xs
** Type checking
Step 0: Type checking the datatype
Nothing strange. We just lift some of the previous restrictions on datatypes.
Step 1: Type checking the pattern
Two interesting differences from the ordinary type checking:
addFirstOrderMeta (α : A)
───────────────────────── same for dot patterns
Γ ⊢ _ : A --> Γ ⊢ α, α
c : Δ -> Θ -> D xs ss' Γ ⊢ ps : Θ[ts] --> Γ' ⊢ us, αs Γ' ⊢ ss = us : Θ[ts]
──────────────────────────────────────────────────────────────────────────────
Γ ⊢ c ps : D ts ss --> Γ' ⊢ c ts us, αs
Interaction between first order metas and η-expansion?
Suppose
data D : (N -> N) -> Set where
id : D (\x -> x)
h : (f : N -> N) -> D f -> ..
h _ id
Now we have to check α = \x -> x : N -> N which will trigger η-expansion and
we'll end up with α x = x : N which we can't solve.
We'll ignore this for now. Possible solution could be to distinguish between
variables introduced by η-expansion and variables bound in the pattern.
Step 2: Turn unsolved metas into bound variables
- make sure that there are no unsolved constraints from type checking the
patterns (if so, fail)
- we need to remember where the first order metas come from, or at least the
order in which they are generated, so type checking should produce a list of
first order metas
- how to get the context in the right order? explicit variables have been
added to the context but not implicit ones. we should probably make sure
that the final context is the right one (otherwise reduction will not work
properly).
- example:
f y _ (cons _ x xs)
the context after type checking is (y x : A)(xs : List A) with meta
variables (α β : N), where α := suc β. We'd want the final pattern to be
f y .(suc n) (cons n x xs)
and the context in the right hand side (y : A)(n : N)(x : A)(xs : List A).
Solution:
- pull out the context (y x : A)(xs : List A) and the meta context
(α := suc β : N)(β : N) and traverse the pattern again, building the right
context, instantiating uninstantiated metas to fresh variables.
Quick solution:
- re-type check the pattern when we know which patterns are dotted and which
are variables. This also gets rid of (some of) the tricky deBruijn
juggling that comes with the first-order metas.
- Problem: when we say
subst ._ _ refl
could this mean
subst x .x refl ?
Answer: no, an explicit underscore can never become dotted. But there is a
similar problem in
tail ._ (x :: xs)
Here we might instantiate the hidden length in the _::_ rather than the
dotted first argument. So we need to keep track of first-order metas that
'wants' to be instantiated, and instantiate those at higher priority than
others.
Why is this a problem? The user won't be able to tell (at least not easily)
that she got
tail n (_::_ .{n} x xs)
rather than
tail .n (_::_ {n} x xs)
The problem is rather an implementation problem. We want to check that
dotted patterns actually get instantiated, and give an error otherwise.
How would we distinguish this case from the bad cases?
Step 3: Type check dot patterns and compare to the inferred values
* after step 2 the context will be the correct one.
* where do we find the type to check against? look at the meta variables
generated during type checking
So,
- traverse the pattern with the list of meta-variables
- for each dot pattern,
+ look up the type of the corresponding meta
+ and check that it's equal to the meta-variable
A BETTER SOLUTION
─────────────────
Context splitting a la Thierry.
For each clause, generate a case tree. Each case is an operation on the context:
(case x of C ys : D ss -> t) corresponds to
(Δ₁, x : D ts, Δ₂) ─→ (Δ₁, ys : Γ, Δ₂[C ys/x])σ
where σ = unify(ss, ts)
So to type check a clause:
∙ generate case tree
∙ perform the context splitting (remembering the substitutions σ)
∙ verify that σ corresponds exactly to the dotted patterns
Questions:
∙ what is the unification algorithm?
∙ what argument to split on?
∙ first constructor pattern? Consider:
data D : Set -> Set where
nat : D Nat
bool : D Bool
f : (A : Set) -> A -> D A -> X
f .Nat zero nat = x
Here we can't split on zero first, since the type is A.
∙ first constructor pattern whose type is a datatype
error if there are constructor patterns left but no argument can be split
vim: tw=80 sts=2 sw=2 fo=tcq