That&#39;s simple Tom.<br>Imagine the factorial function for Int written as a paramorphism:<br><br>type instance F Int = Either One<br><br>instance (Mu Int) where<br>&nbsp;&nbsp;&nbsp; inn (Left _) = 0<br>&nbsp;&nbsp;&nbsp; inn (Right n) = succ n<br>&nbsp;&nbsp;&nbsp; out 0 = Left ()<br>
&nbsp;&nbsp;&nbsp; out n = Right (pred n)<br><br>instance Functor (F Int) where<br>&nbsp;&nbsp;&nbsp; fmap _ (Left ()) = Left ()<br>&nbsp;&nbsp;&nbsp; fmap f (Right n) = Right (f n)<br><br>fact :: Int -&gt; Int<br>fact = para (const 1 \/ (uncurry (*)) . (id &gt;&lt; succ))<br>
<br>If we consider that the paramorphism is implemented as an hylomorphism, then an intermediate virtual type (d in the hylo definition) [Int]<br><br>If you test the constraints for d = [Int], a = Int and c = Int<br><br>F d c ~ F a (c,a)<br>
<br>F d a = F [Int] Int = Either One (Int,Int)<br>F a (c,a) = F Int (Int,Int) = Either One (Int,Int)<br><br>F d a ~ F a (a,a)<br><br>F d a = F a (a,a) -- pure substitution of the above case<br><br>Hope this helps.<br>Thanks again for you patience,<br>
hugo<br><br><br>