Mixing and Matching Variables

Tags coco, haskell, programming, research
Target Audience Haskell programmers.
Epistemic Status I wrote this memo to work out how to implement CoCo. So this all works and is, mostly, still implemented like this.

Thanks to the two prior memos in this series, we can gen­erate schemas and pro­duce a set of terms from a schema, and we can eval­uate these terms and store the res­ults of so do­ing, so that we can later com­pare schemas.

The problem is: given two terms (from dif­ferent schemas) and their res­ults, how do we com­pare them? For in­stance, con­sider we have two terms:

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

Which fulfil the prop­erty that when the z in term1 is equal to the y in term2, the terms have the same res­ult. Each term in­tro­duces its own en­vir­on­ment vari­able namespace, so what we want is a pro­jec­tion into a shared namespace, in which we can reason about the equal­ities we de­sire.

We can sim­plify the problem a little by not chan­ging the number of unique vari­ables in­side a term, only re­stricting ourselves to identi­fying (or not) vari­ables across terms. Here are some pos­sible pro­jec­tions 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 pro­duce a set of all such type-­cor­rect pro­jec­tions.

This memo is a lit­erate Haskell file (though con­fus­ingly I mix source with ex­amples, which are NOT syn­tax-high­lighted), and we’ll need this:

{-# LAN­GUAGE LambdaCase #-}

Aside: The These type

I re­cently read a blog post en­titled These, Align, and Cross­walk about safely zip­ping (or mer­ging) data struc­tures. 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 val­ues.
data These a b
  = This a
  | That b
  | These a b
  de­riving Show

I don’t think I need any­thing else from the these pack­age, so I’ll just in­line that defin­i­tion there. It turns out to be ex­actly the thing we need!

Finding All Re­nam­ings

Firstly, we need a rep­res­ent­a­tion of terms, from which we can ex­tract vari­ables. We don’t ac­tu­ally need any­thing other than vari­able names and types, so let’s just go for that:

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

Our chal­lenge is to find two func­tions:

pro­jec­tions :: Term -> Term -> [[(These Name Name, Type)]]
re­naming    :: (Type -> Name) -> [(These Name Name, Type)] -> ([(­Name, Name)], [(­Name, Name)])

Where a These String String value rep­res­ents a type-­cor­rect re­naming of vari­ables:

-- | Find all type-­cor­rect ways of as­so­ci­ating vari­ables.
pro­jec­tions :: Term -> Term -> [[(These Name Name, Type)]]
pro­jec­tions t1 [] = [[(This v, ty) | (v, ty) <- t1]]
pro­jec­tions [] t2 = [[(That v, ty) | (v, ty) <- t2]]
pro­jec­tions ((vL, tyL):t1) t2 =
 concat [map ((These vL vR, tyL) :) (pro­jec­tions t1 (filter (/=x) t2)) | x@(vR, tyR) <- t2, tyL == tyR]
 ++ map ((This vL, tyL) :) (pro­jec­tions t1 t2)

By ap­pending the concat to the map we can in­stead gen­erate in order from most gen­eral (most This/That us­age) to least gen­eral (most These us­age).

Now that we have pro­jec­tions, we can pro­duce con­sistent re­nam­ings:

-- | Given a pro­jec­tion into a common namespace, pro­duce a con­sistent vari­able re­nam­ing. Vari­ables
-- of the same type, after the first, will have a number ap­pended starting from 1.
re­naming :: (Type -> Name) -> [(These Name Name, Type)] -> ([(Name, Name)], [(Name, Name)])
re­naming varf = go [] ([], []) where
  go e x ((these, ty):rest) =
    let name = varf ty
    in re­name e x name (maybe 0 (+1) $ lookup name e) these rest
  go e x [] = x

  re­name 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 com­bined:

-- | Find all con­sistent re­nam­ings of a pair of terms.
re­nam­ings :: (Type -> Name) -> Term -> Term -> [([(Name, Name)], [(Name, Name)])]
re­nam­ings varf t1 t2 = map (re­naming varf) (pro­jec­tions t1 t2)

My only re­gret is that I found no use for the fan­cier func­tions in the these pack­age.