Generics.Simplistic.Unify

Constraint-based unification algorithm for Holes

Substitution

type Subst kappa fam phi = Map (Exists phi) (Exists (Holes kappa fam phi))

A substitution is but a map; the existential quantifiers are necessary to ensure we can reuse from Data.Map

Note that we must be able to compare Exists phi. This comparison needs to work heterogeneously and it must return EQ only when the contents are in fact equal. Even though we only need this instance for Data.Map

A typical example for phi is Const Int at, representing a variable. The Ord instance would then be:

instance Ord (Exists (Const Int)) where
  compare (Exists (Const x)) (Exists (Const y))
    = compare x y

substEmpty :: Subst kappa fam phi

Empty substitution

substInsert

Arguments

:: Ord (Exists phi)

=> Subst kappa fam phi

-> phi at

-> Holes kappa fam phi at

-> Subst kappa fam phi

Inserts a point in a substitution. Note how the index of phi must match the index of the term being inserted. This is important when looking up terms because we must unsafeCoerce the existential type variables to return.

Please, always use this insertion function; or, if you insert by hand, ensure thetype indices match.

substLkup

Arguments

:: Ord (Exists phi)

=> Subst kappa fam phi

-> phi at

-> Maybe (Holes kappa fam phi at)

Looks a value up in a substitution, see substInsert

substApply

Arguments

:: Ord (Exists phi)

=> Subst kappa fam phi

-> Holes kappa fam phi at

-> Holes kappa fam phi at

Applies a substitution to a term once; Variables not in the support of the substitution are left untouched.

Unification

data UnifyErr kappa fam phi :: * where

Unification can return succesfully or find either a OccursCheck failure or a SymbolClash failure.

Constructors

OccursCheck :: [Exists phi] -> UnifyErr kappa fam phi

The occurs-check fails when the variable in question occurs within the term its supposed to be unified with.

SymbolClash :: Holes kappa fam phi at -> Holes kappa fam phi at -> UnifyErr kappa fam phi

A symbol-clash is thrown when the head of the two terms is different and neither is a variabe.

unify

Arguments

:: (All Eq kappa, Ord (Exists phi), EqHO phi)

=> Holes kappa fam phi at

-> Holes kappa fam phi at

-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)

Attempts to unify two Holes

unify_

Arguments

:: (All Eq kappa, Ord (Exists phi), EqHO phi)

=> Holes kappa fam phi at

-> Holes kappa fam phi at

-> Maybe (Subst kappa fam phi)

Attempts to unify two Holes, but ignores which error happened when they could not be unified.

unifyWith

Arguments

:: (All Eq kappa, Ord (Exists phi), EqHO phi)

=> Subst kappa fam phi

Starting subst

-> Holes kappa fam phi at

-> Holes kappa fam phi at

-> Except (UnifyErr kappa fam phi) (Subst kappa fam phi)

Attempts to unify two Holes with an already existing substitution

minimize

Arguments

:: Ord (Exists phi)

=> Subst kappa fam phi

-> Either [Exists phi] (Subst kappa fam phi)

The minimization step performs the occurs check and removes unecessary steps, returning an idempodent substitution when successful. For example;

sigma = fromList
          [ (0 , bin 1 2)
          , (1 , bin 4 4) ]

Then, minimize sigma will return fromList [(0 , bin (bin 4 4) 2) , (1 , bin 4 4)] This returns Left vs if occurs-check fail for variables vs.