'Progressive' Free profunctors!

FreeProfunctor.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
module Data.Profunctor.Free where

import Data.Profunctor
import Control.Category (Category, (>>>))

data IsCat =
      HasCategory
    | NoCategory

data IsStrong =
      HasStrong
    | NoStrong

data IsChoice =
      HasChoice
    | NoChoice

data FreePro (cat :: IsCat) (str :: IsStrong) (cho :: IsChoice) p c a b where
  Dimap :: (p a b) -> (p y z) -> (FreePro cat str cho p c b y) -> FreePro cat str cho p c a z
  First :: FreePro cat 'HasStrong cho p c a b -> FreePro cat 'HasStrong cho p c (a, x) (b, x)
  Left' :: FreePro cat str 'HasChoice p c a b -> FreePro cat str 'HasChoice p c (Either a x) (Either b x)
  LiftC :: c a b -> FreePro cat str cho p c a b
  Compose :: FreePro 'HasCategory str cho p c x y -> FreePro 'HasCategory str cho p c y z -> FreePro 'HasCategory str cho p c x z

runFreePro :: (Strong p, Choice p, Category p) => (forall x y. c x y -> p x y) -> FreePro cat str cho (->) c a b -> p a b
runFreePro interp = \case
  Dimap l r fp -> (dimap l r (runFreePro interp fp))
  LiftC c -> interp c
  First p -> first' (runFreePro interp p)
  Left' p -> left' (runFreePro interp p)
  Compose l r -> runFreePro interp l >>> runFreePro interp r