Changing up the letters without changing the meaning

Learn
#1

Hi folks,

In Haskell Programming from First Principals, we are comparing the type signatures of the function composition operator and fmap:

(.) :: (b -> c) -> (a -> b) -> (a -> c)

fmap :: (a -> b) -> f a -> f b

The goal is to show that the type signatures are the same, and the exercise begins by changing the type variable names in fmap; 'a’s become 'b’s and 'b’s become 'c’s.

My problem with this approach is that, if we decompose the process into Step 1: Change the "a"s to "b"s, and then Step 2: change the "b"s to "c"s, you end up with a “wrong intermediate type”.

  1. fmap :: (a -> b) -> f a -> f b
  2. fmap :: (b -> b) -> f b -> f b

Now, you need to remember which "b"s are “original” and change only those to "c"s, and error-prone process.

My question is, is there a less error-prone process, one in which we don’t end up with a “wrong intermediate type”.

#2

I think it might be best to just make it clear that you apply a mapping from one set of variable names to another. Something like:

Go over all variables and look up the new name in this table:

 old | new 
===========
  a  |  b
-----------
  b  |  a
-----------
  f  |  f
#3

This is alpha conversion and you can find the two rules not to screw up on Wikipedia.

Routinely in math books you see multiple α-convesions in the same step, I guess care in choosing the intermediate variables is left to the reader, always converting one var at the time (in this case e.g. first «a to x», then «b to c», finally «x to b»).

3 Likes
#4

Can’t thank you enough for giving me a name I can now Google! :+1:

1 Like