Opened 5 years ago
Last modified 7 months ago
#7259 new bug
Eta expansion of products in System FC
Reported by: | simonpj | Owned by: | simonpj |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.6.1 |
Keywords: | Cc: | Conor.McBride@…, nfrisby, eir@…, adamgundry, sweirich@…, ekmett@…, josef.svenningsson@…, wren@…, jstolarek, Iceland_jack | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
This ticket is to capture the ideas in these GHC-users threads: PolyKinds Aug 2012 and PolyKinds Sept 2012
- 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?
Type inference
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
where a:'(k1,k2)
, and we have a type instance like F '(a,b) = ...
Anything else?
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
[W] a~b
where a
and 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.
Fixing Any
- 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
reverse []
At what type should we instantiatereverse
and the empty list[]
? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at(Any *)
: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 argumentk
; because now(Any k1 ~ Any k2)
does not entail(k1~k2)
. See also the moduleGHC.TypeLits
inbase
.
We can't solve this by making
Any
to be an injective type family, because the use inTypeLits
uses it in a type-class instance, and you can't match on type families!
Change History (18)
comment:1 Changed 4 years ago by
Cc: | nfrisby added |
---|
comment:2 Changed 4 years ago by
Cc: | eir@… added |
---|
comment:3 Changed 4 years ago by
Milestone: | → 7.8.1 |
---|---|
Owner: | set to simonpj |
comment:4 Changed 4 years ago by
Cc: | adam.gundry@… added |
---|
I agree that Any
should be a type function: to pass kinds as arguments, the proxy workaround is the right thing for now, at least until we get explicit type/kind application.
Richard, I think your proposed constraint simplification is sound, but I don't really understand the advantage over Simon's version. You are introducing fresh (untouchable?) variables a1
and a2
instead of Fst a
and Snd a
, but they don't get you any further. It doesn't matter that Fst
and Snd
are not injective, because the point of the decomposition into Fst a ~ t1
and Snd a ~ t2
is not to solve for a
(which is untouchable anyway), but that we might be able to solve for t1
or t2
if one of them is a variable, or we might have other given constraints on the projections.
In general, adding support for eta to the constraint solver means it should never get stuck because an inhabitant of a pair (or other record) kind is not canonical. Certainly type family axioms F '(a, b) = t
should be applicable even if the argument is not a canonical pair, but typeclass instances exhibit the same behaviour. For example, given the definitions
class Foo (x :: '(a, b)) instance Foo '(a, b)
we should be able to solve class constraints like Foo t
using the existing instance.
comment:5 Changed 4 years ago by
I updated GHC.TypeLits
to avoid using Any
as a constructor, so now we should be able to convert it to a type function.
In a previous e-mail I mentioned some "sketchiness" that occurs when using Any
(in either form) with empty kinds. Here is an example to illustrate the issue:
data {-kind-} Empty data T (a :: Empty) = C deriving Show main = print C -- what is the type of C here?
The issue is that in main
: constructor C
is of type T Any
, with Any
of kind Empty
. However, kind Empty
has no members, so what does Any
refer to?
comment:6 Changed 4 years ago by
Cc: | Conor.McBride@… sweirich@… added |
---|
Re the sketchiness, is your worry the following?
- Even though the type
Empty
has no data constructors, there are terms with typeEmpty
, namely diverging ones, such asundefined :: Empty
. - But are there any types with kind
Empty
? You might think "no" since we don't have divergent type terms. But there is one, namely(Any Empty)
.
So, is that a problem? Adding Conor to the cc list.
comment:7 Changed 4 years ago by
Just by way of concrete example, here's the smallest example Edward wants to do:
{-# LANGUAGE PolyKinds, DataKinds, GADTs #-} import Prelude hiding (id, (.)) class Category (k :: x -> x -> *) where id :: k a a (.) :: k b c -> k a b -> k a c data P :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where P :: m a b -> n c d -> P m n '(a,c) '(b,d) instance (Category m, Category n) => Category (P m n) where -- id = P id id P lf rf . P lg rg = P (lf . lg) (rf . rg)
The addition of id there causes it to fail to typecheck, because refining the kind to (x,y)
doesn't let it know all types have the form '(a,b)
. It can't because Any
still exists as a distinguishable member of every kind, so such a refinement would (currently) be unsound.
When we try to build indexed monad transformers we wind up wanting to take product over their indices. Similar issues arise when trying to compute with collages of profunctors and other nifty theoretical toys that have proven quite useful in the lens
package.
comment:9 Changed 3 years ago by
Cc: | ekmett@… added |
---|
comment:10 Changed 2 years ago by
Milestone: | 7.10.1 → 7.12.1 |
---|
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
comment:11 Changed 2 years ago by
Cc: | adamgundry added; adam.gundry@… removed |
---|
It occurred to me in passing today that this would be a nice application of typechecker plugins. They should let us experiment with the type inference issues fairly easily.
comment:12 Changed 19 months ago by
Cc: | josef.svenningsson@… added |
---|
comment:13 Changed 19 months ago by
Josef and I chatted about this ticket at HIW today. Now that Any
is moved out of the way, it seems quite possible to revisit this. Shouldn't be too hard.
comment:15 Changed 19 months ago by
Cc: | wren@… added |
---|
comment:16 Changed 19 months ago by
Cc: | jstolarek added |
---|
comment:17 Changed 14 months ago by
Milestone: | 8.0.1 |
---|
comment:18 Changed 7 months ago by
Cc: | Iceland_jack added |
---|
Adding some discussion that happened on the email thread:
The axioms that Simon mentioned:
The last two axioms are the straightforward compilations of the type families
Fst
andSnd
-- nothing new is needed to create these. The first is the challenge and will require some type inference magic.When trying to solve
(where
a
is untouchable), Simon suggested simplifying toI don't think that's the right replacement. The next natural step would be decomposition, leading to
(Fst a ~ t1)
and(Snd a ~ t2)
, which would then get stuck, becauseFst
andSnd
aren't injective. So, I would say we needwhich would then decompose correctly. As I write this, I'm worried about that freshness condition... what if
a
appears multiple times in the type? We would either need to guarantee thata1
anda2
are the same each time, or create new[W]
constraints thata1 ~ a1'
, etc. But, maybe this is easier in practice than it seems. Type inference experts?Simon is a bit concerned about constraints like
where
a:'(k1,k2)
, and we have a type instance likeF '(a,b) = ...
.It seems to me that the proper eta-expansion (a ~ '(Fst a, Snd a)) would work here.
As for
Any
, (as Nick pointed out and Iavor elaborated) there is a workaround that Iavor and I can use involving the promoted version ofto make kind classes and such. So, I think it's OK to relegate
Any
to a type function. Objections?