Experimenting with Progressive Free structures

Hey folks! I’ve been playing with an idea lately and I’m curious what people think about it and whether it’s been done before.

For some background, the problem I’m solving is that I’m writing tools for interpreting Profunctors and Categories into diagrams, the Category and Profunctor typeclasses (and the Profunctor hierarchy) both provide useful and different control flows which I’d like to diagram.

Free structures are very nice for this sort of thing since you can then mix and match different interpreters to accomplish your goals, in my case I have an “evaluate” interpreter which runs things in (->) and a “diagram” interpreter which spits out a flowchart of the program.

My issue is that I’d like to use a Free Structure to represent arbitrary programs which might be evaluated into arbitrary profunctors. Some profunctors have a Category instance, but others don’t! I ran into an issue where I couldn’t easily share a Free structure between these cases without throwing away typesafety.

This isn’t an issue when free structures compose nicely, e.g. a Free Profunctor wrapping a Free Category, but I’m not even sure it’s possible in this case since the operations are very complected, and this approach doesn’t scale well when I also want OPTIONAL instances for Strong, Choice, Closed, Traversing, etc. in my free structure.

So here’s the approach I went with; it uses GADTs with a ‘sentinel’ datakind for each instance I may need.

It allows me to write generalized functions over the free type which specify exactly which instances they require the interpreter to provide, while remaining polymorphic over the others!

Using GADTs for this means that GHC can intelligently detect which cases a given interpreter actually needs to handle, so if your interpreter doesn’t support “Category” you can safely ignore that constructor.

It seems to work quite well, and actually has decent inference, but obviously suffers from the long list of instance sentinels.

Has anyone experimented with something like this before? I’m having fun playing around with it :slight_smile:

{-# 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

-- We can write different interpreters which require different levels of constraints!
-- This one requires everything:
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

-- This one interprets free profunctors which don't have a category!
-- GHC notices and actually disallows us from matching on `Compose`
runFreeProNoCategory :: (Strong p, Choice p) => (forall x y. c x y -> p x y) -> FreePro 'NoCategory str cho (->) c a b -> p a b
runFreeProNoCategory interp = \case
  Dimap l r fp -> (dimap l r (runFreeProNoCategory interp fp))
  LiftC c -> interp c
  First p -> first' (runFreeProNoCategory interp p)
  Left' p -> left' (runFreeProNoCategory interp p)

1 Like