Eta expansion of products in System FC
- We want to add eta-rules to FC. Sticking to pairs for now, that would amount to adding two new type functions (Fst, Snd), and three new, built-in axioms
axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a) axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
Generalising to arbitrary products looks feasible.
- Adding these axioms would make FC inconsistent, because
axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
and that has two different type constructors on each side. However, I think is readily solved: see below under "Fixing Any"
- Even in the absence of Any, it's not 100% obvious that adding the above eta axioms retains consistency of FC. I believe that Richard is volunteering to check this out. Right, Richard?
I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint
[W] (a:'(k1,ks)) ~ '( t1, t2 )
where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint
[W] '(Fst a, Snd a) ~ '( t1, t2)
Is that it? Or do we need more? I'm a bit concerned about constraints like
F a ~ e
a:'(k1,k2), and we have a type instance like
F '(a,b) = ...
I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint
b are both skolems of kind
'(k1,k2). If we eta-expand both we'll get two insoluble constraints
(Fst a ~ Fst b) and
(Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!
Someone pointed out that Agda grapples with this problem and we should talk to them.
- I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type family application on the left and a type constructor on the right.
I have implemented this change already... it seems like a good plan.
- Several people have asked why we need Any at all. Consider this source program
At what type should we instantiate
reverseand the empty list
? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at
reverse (Any *) ( (Any *))
Why is Any poly-kinded? Because the above ambiguity situation sometimes arises at other kinds.
- I'm betting that making Any into a family will mess up Richard's (entirely separate) use of
(Any k)as a proxy for a kind argument
k; because now
(Any k1 ~ Any k2)does not entail
(k1~k2). See also the module
We can't solve this by making
Any to be an injective type family, because the use in
TypeLits uses it in a type-class instance, and you can't match on type families!