Thanks to the two prior memos in this series, we can generate *schemas* and produce a set of *terms* from a schema, and we can evaluate these terms and store the results of so doing, so that we can later compare schemas.

The problem is: given two terms (from different schemas) and their results, how do we compare them? For instance, consider we have two terms:

```
term1 = f (x :: Int) (y :: Int) (z :: Bool)
term2 = g (x :: Int) (y :: Bool) (z :: Bool)
```

Which fulfil the property that when the `z`

in `term1`

is equal to the `y`

in `term2`

, the terms have the same result. Each term introduces its own environment variable namespace, so what we want is a projection into a shared namespace, in which we can reason about the equalities we desire.

We can simplify the problem a little by not changing the number of unique variables inside a term, only restricting ourselves to identifying (or not) variables across terms. Here are some possible projections of those terms:

```
f x1 y1 z1 =?= g x1 y2 z2
f x1 y1 z1 =?= g x2 z1 z2
f x1 y1 z1 =?= g x2 y2 z1
f x1 y1 z1 =?= g x2 y1 z2
and so on
```

So we want to produce a *set* of all such type-correct projections.

This memo is a literate Haskell file (though confusingly I mix source with examples, which are NOT syntax-highlighted), and we’ll need this:

```
{-# LANGUAGE LambdaCase #-}
```

## Aside: The `These`

type

I recently read a blog post entitled These, Align, and Crosswalk about safely zipping (or merging) data structures. The core of the blog post is the `These`

type, defined as so:

```
-- | The @These@ type is like 'Either', but also has the case for when we have both values.
data These a b
= This a
| That b
| These a b
deriving Show
```

I don’t *think* I need anything else from the these package, so I’ll just inline that definition there. It turns out to be exactly the thing we need!

## Finding All Renamings

Firstly, we need a representation of terms, from which we can extract variables. We don’t actually need anything other than variable names and types, so let’s just go for that:

```
type Name = String
type Type = Int
type Term = [(Name, Type)]
```

Our challenge is to find two functions:

```
projections :: Term -> Term -> [[(These Name Name, Type)]]
renaming :: (Type -> Name) -> [(These Name Name, Type)] -> ([(Name, Name)], [(Name, Name)])
```

Where a `These String String`

value represents a type-correct renaming of variables:

`This s`

means a variable from the left term is kept distinct from all variables in the right term.`That s`

means a variable from the right term is kept distinct from all variables in the left term.`These s1 s2`

means a variable from the left term is identified with a variable from the right term.

```
-- | Find all type-correct ways of associating variables.
projections :: Term -> Term -> [[(These Name Name, Type)]]
projections t1 [] = [[(This v, ty) | (v, ty) <- t1]]
projections [] t2 = [[(That v, ty) | (v, ty) <- t2]]
projections ((vL, tyL):t1) t2 =
concat [map ((These vL vR, tyL) :) (projections t1 (filter (/=x) t2)) | x@(vR, tyR) <- t2, tyL == tyR]
++ map ((This vL, tyL) :) (projections t1 t2)
```

By appending the `concat`

to the `map`

we can instead generate in order from most general (most `This`

/`That`

usage) to least general (most `These`

usage).

Now that we have projections, we can produce consistent renamings:

```
-- | Given a projection into a common namespace, produce a consistent variable renaming. Variables
-- of the same type, after the first, will have a number appended starting from 1.
renaming :: (Type -> Name) -> [(These Name Name, Type)] -> ([(Name, Name)], [(Name, Name)])
renaming varf = go [] ([], []) where
go e x ((these, ty):rest) =
let name = varf ty
in rename e x name (maybe 0 (+1) $ lookup name e) these rest
go e x [] = x
rename e ~(l, r) name n = let name' = if n == 0 then name else name ++ show n in \case
This vL -> go ((name, n):e) ((vL, name'):l, r)
That vR -> go ((name, n):e) (l, (vR, name'):r)
These vL vR -> go ((name, n):e) ((vL, name'):l, (vR, name'):r)
```

The two steps can be combined:

```
-- | Find all consistent renamings of a pair of terms.
renamings :: (Type -> Name) -> Term -> Term -> [([(Name, Name)], [(Name, Name)])]
renamings varf t1 t2 = map (renaming varf) (projections t1 t2)
```

My only regret is that I found no use for the fancier functions in the these package.