Generalised unification for FreeScoped terms

[fizruk]

This generalizes ideas implemented in Rzk.Free.Syntax.FreeScoped.Unification2:

• Previously we assumed that the target language has some sort of lambda abstraction and application. This was limiting since we sometimes want several kinds of "lambdas" or applications. Now we only ask the user to provide shapeGuesses which tells us valid shape guesses for meta variables. E.g. when we see the term ?M1 t we know that we want ?M1 = λx.?M2[x] (where ?M2[x] is a fresh meta variable applied to x). The user provides only these simple guesses, and the algorithm picks up on everything else.

• We are now relying on data types a la carte, and provide basic extension functionality (adding language features) via f :+: g. We have corresponding instances for all important type classes. Although I'm sure they are a bit far from being optimal in performance, I believe this can be tidied up and optimized later. For now our goal is providing working higher-order unification "for free" (meaning without extra coding, not necessarily without performance penalty).

• One important realisation (that I've arrived at today!) is that with this new formulation (where each metavariable is grouped with its arguments explicitly using MetaAppF) we always substitute metavariables for an implicit "lambda", represented with Scope Int (FreeScoped b t) v. The important bit is using v instead of UVar a v! Indeed, since all arguments are always packed with the meta variable, it is impossible to have a substitution of a metavariable with an open term! This simplified things a little and I was able to implement substituteGuesses finally and move further!

• Another experimental (but I think a good) idea is to split constraints into regular and ForAll (for when we enter/leave a scope). This should ensure that no bound variables leak into the outer scopes as it was with Unification2.

This is still work in progress, but most of the work seems to be done and I just need to finish this soon and test...

[fizruk]

Main unification algorithm seems complete with a few caveats:

1. In several places we go into "simplified mode" for scopes, which should be fine for most languages based on lambda calculus, but perhaps there are use cases where this will not be enough. In particular, we assume that "head" of a term in a flex-rigid constraint cannot be inside a scope.
2. The implementation requires significant testing and documentation. The types in Haskell ensure that we do not generate nonsense, but the algorithm still might not find a solution when required.
3. Currently there's no way to add a bound on the depth of search for the unification, so it might go into infinite loop.
4. Reduction now has to be defined for an extended language.

Here's a short demo for unification of untyped lambda terms:

stack repl

>>> :m Rzk.Free.Syntax.FreeScoped.ScopedUnification
>>> t1 = lamU "x" (lamU "y" (AppE (AppE (VarE (UMetaVar "f")) (VarE (UFreeVar "x"))) (VarE (UFreeVar "y"))))
>>> t2 = lamU "x" (lamU "y" (AppE (VarE (UFreeVar "y")) (AppE (VarE (UFreeVar "x")) (VarE (UFreeVar "y"))))) :: UTerm'
>>> t1
λx₁ → λx₂ → ?f x₁ x₂
>>> t2
λx₁ → λx₂ → x₂ (x₁ x₂)
>>> unifyUTerms'_ t1 t2
Just [(?f,λx₁ → λx₂ → x₂ (x₁ x₂))]

Here's all that is required from the user:

data TermF scope term
  = AppF term term
  | LamF scope
  deriving (Functor, Foldable, Traversable)

instance HigherOrderUnifiable TermF where
  shapeGuesses (AppF f x)  = AppF (f, [LamF ()]) (x, [])
  shapeGuesses t = noGuesses t
    where
      noGuesses = bimap (,[]) (,[])

  shapes = [ AppF HasHead NoHead ]

instance Reducible TermF where
  reduceInL = \case
    t@VarE{} -> t

    AppE f x ->
      case reduce f of
        LamE body -> reduce (Bound.instantiate1 x body)
        f'        -> AppE f' x
    t@LamE{} -> t

    t -> reduceInR t

The following should be inferred automatically (via Template Haskell or GHC.Generics):

-- ** Simple pattern synonyms

-- | A variable.
pattern Var :: a -> Term b a
pattern Var x = PureScoped x

-- | A \(\lambda\)-abstraction.
pattern Lam :: ScopedTerm b a -> Term b a
pattern Lam body = FreeScoped (LamF body)

-- | An application of one term to another.
pattern App :: Term b a -> Term b a -> Term b a
pattern App t1 t2 = FreeScoped (AppF t1 t2)

{-# COMPLETE Var, Lam, App #-}

-- | A variable.
pattern VarE :: a -> TermE ext b a
pattern VarE x = PureScoped x

-- | A \(\lambda\)-abstraction.
pattern LamE :: ScopedTermE ext b a -> TermE ext b a
pattern LamE body = FreeScoped (InL (LamF body))

-- | An application of one term to another.
pattern AppE :: TermE ext b a -> TermE ext b a -> TermE ext b a
pattern AppE t1 t2 = FreeScoped (InL (AppF t1 t2))

pattern ExtE :: ext (ScopedTermE ext b a) (TermE ext b a) -> TermE ext b a
pattern ExtE ext = FreeScoped (InR ext)

{-# COMPLETE VarE, LamE, AppE, ExtE #-}

instance Unifiable TermF where
  zipMatch (AppF f1 x1) (AppF f2 x2)
    = Just (AppF (Right (f1, f2)) (Right (x1, x2)))
  zipMatch (LamF body1) (LamF body2)
    = Just (LamF (Right (body1, body2)))
  zipMatch _ _ = Nothing