Mixing and Matching Variables

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.