**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
#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]
product kinds, we have to curry the type constructors: `Fix_1 f1 f2 = Outl
(Fix