-- Required for Show instances {-# LANGUAGE FlexibleContexts, UndecidableInstances #-} -- Required more generally {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- -- ~ 2011.07.11 -- | -- Module : Control.Unification.Types -- Copyright : Copyright (c) 2007--2011 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : experimental -- Portability : semi-portable (MPTCs, fundeps,...) -- -- This module defines the classes and primitive types used by -- unification and related functions. ---------------------------------------------------------------- module Control.Unification.Types ( -- * Mutable terms MutTerm(..) , freeze , unfreeze -- * Errors , UnificationFailure(..) -- * Basic type classes , Unifiable(..) , Variable(..) , BindingMonad(..) -- * Weighted path compression , Rank(..) , RankedBindingMonad(..) ) where import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) import Data.Word (Word8) import Data.Functor.Fixedpoint (Fix(..)) import Data.Traversable (Traversable(..)) import Control.Applicative (Applicative(..), (<$>)) import Control.Monad.Error (Error(..)) ---------------------------------------------------------------- ---------------------------------------------------------------- -- | The type of terms generated by structures @t@ over variables -- @v@. The structure type should implement 'Unifiable' and the -- variable type should implement 'Variable'. The 'Show' instance -- doesn't show the constructors, for legibility. data MutTerm v t = MutVar !(v (MutTerm v t)) | MutTerm !(t (MutTerm v t)) instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) => Show (MutTerm v t) where showsPrec p (MutVar v) = showsPrec p v showsPrec p (MutTerm t) = showsPrec p t -- | /O(n)/. Embed a pure term as a mutable term. unfreeze :: (Functor t) => Fix t -> MutTerm v t unfreeze = MutTerm . fmap unfreeze . unFix -- | /O(n)/. Extract a pure term from a mutable term, or return -- @Nothing@ if the mutable term actually contains variables. N.B., -- this function is pure, so you should manually apply bindings -- before calling it. freeze :: (Traversable t) => MutTerm v t -> Maybe (Fix t) freeze (MutVar _) = Nothing freeze (MutTerm t) = Fix <$> mapM freeze t ---------------------------------------------------------------- -- TODO: provide zipper context so better error messages can be generated. -- -- | The possible failure modes that could be encountered in -- unification and related functions. While many of the functions -- could be given more accurate types if we used ad-hoc combinations -- of these constructors (i.e., because they can only throw one of -- the errors), the extra complexity is not considered worth it. data UnificationFailure v t = OccursIn (v (MutTerm v t)) (MutTerm v t) -- ^ A cyclic term was encountered (i.e., the variable -- occurs free in a term it would have to be bound to in -- order to succeed). Infinite terms like this are not -- generally acceptable, so we do not support them. In logic -- programming this should simply be treated as unification -- failure; in type checking this should result in a \"could -- not construct infinite type @a = Foo a@\" error. -- -- Note that since, by default, the library uses visited-sets -- instead of the occurs-check these errors will be thrown -- at the point where the cycle is dereferenced\/unrolled -- (e.g., when applying bindings), instead of at the time -- when the cycle is created. However, the arguments to -- this constructor should express the same context as if -- we had performed the occurs-check, in order for error -- messages to be intelligable. | TermMismatch (t (MutTerm v t)) (t (MutTerm v t)) -- ^ The top-most level of the terms do not match (according -- to 'zipMatch'). In logic programming this should simply -- be treated as unification failure; in type checking this -- should result in a \"could not match expected type @Foo@ -- with inferred type @Bar@\" error. | UnknownError String -- ^ Required for the @Error@ instance, which in turn is -- required to appease @ErrorT@ in the MTL. We do not use -- this anywhere. -- Can't derive this because it's an UndecidableInstance instance (Show (t (MutTerm v t)), Show (v (MutTerm v t))) => Show (UnificationFailure v t) where -- TODO: implement 'showsPrec' instead show (OccursIn v t) = "OccursIn ("++show v++") ("++show t++")" show (TermMismatch tl tr) = "TermMismatch ("++show tl++") ("++show tr++")" show (UnknownError msg) = "UnknownError: "++msg instance Error (UnificationFailure v t) where noMsg = UnknownError "" strMsg = UnknownError ---------------------------------------------------------------- -- | An implementation of syntactically unifiable structure. The -- @Traversable@ constraint is there because we also require terms -- to be functors and require the distributivity of 'sequence' or -- 'mapM'. class (Traversable t) => Unifiable t where -- | Perform one level of equality testing for terms. If the -- term constructors are unequal then return @Nothing@; if they -- are equal, then return the one-level spine filled with pairs -- of subterms to be recursively checked. zipMatch :: t a -> t b -> Maybe (t (a,b)) -- | An implementation of unification variables. Note that we do -- not require variables to be functors. Thus, it does not matter -- whether you give them vacuous functor instances, or use clever -- tricks like @CoYoneda STRef@ to give them real functor instances. class Variable v where -- | Determine whether two variables are equal /as variables/, -- without considering what they are bound to. The default -- implementation is: -- -- > eqVar x y = getVarID x == getVarID y eqVar :: v a -> v b -> Bool eqVar x y = getVarID x == getVarID y -- | Return a unique identifier for this variable, in order to -- support the use of visited-sets instead of occurs-checks. getVarID :: v a -> Int ---------------------------------------------------------------- -- | The basic class for generating, reading, and writing to bindings -- stored in a monad. These three functionalities could be split -- apart, but are combined in order to simplify contexts. Also, -- because most functions reading bindings will also perform path -- compression, there's no way to distinguish \"true\" mutation -- from mere path compression. -- -- The superclass constraints are there to simplify contexts, since -- we make the same assumptions everywhere we use @BindingMonad@. class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad v t m | m -> v t where -- | Given a variable pointing to @MutTerm v t@, return the -- term it's bound to, or @Nothing@ if the variable is unbound. lookupVar :: v (MutTerm v t) -> m (Maybe (MutTerm v t)) -- | Generate a new free variable guaranteed to be fresh in -- @m@. freeVar :: m (v (MutTerm v t)) -- | Generate a new variable (fresh in @m@) bound to the given -- term. The default implementation is: -- -- > newVar t = do { v <- freeVar ; bindVar v t ; return v } newVar :: MutTerm v t -> m (v (MutTerm v t)) newVar t = do { v <- freeVar ; bindVar v t ; return v } -- | Bind a variable to a term, overriding any previous binding. bindVar :: v (MutTerm v t) -> MutTerm v t -> m () ---------------------------------------------------------------- -- | The target of variables for 'RankedBindingMonad's. In order -- to support weighted path compression, each variable is bound to -- both another term (possibly) and also a \"rank\" which is related -- to the length of the variable chain to the term it's ultimately -- bound to. -- -- The rank can be at most @log V@, where @V@ is the total number -- of variables in the unification problem. Thus, A @Word8@ is -- sufficient for @2^(2^8)@ variables, which is far more than can -- be indexed by 'getVarID' even on 64-bit architectures. data Rank v t = Rank {-# UNPACK #-} !Word8 !(Maybe (MutTerm v t)) -- Can't derive this because it's an UndecidableInstance instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) => Show (Rank v t) where show (Rank n mb) = "Rank "++show n++" "++show mb -- TODO: flatten the Rank.Maybe.MutTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)? {- instance Monoid (Rank v t) where mempty = Rank 0 Nothing mappend (Rank l mb) (Rank r _) = Rank (max l r) mb -} -- | An advanced class for 'BindingMonad's which also support -- weighted path compression. The weightedness adds non-trivial -- implementation complications; so even though weighted path -- compression is asymptotically optimal, the constant factors may -- make it worthwhile to stick with the unweighted path compression -- supported by 'BindingMonad'. class (BindingMonad v t m) => RankedBindingMonad v t m | m -> v t where -- | Given a variable pointing to @MutTerm v t@, return its -- rank and the term it's bound to. lookupRankVar :: v (MutTerm v t) -> m (Rank v t) -- | Increase the rank of a variable by one. incrementRank :: v (MutTerm v t) -> m () -- | Bind a variable to a term and increment the rank at the -- same time. The default implementation is: -- -- > incrementBindVar v t = do { incrementRank v ; bindVar v t } incrementBindVar :: v (MutTerm v t) -> MutTerm v t -> m () incrementBindVar v t = do { incrementRank v ; bindVar v t } ---------------------------------------------------------------- ----------------------------------------------------------- fin.