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.


About Brent

Associate 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:

    Are you aware of any connections in this direction?

    Wonderful graphics and exposition :)

  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’.

    Otherwise a very readable paper!

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.