[GHC] #10318: Cycles in class declaration (via superclasses) sometimes make sense.

[GHC]

#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/src/Hask/Category.hs#L68

 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/src/Hask/Tensor/Compose.hs#L134

 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/src/Hask/Tensor/Compose.hs#L104

 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/src/Hask/Tensor/Day.hs#L46

 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