Bifunctorial category

[dimecon]

So I took a guess on what the bifunctorial category stage expressions and laws should look like. How does it look to you? How can I tell if I have exhausted all the laws we need and if they are the correct ones?

module Bifunctor {ℓ} (A : Set ℓ) (C : A → A → Set ℓ) (_,,_ : A → A → A) where

  infixr 80 _∥_
  infixr 70 _<>_

  data Exp : A → A → Set ℓ where
    embed : ∀ {a a′}
         → C a a′
         → Exp a a′
    id    : ∀ {a}
         → Exp a a
    _<>_   : ∀ {a a′ a′′}
          → Exp a a′ → Exp a′ a′′ → Exp a a′′
    _∥_ : ∀ {a a′ b b′}
      → Exp a a′ → Exp b b′ → Exp (a ,, b) (a′ ,, b′)

  data EquivExp : ∀ {a a′}
                     → Exp a a′
                     → Exp a a′
                     → Set ℓ where
    equiv-refl : ∀ {a a′}
               → {e : Exp a a′}
               → EquivExp e e
    equiv-sym : ∀ {a a′}
              → {e₁ e₂ : Exp a a′}
              → EquivExp e₁ e₂
              → EquivExp e₂ e₁
    equiv-trans : ∀ {a a′}
                → {e₁ e₂ e₃ : Exp a a′}
                → EquivExp e₁ e₂
                → EquivExp e₂ e₃
                → EquivExp e₁ e₃
    equiv-cong : ∀ {a a′ a′′}
               → {e₁  e₂  : Exp a a′}
               → {e₁′ e₂′ : Exp a′ a′′}
               → EquivExp e₁  e₂
               → EquivExp e₁′ e₂′
               → EquivExp (e₁ <> e₁′) (e₂ <> e₂′)
    left-id-id : ∀ {a a′}
               → {e : Exp a a′}
               → EquivExp (id <> e) e
    right-id-id : ∀ {a a′}
                → {e : Exp a a′}
                → EquivExp (e <> id) e
    assoc-<> : ∀ {a a′ a′′ a′′′}
            → (e   : Exp a a′)
            → (e′  : Exp a′ a′′)
            → (e′′  : Exp a′′ a′′′)
            → EquivExp ((e <> e′) <> e′′) (e <> (e′ <> e′′))
    bimap-id : ∀ {a b}
            → EquivExp (id {a} ∥ id {b}) (id {a ,, b})
    bimap-<> : ∀ {a b c} {a′ b′ c′}
            → (f : Exp a b) → (g : Exp b c)
            → (h : Exp a′ b′) → (i : Exp b′ c′)
            → EquivExp ((f <> g) ∥ (h <> i)) (f ∥ h <> g ∥ i)

And should the free bicategory look like what we usually have, or do we need something more with bimap?

  infixr 6 _∷_
  data FreeBiCat : A → A → Set ℓ where
    nil : ∀ {a} → FreeBiCat a a
    _∷_ : ∀ {a a′ a′′} → C a a′ → FreeBiCat a′ a′′ → FreeBiCat a  a′′

or should we additionally have something like:

_||_ : C a a' -> C b b'
    -> FreeBiCat a' a'' -> FreeBiCat b' b'' -> FreeBiCat (a ,, b) (a'' ,, b'')

?

[gelisam]

I don't know how to confirm that a set of laws is sufficient, but here's my reasoning as I'm trying to find laws you might have missed.

1. Did you cover all the combinations? You have _∥_ with id, and _∥_ with _<>_... how about _∥_ with itself?
2. _∥_ with itself would be something like f ∥ (g ∥ h), so maybe some kind of associativity law? Nah, we're not at the semigroupoidal level yet.
3. Are the existing combinations sufficient? You cover id ∥ id, but does anything special happen when one side is id and the other isn't?
4. Aha! (f ∥ id) <> (id ∥ g) is equivalent to f ∥ g and to (id ∥ g) <> (f ∥ id). That's an extra law which I don't think follows from the ones you already have.
5. Or does it? (f ∥ id) <> (id ∥ g) is equivalent to (f <> id) ∥ (id <> g) by bimap-<>, which in turn is equivalent to f ∥ g, and the same logic applies to (id ∥ g) <> (f ∥ id). So that's not an extra law.
6. Oh, but wait, I just used the law (f <> id) = f inside an _∥_, that's not covered by your laws! You have equiv-cong, but it should probably be called cong-<>, and you also need to add cong-∥.

