Want to see a magic trick? Pick a function, any function:

Watch closely…​

A good candidate for equational reasoning?

## A rose by any other name

How do we automatically discover a theorem for any function?

foo :: [a] -> [a]

Suppose foo "schooled" == "shoe". What is foo "SCHOOLED"?

It must be "SHOE". The function foo has black-box access to the elements of its input list, that is, it can only perform some combination of rearranging or duplicating or discarding the given letters. If foo were able to exploit some property of characters then it would instead have type [Char] → [Char]. We relabeled the input, so the output must be exactly what it was before, except relabeled.

We could go beyond letters. If we replace each input letter with its ASCII code, we obtain "shoe" in ASCII. In other words, given a relabeling function:

relabel :: Char -> Int

we have the rewrite rule, or theorem:

foo (map relabel xs) = map relabel (foo xs)

There’s nothing special about Char and Int. This holds for any relabel function from any type to any other type.

We can conjure up a theorem from any type signature. (We’re really just specializing the parametricity theorem to a particular case.) The resulting theorem is nontrivial if a type variable is present.

Let’s walk through some examples. Suppose we have a function:

bar :: a - > b -> a

There are two type variables, which may have independent relabeling functions. So for any functions relabelA, relabelB we have:

bar (relabelA x) (relabelB y) = relabelA (bar x y)

The left-hand side relabels before applying bar, while the right-hand side applies bar before relabeling.

It’s slightly tougher when an argument is a function:

baz :: (a -> b -> b) -> b -> [a] -> b

We can relabel the other arguments easily enough; for any functions relabelA, relabelB we have:

baz f' (relabelB y) (map relabelA ys) = relabelB (baz f x ys)

where we still must address the relationship between f' and f.

Recursion is the answer. We equate the relabeled output of f with the output of f' run on relabeled inputs:

f' (relabelA x) (relabelB y) = relabelB (f x y)

If this equality holds, then our first equality holds.

More generally, if there are function arguments within function arguments, then we recurse deeper.

The code below automates the above for a type system limited to type constants, type variables, functions, and lists. We refer to lists as functors to stress we can replace any list with any Functor instance.

The theorize function returns a list of equalities, the head of which is true whenever all of the equalities in the tail are true.

Lists of functions are irksome. We expediently introduce lambdas rather than figuring out how to write the relabeling condition with combinators.

module Main where
import Base
import System
import Charser
foreign export ccall "main" main
{- GHC edition:
{-# LANGUAGE FlexibleContexts, LambdaCase #-}
import Text.Megaparsec hiding (State)
import Text.Megaparsec.Char
import Data.List
type Charser = Parsec () String
-}

infixr 5 :->
data Type = TFunctor Type | TC String | TV String | Type :-> Type deriving Show
data Expr = Var String | Expr :@ Expr | Lam String Expr
data Theorem = Expr := Expr

data Scratch = Scratch  -- Scratch space.
{ varCount :: Int
, conds :: [Theorem]
}

theorize :: String -> Type -> [Theorem]
theorize fun t = evalState (theorize' (Var fun) (Var fun) t)
$Scratch 0 [] theorize' :: Expr -> Expr -> Type -> State Scratch [Theorem] theorize' lhs rhs t = case t of a :-> b -> do v <- genVar v' <- relabel id a v theorize' (lhs :@ v') (rhs :@ v) b _ -> do r <- relabel id t rhs scr <- get pure$ (lhs := r) : conds scr

relabel :: (Expr -> Expr) -> Type -> Expr -> State Scratch Expr
relabel f t v = case t of
TC _ -> pure v
TV s -> pure $f (Var$ s <> "R") :@ v
TFunctor u -> relabel (f . (Var "fmap" :@)) u v
_ :-> _ -> do
v' <- case v of
Var s -> pure $Var$ s <> "'"
_ -> genVar
let
((vL, postL), (vR, postR)) = case f (Var "") of
Var "" -> ((v', id), (v, id))
_ -> (functored v', functored v)
functored vv = (Var "l", \x -> f (Lam "l" x) :@ vv)
s0 <- get
let
((xL := xR):xt, s1) = runState (theorize' vL vR t)
$Scratch (varCount s0) [] put s0 { conds = conds s0 <> ((postL xL := postR xR):xt) , varCount = varCount s1 } pure v' genVar :: State Scratch Expr genVar = do s <- get let n = varCount s put s { varCount = n + 1 } pure$ Var $'x' : show n Product and coproduct types are hopefully only a little more work, but may mean some shortcuts we took are unavailable. That leaves the boring stuff: parsing types, pretty-printing theorems, interfacing with this webpage, and so on. instance Show Expr where show = \case Var s -> s a :@ b -> show a <> " " <> showR b Lam s x -> "(\\" <> s <> " -> " <> show x <> ")" where showR x = case x of _ :@ _ -> "(" <> show x <> ")" _ -> show x instance Show Theorem where show (l := r) = show l <> " = " <> show r decl :: Charser (String, Type) decl = (,) <$> sp ((:) <$> lowerChar <*> many alphaNumChar) <*> (sp (string "::") *> typ) where typ = foldr1 (:->) <$>
((:) <$> typeAtom <*> many (sp (string "->") *> typeAtom)) typeAtom = typeCon <|> typeVar <|> between (spch '[') (spch ']') (TFunctor <$> typ)
<|> between (spch '(') (spch ')') typ
typeCon = TC <$> sp ((:) <$> upperChar <*> many alphaNumChar)
typeVar = TV <$> sp ((:) <$> lowerChar <*> many alphaNumChar)
sp :: Charser a -> Charser a
sp   = (<* space)
spch = sp . char

gvs :: Type -> [String]
gvs = \case
TC _ -> []
TV v -> [v]
TFunctor t -> gvs t
x :-> y -> gvs x union gvs y

pretty :: Type -> [Theorem] -> String
pretty t (thm:conds) = "Theorem: For all functions "
<> unwords ((<> "R") <$> gvs t) <> ",\n" <> case conds of [] -> " " <> show thm _ -> concat [ "If:\n" , unlines$ ("  " <>) . show <$> conds , "then:\n " , show thm ] go :: String -> String go s = case parse (decl <* eof) "" s of Left err -> show err Right (s, t) -> pretty t$ theorize s t

main :: IO ()
main = interact go