Almost obnoxious levels of duality in fixed-points.

Rec.hs

{-# LANGUAGE QuantifiedConstraints, BlockArguments, LambdaCase #-}

module Rec where

import Data.Functor.Product (Product(..))
import Data.Functor.Sum (Sum(..))
import Data.Kind (Type, Constraint)
import Control.Arrow ((&&&), (|||))


newtype LFP f = LFP (           forall x. (f x -> x) -> x           )
--      GFP f ~                 exists x. (x -> f x,    x)
newtype GFP f = GFP (forall r. (forall x. (x -> f x) -> x -> r) -> r)

fold   :: (f a -> a) -> LFP f -> a
unfold :: (a -> f a) -> a -> GFP f
fold     alg (LFP k) =           k   alg
unfold coalg      x  = GFP \k -> k coalg x

inL  :: Functor f => f (LFP f) ->    LFP f
outG :: Functor f =>    GFP f  -> f (GFP f)
inL       ft = LFP \alg -> alg . fmap (  fold   alg)         $ ft
outG (GFP k) = k \coalg ->       fmap (unfold coalg) . coalg

outL :: Functor f =>    LFP f  -> f (LFP f)
inG  :: Functor f => f (GFP f) ->    GFP f
outL =   fold (fmap inL )
inG  = unfold (fmap outG)

rec   :: Functor f => (f (LFP f, a)        -> a ) -> LFP f -> a
corec :: Functor f => (a -> f (Either (GFP f) a)) -> a -> GFP f
rec     alg = snd . fold (      inL . fmap fst &&&   alg)
corec coalg =     unfold (fmap Left . outG     ||| coalg) . Right


type f ~> g = forall x. f x -> g x

class HFunctor h where
  hmap :: Functor f => f ~> g -> h f ~> h g

type    LFPF :: ((Type -> Type) -> (Type -> Type)) -> (Type -> Type)
newtype LFPF h a = LFPF (forall f. Functor f => h f ~> f -> f a)
  deriving Functor

type    GFPF :: ((Type -> Type) -> (Type -> Type)) -> (Type -> Type)
newtype GFPF h a = GFPF
  (forall r. (forall f. Functor f => f ~> h f -> f a -> r) -> r)
  deriving Functor

foldF   :: Functor f => h f ~>   f -> LFPF h ~> f
unfoldF :: Functor f =>   f ~> h f -> f ~> GFPF h
foldF     alg (LFPF k) =            k   alg
unfoldF coalg       x  = GFPF \k -> k coalg x

inLF  :: HFunctor h => h (LFPF h) ~>    LFPF h
outGF :: HFunctor h =>    GFPF h  ~> h (GFPF h)
inLF        ft = LFPF \alg   -> alg (hmap (foldF     alg) ft)
outGF (GFPF k) = k  \coalg x ->      hmap (unfoldF coalg) (coalg x)

type FuncTrans h = forall f. Functor f => Functor (h f) :: Constraint

outLF :: (HFunctor h, FuncTrans h) =>    LFPF h  ~> h (LFPF h)
inGF  :: (HFunctor h, FuncTrans h) => h (GFPF h) ~>    GFPF h
outLF =   foldF (hmap inLF )
inGF  = unfoldF (hmap outGF)

recF
  :: (HFunctor h, Functor f)
  => h (Product (LFPF h) f) ~> f
  -> LFPF h                 ~> f
recF alg = fsnd . foldF (inLF . hmap ffst &&&~ alg)
  where
    ffst (Pair fa _) = fa
    fsnd (Pair _ ga) = ga
    (f &&&~ g) a = Pair (f a) (g a)
    infixr 3 &&&~

corecF
  :: (HFunctor h, Functor f)
  => f ~> h (Sum (GFPF h) f)
  -> f ~> GFPF h
corecF coalg = unfoldF (hmap InL . outGF |||~ coalg) . InR
  where
    f |||~ g = \case
      InL fa -> f fa
      InR ga -> g ga
    infixr 2 |||~


-- A use case where *FP does not suffice:

data DeepH f a
  = Empty
  | Leaf a
  | Deep (f a) (f (f a)) (f a)
  deriving Functor

instance HFunctor DeepH where
  hmap fg = \case
    Empty            -> Empty
    Leaf a           -> Leaf a
    Deep fa1 ffa fa2 -> Deep (fg fa1) (fg $ fmap fg ffa) (fg fa2)

type LDeep = LFPF DeepH

lempty :: LDeep a
lempty = inLF Empty

lleaf :: a -> LDeep a
lleaf a = inLF (Leaf a)

ldeep :: LDeep a -> LDeep (LDeep a) -> LDeep a -> LDeep a
ldeep d1 dd d2 = inLF (Deep d1 dd d2)


-- Even when *FP does suffice, *FPF is more appropriate when the fixed type
-- should be a Functor.
--
-- Below, both 'LList' and 'GList' are Functors as they should be, whereas an
-- instance for the more conventional 'LFP (ListF a)' is precluded by its form.

type LList = LFPF ListH
type GList = GFPF ListH

data ListH f a = Nil | Cons a (f a)
  deriving Functor

instance HFunctor ListH where
  hmap fg = \case
    Nil       -> Nil
    Cons a fa -> Cons a (fg fa)

lnil :: LList a
lnil = inLF Nil

lcons :: a -> LList a -> LList a
lcons a l = inLF (Cons a l)