I can't think of any other ways to combine the operators, so I think that's it! If this cong-∥ you've missed isn't a big deal, we probably would have figured it out while writing the soundess and completeness proofs. I'm more concerned about equivalences like (4) above, which could have caused us to pick the wrong free structure and to succeed at proving it correct simply because we might have had the wrong mental model of which equivalence classes we're trying to represent.

[dimecon]

Ah, I see, this makes sense. I'm stuck on finding the proper free structure. So I assume this is part of it:

  infixr 6 _∷_
  data FreeBiCat : A → A → Set ℓ where
    nil : ∀ {a} → FreeBiCat a a
    _∷_ : ∀ {a a′ a′′} → C a a′ → FreeBiCat a′ a′′ → FreeBiCat a  a′′

But I think we also need something to correspond to _∥_, such as

bimap : ∀ {a a′ b b′}
        → FreeBiCat a a′ → FreeBiCat b b′ -> FreeBiCat (a ,, b) (a′ ,, b′)

But then it isn't clear how concatenation would work. Am I on the right track?

[gelisam]

I'm working on a longer response, but I think it will have to be much more complicated than that.

[dimecon]

Okay, thanks for letting me know!

[gelisam]

I drew a few diagrams, it helps me to reason about this kind of things.

First, let's consider the simpler case in which all of the Cs apply to atomic types, never pairs, and they never modify their input type either. So the whole transformation also keeps its original type, and looks like this:

Each square is a C, squares on the same row are joined by _∥_, and rows are composed using _<>_. That's the row-based encoding. Or, equivalently, we could use a column-based encoding, in which squares on the same column are joined by _<>_, and columns are composed using _∥_.

