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?