#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by ekmett): I can provide much larger examples. =) The problem with the middle solution is it doesn't scale out when the cycles get much harder and doesn't work at all when reasoning becomes inductive and doesn't self-terminate like this. When I have things like (simplified): * the field of fractions for an integral domain is a field. * every field is an integral domain. * the field of fractions of any field is itself. * polynomial over an integral domain are an integral domain * polynomials over a field form a field * the field of rational functions over a field is the same as the field of fractions of the ring of polynomials over that field So if we take "Rat" to be the field of rational functions over a field and you take Poly to be the ring of polynomials over a type, and Frac to be the field of fractions over an integral domain, these all get a very incestuous relationship. Frac (Frac a) ~ Frac a For every field Frac a ~ a but we need to know that integral domain implies integral domain for the field of fractions, this one is nice because it terminates. Frac (Frac a) ~ Frac a is given to us, so GHC is happy, and we can stop with the middle technique I mentioned. But the field of rational functions over a given field is a new field, and the field of rational functions over that is also a new field, so I can't use a finite version of the middle trick to supply this information. I have to instead turn to the second trick. So here I only get a few hundred lines of code. For a few thousand, we need to turn to category theory. =) https://github.com/ekmett/hask/blob/d945e09779bd0b63af05e649b142cde6477856f0... defines a sufficiently nice version of a category that we can do some real category theory, well, most of a category, because of these sort of circular definitions. {{{ class Category' (p :: i -> i -> *) }}} Now I can define functors between categories with something that includes: {{{ class (Category' (Dom f), Category' (Cod f)) => Functor (f :: i -> j) where type Dom f :: i -> i -> * type Cod f :: j -> j -> * }}} Then I have to iterate the middle trick twice to get to the real definition I want. Given the convenience alias {{{ class (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor (p :: i -> j -> k) instance (Functor p, Cod p ~ Nat (Dom2 p) (Cod2 p), Category' (Dom2 p), Category' (Cod2 p)) => Bifunctor (p :: i -> j -> k) }}} we can step one step further to tying off the notion of a Category {{{ class (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p instance (Category' p, Bifunctor p, Dom p ~ Op p, p ~ Op (Dom p), Cod p ~ Nat p (->), Dom2 p ~ p, Cod2 p ~ (->)) => Category'' p }}} and then finally give: {{{ -- | The full definition for a (locally-small) category. class (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p instance (Category'' p, Category'' (Op p), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category p }}} Here what we really want is: {{{ data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where Nat :: ( FunctorOf p q f , FunctorOf p q g ) => { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g class (Functor p, Dom p ~ Op p, Cod p ~ Nat p (->), p ~ Op (Op p), Ob p ~ Ob (Op p)) => Category (p :: i -> i -> *) where type Ob p :: i -> Constraint class (Category (Dom p), Category (Cod p)) => Functor (p :: i -> j) type Dom f :: i -> i -> * type Cod f :: j -> j -> * class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a } type family Op (p :: i -> i -> *) :: i -> i -> * where Op (Yoneda p) = p Op p = Yoneda p }}} but this small definition is (deliberately) circular in several ways. These are needed to express that every category can be used itself as a functor from its opposite category to the category of natural transformations from it to "Hask", which is the definition of the Yoneda lemma. It expresses the fact that we can do all of category theory in Haskell "curried" because everything is sufficiently locally small. This is critical to avoid the need to define bifunctors explicitly, but rather let us view a bifunctor as a functor to a functor category. Even once I have that machinery in place it is indeed a "few thousand lines of code hacking around limitations" til I get to https://github.com/ekmett/hask/blob/d945e09779bd0b63af05e649b142cde6477856f0... wherein the well known claim that "a monad is a monoid in the category of endofunctors, what is the problem" gets used as code. Much of it is spent opening up data constructors in local scope to get at instances, many of which must exist canonically, but I have to carry them around here because I can't make these sorts of circular claims more directly. Consider: https://github.com/ekmett/hask/blob/d945e09779bd0b63af05e649b142cde6477856f0... Those lines are mostly opening dictionaries. the line I want is the one at the end. What I have to write is 4 lines of preamble to state the real theorem. This project choked on its own complexity after this theorem: https://github.com/ekmett/hask/blob/d945e09779bd0b63af05e649b142cde6477856f0... caused everyone involve to have a collective aneurysm. ;) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by simonpj): OK, well I don't understand much of comment:2, but I'll take it on trust. What is difficult about recursive superclasses? I'll use the example in the Description. * '''"Given" superclasses'''. Suppose we have {{{ f :: C a => .... }}} and on f's RHS we have the constraint `(D a)`. GHC treats `(C a)` as a "given", and then adds all of `C`'s superclasses as "givens" too, and their superclasses, and so on; in case they are useful to prove the constraints arising from f's RHS. For example, `(D a)` might be a distant superclass of `(C a)`. If there are an infinite number of superclasses, this "add all superclasses" idea isn't going to work. I expect you'll say "well, in my case `Frac (Frac a) ~ Frac a`, so the second-level superclass is the same as the first". That may be true, but it requires somewhat-sophisticated reasoning; a kind of fixpoint calculation. I can see it might be possible, but the penalty for (the programmer) getting it wrong is severe; the type checker goes into a loop. * '''"Wanted" superclasses'''.Similarly, for "wanted" constraints we fluff up the superclases in case one of them has a functional dependency that will help us make progress. * '''Instance declarations'''. In an instance declaration we must cough up a witness for the superclass. This part might not be too hard. At lesat in the monomorphic cases you give, like `instance IntegralDomain Integer`, we seek an instance for `IntegralDomain (Frac Integer)`, which is just `IntegralDomain Rational`, and we have that. Again things could go badly wrong, but I think the existing superclass code might "just work". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by simonpj): Hmm. In all the examples you give, one can statically enumerate the transitive superclasses. Fro example in comment:5 we have {{{ Ring r ==> Module r r ==> Group r ==> Module r Integer ==> Group r -- STOP Ring Integer ==> Module Integer Integer ==> Group Integer ==> Module Integer -- STOP Ring Integer -- STOP Ring r -- STOP }}} Here I am writing {{{ Class a b ==> Superclass1 a b Superclass2 a b }}} with nesting to describe nested superclasses. `STOP` means that we've seen this before, so going on generating superclasses will reveal nothing new. Notice that I reach a fixpoint for every instantiation of `r`. Indeed I can precompute all these transitive superclasses, once and for all, at the class declaration. Similarly for `IntegralDomain`, but I have to use the equalities: class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a)) => IntegralDomain a where {{{ ID a ==> Frac (Frac a) ~ Frac a -- (1) Fractional (Frac a) ==> superclasses of Fractional ID (Frac a) ==> Frac (Frac (Frac a)) ~ Frac (Frac a) -- STOP; a consequence of (1) ID (Frac (Frac a) -- rewrite with (1) = ID (Frac a) -- STOP Fractional (Frac (Frac a)) -- rewrite with (1) = Fractional (Frac a) -- STOP }}} In the examples you care about, does the collection of superclasses always statically terminate in this way? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): I think that every example I have does indeed terminate in a finite manner in this way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10318 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => indexed-types/should_compile/T10318 Comment: OK, this is done! Edward: can you try it out? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: infoneeded Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10318 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => infoneeded -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10318: Cycles in class declaration (via superclasses) sometimes make sense. -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: infoneeded Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T10318 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): I'm looking forward to being able to remove all sorts of helper classes and trickery from my `algebra` and `hask` packages -- and closing out a bunch of longstanding issues. (My tests all worked as expected.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10318#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler