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.