eq

The eq function is the cannonical example of a polytypic function. Let's consider how eq looks for each of the datatypes introduced in the previous section.

For D and C the eq functions are the obvious implementations. We just present the types of the functions here:
eqD :: D $\rightarrow$D $\rightarrow$Bool
eqC :: C $\rightarrow$C $\rightarrow$Bool

For M and L the eq functions are again obvious, but require an auxilary equality function for testing the equality of the polymorphic data. We just present the types of the functions here:
eqM :: ($\alpha$ $\rightarrow$$\alpha$ $\rightarrow$Bool) $\rightarrow$M $\alpha$ $\rightarrow$M $\alpha$ $\rightarrow$Bool
eqL :: ($\alpha$ $\rightarrow$$\alpha$ $\rightarrow$Bool) $\rightarrow$L $\alpha$ $\rightarrow$L $\alpha$ $\rightarrow$Bool

For P and B the eq functions are fairly straightforward, but let's look at the implementation of eqB:
eqB eqa NilB NilB = True
eqB eqA NilB _ = False
eqB eqA _ NilB = False
eqB eqA (ConsB x xb) (ConsB y yb) = (eqa x y) $\wedge$ (eqB (eqB eqa) xb xy)
Note that with the recursive call to eqB, we are checking for the equality of xb and yb, which have the type Bush (Bush $\alpha$). Hence, the implementation of eqB requires polymorphic recursion, and requires explicit typing:
eqB :: ($\alpha$ $\rightarrow$$\alpha$ $\rightarrow$Bool) $\rightarrow$B $\alpha$ $\rightarrow$B $\alpha$ $\rightarrow$Bool

Finally, consider the implementation of eqG:
eqG eqf eqa (Branch x xg) (Branch y yg) = (eqa x y) $\wedge$ (eqf (eqG eqf eqa) xg yg)
That is, given a way to check the equality of $\mathcal{F}$ structures and of $\alpha$ values, we can check the equality of a G $\mathcal{F}$ $\alpha$ datatype by comparing the two values of type $\alpha$ with eqa and by comparing the two structures of type $\mathcal{F}$ (G $\mathcal{F}$ $\alpha$) with eqf. At a minimum, we type eqG as follows:
eqG :: ((G $\mathcal{F}$ $\alpha$ $\rightarrow$G $\mathcal{F}$ $\alpha$ $\rightarrow$Bool) $\rightarrow$ $\mathcal{F}$ (G $\mathcal{F}$ $\alpha$) $\rightarrow$ $\mathcal{F}$ (G $\mathcal{F}$ $\alpha$) $\rightarrow$Bool) $\rightarrow$ ($\alpha$ $\rightarrow$$\alpha$ $\rightarrow$Bool) $\rightarrow$ G $\mathcal{F}$ $\alpha$ $\rightarrow$ G $\mathcal{F}$ $\alpha$ $\rightarrow$Bool
However, for reasons that won't become apparent until a later talk, it makes sense to type eqG as follows, using rank-2 polymorphism:
eqG :: ($\forall \beta$. ($\beta$ $\rightarrow$$\beta$ $\rightarrow$Bool) $\rightarrow$ $\mathcal{F}$ $\beta$ $\rightarrow$ $\mathcal{F}$ $\beta$ $\rightarrow$Bool) $\rightarrow$ ($\alpha$ $\rightarrow$$\alpha$ $\rightarrow$Bool) $\rightarrow$ G $\mathcal{F}$ $\alpha$ $\rightarrow$ G $\mathcal{F}$ $\alpha$ $\rightarrow$Bool

Some similarities among all of these functions:

• ``structural'' equality
• zero or more ``sub-equality'' functions
• $\wedge$ together equality results for sub-components