Squares can move freely up and down (as long as they don't move over one another) without breaking equivalence, but they cannot move left nor right. So if we want a canonical representation, we should push all of the block as high (or alternatively as low) as possible. With the row-based encoding, this would mean annotating each horizontal position with a boolean indicating whether id has been in this position already, and if so, all further elements at this position must also be id (otherwise the element would be a square which could have been higher). That's moderately complicated. With the column-based encoding, there are no restrictions: each column can contain any number of squares, and that's it. Clearly, we should use the column-based encoding.

Next, let's consider a slightly more complicated case in which Cs still never modify their input types, but are now allowed to apply on pairs. Pictorially, this means we now have a mix of squares and rectangles:

There is a row-based encoding which isn't that bad, but let's continue with the column-based encoding. Let's focus on the widest rectangles:

(the colors don't mean anything, I simply ran out of green)

This is simple: a list consisting of an arbitrary number of rectangles, with maybe some stuff in-between. Let's add the next-biggest rectangles:

The stuff in-between has the same structure as the outer structure. Cool, a recursive type definition, looks like we're on the right track!

One difficulty is that we're only allowed to nest an inner structure if the type is a pair. I guess we could use universes or something to pattern-match on the type, but I'm not sure I'd be able to convert such a complicated encoding back into Haskell. So instead I was thinking that there would be two constructors for the inner structure: one called none which would represent id and would work for both pairs and non-pairs, and one called both which would contains the inner structure and would only type check with pairs.

Except now we have two representations for an inner id: the none constructor and a both with two empty lists. So I guess they should be non-empty lists. But that would make it impossible to represent something like f ∥ id! We want to allow id, f ∥ id, id ∥ g, and f ∥ g, but not id ∥ id. Okay, so how about 4 constructors: none, first, second, and both. That should work!

More complications to follow, I have to go :)

[gelisam]

I just realized I wrote (a || b) instead of (a ,, b) in all my drawings, sorry for the confusion!

[gelisam]

The next difficulty is that the notion of "non-empty" I mentioned earlier is more complicated than for a non-empty list. I wrote a lot about said difficulties, but the rabbit hole went quite deep, and so in order to preserve our sanity, I recommend we choose a different path. Let's use a universe of types after all, it will be much simpler! I'll figure out how to translate that to Haskell later.

So here's the type universe I had in mind:

data Type : Set where
  Atom : A -> Type
  Pair : Type -> Type -> Type

Hmm, come to think about it, it's not really a universe, because it doesn't describe a type, it describes an A. So it's more like a version of A and _,,_ on which we can pattern match to figure out if a type is a pair or not. This will be very helpful!

C (and everything else) should be indexed by two Types instead of by two As. This will allow our free structure to use a different shape depending on the type: we can use a nested structure for pairs and an ordinary list for atoms (recall that input types are still being left untouched in the output):

data FreeBiCat : Type -> Type -> Set where
  nil-atom :: FreeBiCat (Atom a) (Atom a)
  cons-atom :: C (Atom a) (Atom a)
            -> FreeBiCat (Atom a) (Atom a)
            -> FreeBiCat (Atom a) (Atom a)

  nil-pair :: FreeBiCat t1 t1
           -> FreeBiCat t2 t2
           -> FreeBiCat (Pair t1 t2) (Pair t1 t2)
  cons-pair :: FreeBiCat t1 t1'
            -> FreeBiCat t2 t2'
            -> C (Pair t1' t2') (Pair t1'' t2'')
            -> FreeBiCat (Pair t1'' t2'') (Pair t1''' t2''')
            -> FreeBiCat (Pair t1 t2) (Pair t1''' t2''')

With this definition, we no longer need to worry about having distinct representations for id and id || id: if the type is an atom, it will be nil-atom, if it's a pair of atoms, it will be nil-pair nil-atom nil-atom, and so on. Morphisms of different types are not equivalent.

[gelisam]

All right, the final complication: let's allow the Cs to modify their input type. Rectangles become trapezoids, in which the output type may be wider or narrower than the input type (the width represents the number of atoms in the type):

Not only do the trapezoids change the types, the recursive ... parts can change it too. However, while the trapezoids can change it from any type to any type, the recursive ... parts can only change it from a pair to another pair, because the two nested towers don't interact with each other.

And if the type is an atom, like in the third ... from the top in the picture? Well, now that I think about it, there should be no recursive bit at all in there! Whichever operation would appear next, it applies to the full width of the top-level type, a'''', so it should be a top-level trapezoid, not a nested operation.

So, combining all that, I believe the structure for a free bifunctorial category is:

data FreeBiCat : Type -> Type -> Set where
  nil-atom :: FreeBiCat (Atom a) (Atom a)
  nil-pair :: FreeBiCat t1 t1'
           -> FreeBiCat t2 t2'
           -> FreeBiCat (Pair t1 t2) (Pair t1' t2')
  cons-atom :: C (Atom a) t'
            -> FreeBiCat t' t''
            -> FreeBiCat (Atom a) t''
  cons-pair :: FreeBiCat t1 t1'
            -> FreeBiCat t2 t2'
            -> C (Pair t1' t2') t''
            -> FreeBiCat t'' t'''
            -> FreeBiCat (Pair t1 t2) t'''

[gelisam]

Hmm, renaming the constructors, it seems like you weren't too far after all! You've got a good intuition for this!

data FreeBiCat : Type -> Type -> Set where
  nil :: FreeBiCat (Atom a) (Atom a)
  _||_ :: FreeBiCat t1 t1'
       -> FreeBiCat t2 t2'
       -> FreeBiCat (Pair t1 t2) (Pair t1' t2')
  _∷_ :: C (Atom a) t'
      -> FreeBiCat t' t''
      -> FreeBiCat (Atom a) t''
  cons-pair :: FreeBiCat t1 t1'
            -> FreeBiCat t2 t2'
            -> C (Pair t1' t2') t''
            -> FreeBiCat t'' t'''
            -> FreeBiCat (Pair t1 t2) t'''

[dimecon]

Wow, thanks for this. I've been reading through it multiple times trying to gain an intuition for what you are doing in the drawings, but I'm not really getting it. 1) Could you explain more about what the drawings are depicting and how they connect to FreeBiCat?

2) Why don't we want to allow id ∥ id?

3) For cons-pair, could

cons-pair :: FBC a a' -> FBC b b' -> C (a' , b') c -> FBC (a , b) c

work? (FBC = FreeBiCat)

How about

cons-pair :: C c (a , b) -> FBC a a' -> FBC b b' -> FBC c (a' , b')

Or why can't we mimic cons-atom = _::_ like this?:

cons-pair :: C (a , b) c -> FBC c c' -> FBC (a , b) c'

[gelisam]

1) Could you explain more about what the drawings are depicting and how they connect to FreeBiCat?

I drew the diagrams to help me develop an intuition for what an example value of type FreeBiCat might look like. This in turn allowed me to figure out how FreeBiCat should be defined.

It is simultaneously the image of an Exp and the image of the corresponding FreeBiCat: I'm trying to find a way to draw an Exp such that the differences between two equivalent Exps are invisible in the drawing. For example, for a monoid, the expressions (x*y)*z and x*(y*z), are equivalent, so the notation x*y*z is more appropriate since the lack of parentheses erases the distinction between the two expressions. An even better notation is xyz, using blank space to represent mempty, because now x*mempty*y and x*y are also represented the same.

Since bifunctorial categories have two operators, _<>_ and _∥_, I can't use the same trick of replacing the operators with juxtaposition, because it would then be ambiguous which juxtaposition represents which operator. At least, I can't do that in a 1D expression. In 2D, however, I can use horizontal juxtaposition to represent _∥_ and vertical juxtaposition to represent _<>_. This has the additional benefit that (f <> g) ∥ (h <> i) and (f ∥ h) <> (g ∥ i) are both represented as

+---++---+
| f || h |
+---++---+
+---++---+
| g || i |
+---++---+

Despite this trick, there are still a few equivalences which I could not accurately represent in my drawings. For example, (id <> f) ∥ (g <> h), f ∥ (g <> h) and (f <> id) ∥ (g <> h) are all equivalent, but they have three different pictorial representations:

     +---+
     | g |
     +---+
+---++---+
| f || h |
+---++---+

     +---+
+---+| g |
| f |+---+
+---++---+
     | h |
     +---+

+---++---+
| f || g |
+---++---+
     +---+
     | g |
     +---+

So that's what I meant when I said that squares were free to move up and down but not left and right: the drawing necessarily chooses a position for f, but in order to see those three diagrams as equivalent, we should imaging that f is loose and can freely move along a vertical track. And we should consider that two diagrams are equivalent when its blocks are on the same tracks, not just when they are at the exact same positions.

2) Why don't we want to allow id ∥ id?

There should be one FreeBiCat value per equivalence class. So since id and id ∥ id are equivalent, we want to make sure that they are both represented by the same FreeBiCat value. What I said was:

We want to allow id, f ∥ id, id ∥ g, and f ∥ g, but not id ∥ id.

What I should perhaps have said instead is that we want separate FreeBiCat values for id, f ∥ id, id ∥ g, and f ∥ g, but we don't want a fourth separate value for id ∥ id, we want to reuse the same one as for id.

(I'll answer (3) later...)

[gelisam]

3) For cons-pair, could [...] work? How about [...]? Or why can't we mimic cons-atom = _::_ like this?: [...]

Each of those alternative definitions would break the alternation of inner structures and rectangles. Let's consider a simpler example: suppose I wanted to model a list of Strings separated by Ints. So I want to be able represent ["hello"], ["foo", 42, "bar"], and ["foo", 1, "bar", 2, "baz"], but not [], ["foo", 1, 2, "bar"], nor ["foo", 1, "bar", 2]. I'd use this type:

data AlternatingList where
  nil :: String -> AlternatingList
  cons :: String -> Int -> AlternatingList -> AlternatingList

This way I can represent ["hello"] as nil "hello", ["foo", 42, "bar"] as cons "foo" 42 (nil "bar"), and ["foo", 1, "bar", 2, "baz"] as cons "foo" 1 (cons "bar" 2 (nil "baz")).

In this simpler setting, the changes you suggest are, respectively:

-- cons-pair :: FBC a a' -> FBC b b' -> C (a' , b') c -> FBC (a , b) c
data AlternatingList where
  nil :: String -> AlternatingList
  cons :: String -> Int -> AlternatingList

["foo", 42] is allowed, but shouldn't be. ["foo", 1, "bar"] cannot be represented.

-- cons-pair :: C c (a , b) -> FBC a a' -> FBC b b' -> FBC c (a' , b')
data AlternatingList where
  nil :: String -> AlternatingList
  cons :: Int -> String -> AlternatingList

[1, "foo", "bar"] is allowed, but shouldn't be. ["foo", 1, "bar"] cannot be represented.

-- cons-pair :: C (a , b) c -> FBC c c' -> FBC (a , b) c'
data AlternatingList where
  nil :: String -> AlternatingList
  cons :: Int -> AlternatingList -> AlternatingList

[1, 2, "bar"] is allowed, but shouldn't be. ["foo", 1, "bar"] cannot be represented.

Similarly, I want a list of inner structures (that is, a pair of nested FreeBiCat values indexed by smaller types) separated by rectangles (that is, Cs indexed by the whole type). So instead of String, I use FBC a a' and FBC b b', and instead of Int, I use C (Pair a b) (Pair a' b'):

data FBC a a' where
  nil-pair : FBC a a' -> FBC b b' -> FBC (a, b) (a', b')
  cons-pair : FBC a a' -> FBC b b' -> C (a', b') (a'', b'') -> FBC (a'', b'') (a''', b''') -> FBC (a, b) (a''', b''')

Plus a few more complications to account for Cs which take atoms as input or output.

[dimecon]

Okay, thanks for bearing with me. Let me make sure I understand something about the drawings. What is (a , (b , c)) || (d , e) in the "trapezoid" drawings (I switched from _,,_ to _,_)? Is (a , (b , c)) || (d , e) the input type to the shapes (Cs) below it? And should the || there also be a ,? If not, I don't understand how to interpret it. I thought that _||_'s were only represented with vertical composition.

[dimecon]

For

    nil-pair : ∀ {a a′ b b′}
            → FreeBiCat a a′ → FreeBiCat b b′ → FreeBiCat (a , b) (a′ , b′)

I am trying to define the nil-pair case for _++_:

_++_ : ∀ {a a′ a′′} → FreeBiCat a a′ → FreeBiCat a′ a′′ → FreeBiCat a a′′
  nil-atom ++ y = y
  nil-pair f g ++ h = {!!}
  cons-atom f g ++ h = cons-atom f (g ++ h)
  cons-pair f g h i ++ j = cons-pair f g h (i ++ j)

The only thing I can see to do is

  nil-pair f g ++ h = cons-pair f g {0} h

Now {0} has goal C (a' , b') (a' , b'), but I don't see how to produce one of these.

Should the type of nil-pair rather be

nil-pair : ∀ {a b} → FreeBiCat (a , b) (a , b)

(then finishing _++_ is easy) or is there something wrong with that?

[gelisam]

Okay, thanks for bearing with me.

And thanks for your interest! Agda and category theory aren't very common interests among my peers, and so I really appreciate having someone with whom I can discuss these things :)

What is (a , (b , c)) || (d , e) in the "trapezoid" drawings

The green type at the top is the type of the input of the whole expression, and the blue types above and below each trapezoid is the input and output type of each C. For consistency, I guess I should add another green type at the very bottom.

And should the || there also be a ,?

Oops! You're right, it should be a ,.

[gelisam]

Should the type of nil-pair rather be [...] and then I can easily finish _++_. Or is there something wrong with that?

Same kind of counter-example as usual:

-- nil-pair : ∀ {a b} → FreeBiCat (a , b) (a , b)
data AlternatingList where
  nil :: AlternatingList
  cons :: String -> Int -> AlternatingList

["foo", 42] is allowed, but shouldn't be. ["foo", 1, "bar"] cannot be represented. Or, back in FreeBiCat-land, it's f <> (g || h) which cannot be represented.

The only thing I can see to do is

nil-pair f g ++ h = cons-pair f g {0} h

That doesn't seem right. Think of the drawing: it has two towers at the very top, and now we want to extend both towers. Doing so might change the number of Cs in each tower, but it should not change the number of top-level Cs. So if there were zero (i.e., if h is a nil-pair), the result should still have zero, and if there was at least one (i.e. if h is a cons-pair), the result should still have at least one. I know this is unusual for an implementation of _++_, but for once, you need to pattern-match on h!

[dimecon]

Ah, okay, I'm starting to understand this!

How does this free representation of these expressions look?

One issue I'm running into is that I need to write redundant proofs for different cases of a and a' in for example here.

Not writing the proof for each case tells me that

exp→free f ++ exp→free g != exp→free (f <> g) 

which is strange and I can't figure out why it's true. I'm not sure if there is something subtle going on with the definition of exp→free or _++_, or something else. Any ideas?

[gelisam]

How does this free representation of these expressions look?

It looks slightly redundant. I'd use some auxiliary definitions and I'd define exp→free (embed f) and exp→free (id _) in terms of them:

nil : ∀ {a} → FreeBiCat a a                                              
_∷_ : ∀ {a a′ a′′} → C a a′ → FreeBiCat a′ a′′ → FreeBiCat a a′′

-- Why do I need to specify the implicit cases {atom x} {atom k} and {atom x} {a , b} if the proofs are the same? -- Doing {atom x} {_} or {atom x} or {atom x} {a′} doesn't work

Hmm, {_} works for me...

Playing around with the code, I see that the reason it works for me is because I've used the auxiliary nil and _∷_ definitions above! Moving your four exp→free ... (embed f) definitions to the end of the function works too. I think what's happening is that with an unknown Ty, agda doesn't know whether any of the first line matches, because it cannot successfully nor unsuccessfully pattern-match on the Ty part of the pattern. Which is silly, since f <> g clearly doesn't match with embed f and so of course the first line can be skipped, but oh well. The reason it works with the lines at the end is because this way it reaches the f <> g case before the cases which require a known Ty, and the reason it works with exp→free (embed f) = f ∷ nil is because I'm not pattern-matching on Ty yet, that will be done inside nil and _∷_.