Re: [GHC] #12369: data families shouldn't be required to have return kind *, data instances should

15 Oct 2016

      #12369: data families shouldn't be required to have return kind *, data instances
should
-------------------------------------+-------------------------------------
        Reporter:  ekmett            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Iceland_jack):

 Should it be

 {{{#!hs
 type FIX k = (* -> k) -> k

 data family Fix :: FIX k
 }}}

 which fits the type of `newtype Fix2 f a = In2 (f (Fix2 f a) a)`

 {{{#!hs
 Fix2 :: FIX (k -> Type)
 }}}

 or

 {{{#!hs
 type FIX k = (k -> k) -> k

 data family Fix :: FIX k
 }}}

 which fits `newtype Fix_ f a = In_ (f (Fix_ f) a)`'s type

 {{{#!hs
 Fix_ :: FIX (k -> Type)
 }}}

 I would be **very** interested if this somehow tied in with the example of
 a fixed point of mutually recursive types from
 [http://www.cs.ox.ac.uk/ralf.hinze/publications/SCP-78-11.pdf s]
...
**Definition 2.** In Haskell, mutually recursive types can be modelled
 as follows.
{{{#!hs
newtype Fix_1 f1 f2 = In_1 (f1 (Fix_1 f1 f2) (Fix_2 f1 f2))
newtype Fix_2 f1 f2 = In_2 (f2 (Fix_1 f1 f2) (Fix_2 f1 f2))
}}}
Since Haskell has no concept of pairs on the type level, that is, no
 product kinds, we have to curry the type constructors: `Fix_1 f1 f2 = Outl
 (Fix <f1, f2>)` and `Fix_2 f1 f2 = Outr (Fix <f1, f2>)`.
We can get close to an arrow in a product category

 {{{#!hs
 -- Beautiful definition btw
 data (×) :: Cat x -> Cat y -> Cat (x, y) where
   Prod :: c1 a a_
        -> c2 b b_
        -> (c1 × c2) '(a, b) '(a_, b_)
 }}}

 but the closest I've gotten to modelling an endofunctor over a product
 category

 {{{
 F <A, B> = <Nat × B, 1 + A × B>
 }}}

 is

 {{{#!hs
 type family
   F (pair :: (*, *)) :: (*, *) where
   F '(a, b) = '((Int, b), Either () (a, b))
 }}}

 and the desired `FixProd` would probably have a type like `((*, *) -> (*,
 *)) -> (*, *)` (kinds can probably be generalised)

 {{{#!hs
 newtype FixProd :: FIX (*, *) where
   FixProd :: ...
 }}}

 Except this requires a non-`Type` return kind, I appreciate any pointers
 and if having a value of type `(*, *)` might ever make sense

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12369#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler