{-# language DefaultSignatures, UndecidableInstances, GADTs, MultiWayIf, AllowAmbiguousTypes #-}
-- | Unification for @unbound-generics@
module Unbound.Generics.Unify (
-- * Main unification functions
unify', Unify(..),
-- ** Information about errors
UnificationError, UnificationErrorCause(..),
Path, PathElement(..),
-- * Unification as a monad
Unification(..),
-- ** Base implementation
UnificationM, runUnification,
-- ** Including fresh creation
UnificationFreshM, runUnificationFresh,
-- ** As a monad transformer
UnificationMT(..), runUnificationT,
-- * Generic methods
GUnify(..)
) where
import Data.Bifunctor
import Control.Monad (forM)
import Control.Monad.Trans.State
import Data.Functor.Identity
import Data.Map
import GHC.Generics
import Unbound.Generics.LocallyNameless
-- | Path to navigate to a unification error.
type UnificationError = (Path, UnificationErrorCause)
-- | Potential causes for unification errors.
data UnificationErrorCause where
OccursCheck :: (Name t) -> t -> UnificationErrorCause
DifferentConstructor :: UnificationErrorCause
DifferentListLength :: UnificationErrorCause
instance Show UnificationErrorCause where
show OccursCheck {} = "OccursCheck"
show DifferentConstructor = "DifferentConstructor"
show DifferentListLength = "DifferentListLength"
type Path = [PathElement]
-- | Ways to navigate within a value.
data PathElement
= PathConstructor String | PathSelector String | PathIndex Int
deriving (Eq, Show)
-- | Stateful storage of substitutions as required for unification.
--
-- The substitution operates only on terms and variables of type 't'.
class Monad m => Unification t m where
-- | Obtain the current substitution.
currentSubst :: m (Map (Name t) t)
-- | Add a new substitution.
recordSubst :: Name t -> t -> m ()
applySubst :: forall t a m. (Unification t m, Subst t a) => a -> m a
applySubst term = do
current <- currentSubst @t @m
pure $ foldlWithKey (\t v u -> subst v u t) term current
type UnificationM t = UnificationMT t Identity
type UnificationFreshM t = UnificationMT t FreshM
runUnification :: forall t a. UnificationM t a -> (a, Map (Name t) t)
runUnification action = runIdentity (runUnificationT action)
runUnificationFresh :: forall t a. UnificationFreshM t a -> (a, Map (Name t) t)
runUnificationFresh action = runFreshM (runUnificationT action)
runUnificationT :: forall t m a. Monad m => UnificationMT t m a -> m (a, Map (Name t) t)
runUnificationT action = runStateT (unUnificationMT action) empty
newtype UnificationMT t m a
= UnificationMT { unUnificationMT :: StateT (Map (Name t) t) m a }
deriving (Functor, Applicative, Monad)
instance (Monad m) => Unification t (UnificationMT t m) where
currentSubst = UnificationMT $ get
recordSubst v t = UnificationMT $ modify (insert v t)
instance (Fresh m) => Fresh (UnificationMT t m) where
fresh = UnificationMT . fresh
-- | Tries to unify two terms, giving back a common term, or a unification error.
--
-- This variant requires the terms to be of the same type 't' as the variables within them.
unify' :: forall t m. (Unification t m, Unify t t) => t -> t -> m (Either UnificationError t)
unify' = unify @t
-- | Declares the ability to unify values of type 'a' containing variables of type 't'.
class Subst t a => Unify t a where
-- | Tries to unify two terms, giving back a common term, or a unification error.
unify :: Unification t m => a -> a -> m (Either UnificationError a)
default unify :: forall m. (Generic a, GUnify t (Rep a), Unification t m)
=> a -> a -> m (Either UnificationError a)
unify x y = do
x' <- applySubst @t x
y' <- applySubst @t y
result <- unifyIsvar x' y'
case result of
Left e -> pure $ Left e
Right r -> Right <$> applySubst @t r
where
unifyIsvar x y
| Just (SubstName v1) <- isvar @t @a x
, Just (SubstName v2) <- isvar @t @a y
= if | v1 == v2 -> Right <$> applySubst @t x
| v1 < v2 -> do { recordSubst v1 y ; Right <$> applySubst @t x }
| otherwise -> do { recordSubst v2 x ; Right <$> applySubst @t y }
-- do occurs check!!
| Just (SubstName v) <- isvar @t @a x = do { recordSubst v y ; Right <$> applySubst @t x }
| Just (SubstName v) <- isvar @t @a y = do { recordSubst v x ; Right <$> applySubst @t y }
| otherwise = unify_ x y
unify_ :: a -> a -> m (Either UnificationError a)
unify_ x y = fmap to <$> gunify @t @(Rep a) @m (from x) (from y)
instance {-# overlaps #-} Unify t (Name t) where
unify = error "should have never arrived here"
-- required because otherwise strings are matched as lists
instance {-# overlaps #-} Unify t String where
unify x y
| x == y = pure $ Right x
| otherwise = pure $ Left ([], DifferentConstructor)
instance {-# overlaps #-} (Unify t a) => Unify t [a] where
unify xlst ylst
| length xlst /= length ylst = pure $ Left ([], DifferentListLength)
| otherwise = sequence <$> forM (zip3 [0 .. ] xlst ylst) (\(i, x, y) -> first (first (PathIndex i :)) <$> unify @t x y)
-- | Implementation of unification using @GHC.Generics@.
class GUnify t f where
gunify :: Unification t m => f a -> f a -> m (Either UnificationError (f a))
instance GUnify t U1 where
gunify _ _ = pure $ Right U1
instance (Unify t a) => GUnify t (K1 i a) where
gunify (K1 x) (K1 y) = fmap K1 <$> unify @t x y
instance GUnify t f => GUnify t (D1 d f) where
gunify (M1 x) (M1 y) = fmap M1 <$> gunify @t x y
instance (Constructor c, GUnify t f) => GUnify t (C1 c f) where
gunify c@(M1 x) (M1 y) = bimap (first (PathConstructor (conName c) :)) M1 <$> gunify @t x y
instance (Selector s, GUnify t f) => GUnify t (S1 s f) where
gunify c@(M1 x) (M1 y) =
case selName c of
"" -> fmap M1 <$> gunify @t x y
con -> bimap (first (PathSelector con :)) M1 <$> gunify @t x y
instance (GUnify t f, GUnify t g) => GUnify t (f :*: g) where
gunify (x1 :*: x2) (y1 :*: y2) = do
r1 <- gunify @t x1 y1
r2 <- gunify @t x2 y2
pure $ (:*:) <$> r1 <*> r2
instance (GUnify t f, GUnify t g) => GUnify t (f :+: g) where
gunify (R1 x) (R1 y) = fmap R1 <$> gunify @t x y
gunify (L1 x) (L1 y) = fmap L1 <$> gunify @t x y
gunify _ _ = pure $ Left ([], DifferentConstructor)