## New ICFP functional pearl on subtracting bijections

Kenny Foner and I have a paper accepted to ICFP on subtracting bijections. Here’s the basic problem: suppose you have a bijection $h$ between two sum types, $h : A + B \leftrightarrow A' +B'$, and another bijection $g : B \leftrightarrow B'$. Of course $A$ and $A'$ must have the same size, but can you construct an actual bijection $f$ between $A$ and $A'$?

This problem and its solution has been well-studied in the context of combinatorics; we were wondering what additional insight could be gained from a higher-level functional approach. You can get a preprint here.

Assistant Professor of Computer Science at Hendrix College. Functional programmer, mathematician, teacher, pianist, follower of Jesus.
This entry was posted in combinatorics, haskell, writing and tagged , , , , , . Bookmark the permalink.

### 5 Responses to New ICFP functional pearl on subtracting bijections

1. Anton says:

I’m a bit confused about the definition of compatibility (section 5): doesn’t this define usual function equality? I would expect compatibility to be something like “If f a = Just b1 and g a = Just b2, then b1 = b2”.

• Brent says:

You’re absolutely right, thanks for the correction! Not sure how I missed that. =) Fortunately it is not too late, we haven’t turned in the camera-ready version yet.

2. I only skimmed, but this proof structure feels a lot like schroder-bernstein: https://en.wikipedia.org/wiki/Schr%C3%B6der%E2%80%93Bernstein_theorem

Are you aware of any connections in this direction?

Wonderful graphics and exposition :)

• Brent says:

Yes, it does have a similar feel to it! I haven’t thought too much about the exact connection (if there is one).

3. Audun says:

In section 4, are you mixing A’ with B? I am thinking of the sentences about “recycling” elements which land in B. From the figure, it seems to me that it’s the elements that land in A’ that get recycled back to their original positions in A, while elements that land in B’ are carried on through the bijection until they land in A’.