Modeling monoidal coherence in Haskell

Oftentimes, whenever working with monoidal operators in Haskell (or in any other languages for that matter), I find myself asking "Wouldn't it be convenient if the language itself had support for the normalization of monoidal operations? Allowing us to work in something like a strict monoidal category?"

Recently, I had the idea that something similar to this (albeit, not exactly the same, as e.x. ((), a) and a will still be distinct types could be implemented in Haskell by using type families. To see what I mean, consider the following types:

-- From Control.Arrow
(***) :: a b c -> a b' c' -> a (b, b') (c, c')

x :: MyArrow () Int
y :: MyArrow String Int

Currently with this API, combining x and y with *** yields:

x *** y :: MyArrow ((),String) (Int,Int)

But from a "monoidal" perspective the type I would really want to see would be the isomorphic:

x *** y :: MyArrow String (Int,Int)

Whereas, to actually achieve this using the standard arrow combinators, one would need to write:

(\x -> ((), x)) ^>> (x *** y) :: MyArrow String (Int,Int)

Now, to get around this boilerplate (assuming we don't want to deal with this kind of book-keeping for simplifying monoidal types to a normal form), my idea was the use the type family:

type family Reduce (pi :: * -> * -> *) (u :: *) (x :: *) :: * where
  Reduce pi u (pi u x) = Reduce pi u x
  Reduce pi u (pi x u) = Reduce pi u x
  Reduce pi u (pi (pi x y) z) = Reduce pi u (pi 
    (Reduce pi u x) 
    (pi 
       (Reduce pi u y) 
       (Reduce pi u z)
    )
   )
  Reduce pi u x = x

Trying this out at the ghci repl, this seems to give me the correct "normalized" monoidal types:

> let x :: Reduce (,) () (((), Int), String) = undefined
> :t x
x :: (Int, [Char])

Great! So, the idea would be to re-write any combinator introducing a monoidal operation so that it applies the Reduce type family:

-- My version
(***) :: a b c -> a b' c' -> a (Reduce (,) () (b, b')) (Reduce (,) () (c, c'))

x :: MyArrow () Int
y :: MyArrow String Int
x *** y :: MyArrow String (Int, Int)

The issue now being, how do I write my version of (***)? I would need to do something like "pattern matching" on types. That's no good. So, next I tried to use type classes with associated types instead.

class Reducible (pi :: * -> * -> *) (u :: *) (x :: *) | pi -> u where
  type Reduce x :: *
  reduce :: x -> Reduce x
  unReduce :: Reduce x -> x

Alright, so now we have an associated Reduce type to apply the monoidal normalization to our types, but also some operations to actually write functions to and from the reduced reresentations. Next, I wrote a utility Monoidal typeclass supplying the monoidal coherence isomorphisms to facilitate implementing the Reducible typeclass:

class Monoidal pi u where
  lambdaR :: pi u x -> x
  lambdaRi :: x -> pi u x
  lambdaL :: pi x u -> x
  lambdaLi :: x -> pi x u
  assocR :: pi x (pi y z) -> pi (pi x y) z
  assocL :: pi (pi x y) z -> pi x (pi y z)

Now here is where the problem comes along. I define the first two instances corresponding to the cases for reducing monoidal units...

instance (Monoidal pi u, Reducible pi u x) => Reducible pi u (pi u x) where
  type Reduce (pi u x) = x
  reduce x = lambdaR x
  unReduce x = lambdaRi x

instance (Monoidal pi u, Reducible pi u x) => Reducible pi u (pi x u) where
  type Reduce (pi x u) = x
  reduce x = lambdaL x
  unReduce x = lambdaLi x

...and GHC tells me:

main.hs:18:8: error:
    Conflicting family instance declarations:
      Reduce (pi u x) = x -- Defined at main.hs:18:8
      Reduce (pi x u) = x -- Defined at main.hs:23:8
   |
18 |   type Reduce (pi u x) = x
   |

Now, the issue here seems to be the distinction between open and closed type families. As I understand it, associated types act like open type families, where what I had written before was a closed type family, and open type families have overlap restrictions (much like type classes).

I found an unresolved GHC issue which I think might be relevant here, but beyond that (as it is unclear if/when this will be implemented) -- are there any workarounds to this issue that will let me define my Reduce typeclass with reduce and unReduce functions in a released GHC version?

Recommended topics

Hot tags