Unification based on unbound-generics.

Unification for unbound-generics

This package implements (first-order) unification by reusing the framework of unbound-generics.

To use it, declare your data types as usual, including the generically-derived instances for alpha-equivalence (Alpha) and substitution (Subst) from unbound-generics. In addition to those, ask for a new instance of Unify with the same arguments as Subst, that is, the type from which we build variables, and the type we want to unify.

The packages provides a function unify which works on a Unification monad. This monad is parametrized by the type we draw variables from. That means you can have as many types as you want, but there should be a single type of variables. In many cases the compiler fails to infer that argument to the Unification monad, so we recommend enabling TypeApplications for that matter.

The result of unify is either a single value which is an instance of both arguments, or a UnificationError. That error explains where the process has failed by a Path consisting of constructor, fields, and indices; and a cause.

This is an example in which Type is the one we draw variables from. Since we also use TypeConstructor inside the TyCon constructor, we also need to "request" to derive Unify Type TypeConstructor.

type TypeVar = Name Type

data Type = TyVar { var :: TypeVar }
          | TyFun { args :: [Type], ret :: Type }
          | TyCon { con :: TypeConstructor, args :: [Type] }
          deriving (Eq, Show, Generic, Typeable)

data TypeConstructor = TyConInt | TyConBool deriving (Eq, Show, Generic)

pattern TyInt, TyBool :: Type
pattern TyInt  = TyCon TyConInt []
pattern TyBool = TyCon TyConBool []

instance Alpha Type
instance Alpha TypeConstructor

instance Subst Type Type where
  isvar (TyVar v) = Just $ SubstName v
  isvar _ = Nothing
instance Subst Type TypeConstructor

instance Unify Type Type
instance Unify Type TypeConstructor

Here are some example runs, using the explicitly-typed version of runUnification to declare that we are using Type-variables. To create new variables we use the usual s2n function from unbound-generics.

>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyVar x] (TyVar x))
( Right (TyFun {args = [TyCon {con = TyConInt, args = []}], ret = TyCon {con = TyConInt, args = []}})
, fromList [(x,TyCon {con = TyConInt, args = []})] )

>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyBool] (TyVar x))
( Left ([PathConstructor "TyFun", PathSelector "ret", PathConstructor "TyCon", PathSelector "con"], DifferentConstructor)
, fromList [(x,TyCon {con = TyConBool, args = []})] )