diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,45 @@ +=== Notes === + +The following license applies to all code in this package. The +module Control.Monad.MaybeK is derived from code on the Haskell +Wiki[1] which was released under a simple permissive license[2]. + +[1] +[2] + + +=== unification-fd license === + +Copyright (c) 2007, 2008, 2011, wren ng thornton. +ALL RIGHTS RESERVED. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of the copyright holders nor the names of + other contributors may be used to endorse or promote products + derived from this software without specific prior written + permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE. + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,7 @@ +#!/usr/bin/env runhaskell + +module Main (main) where +import Distribution.Simple + +main :: IO () +main = defaultMain diff --git a/src/Control/Monad/EitherK.hs b/src/Control/Monad/EitherK.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/EitherK.hs @@ -0,0 +1,219 @@ + +-- The MPTCs and FlexibleInstances are only for +-- mtl:Control.Monad.Error.MonadError +{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.06.30 +-- | +-- Module : Control.Monad.EitherK +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : provisional +-- Portability : semi-portable (Rank2Types, MPTCs, FlexibleInstances) +-- +-- A continuation-passing variant of 'Either' for short-circuiting +-- at failure. This code is based on "Control.Monad.MaybeK". +---------------------------------------------------------------- +module Control.Monad.EitherK + ( + -- * The short-circuiting monad + EitherK() + , runEitherK + , toEitherK + , eitherK + , throwEitherK + , catchEitherK + -- * The short-circuiting monad transformer + , EitherKT() + , runEitherKT + , toEitherKT + , liftEitherK + , lowerEitherK + , throwEitherKT + , catchEitherKT + ) where + +import Data.Monoid (Monoid(..)) +import Control.Applicative (Applicative(..), Alternative(..)) +import Control.Monad (MonadPlus(..), liftM, ap) +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.Error (MonadError(..)) +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | A continuation-passing encoding of 'Either' as an error monad; +-- also known as @Codensity (Either e)@, if you're familiar with +-- that terminology. N.B., this is not the 2-continuation implementation +-- based on the Church encoding of @Either@. The latter tends to +-- have worse performance than non-continuation based implementations. +-- +-- This is generally more efficient than using @Either@ (or the +-- MTL's @Error@) for two reasons. First is that it right associates +-- all binds, ensuring that bad associativity doesn't artificially +-- introduce midpoints in short-circuiting to the nearest handler. +-- Second is that it removes the need for intermediate case +-- expressions. +-- +-- Another benefit over MTL's @Error@ is that it doesn't artificially +-- restrict the error type. In fact, there's no reason why @e@ must +-- denote \"errors\" per se. This could also denote computations +-- which short-circuit with the final answer, or similar methods +-- of non-local control flow. +-- +-- N.B., the 'Alternative' and 'MonadPlus' instances are left-biased +-- in @a@ and monoidal in @e@. Thus, they are not commutative. +newtype EitherK e a = EK (forall r. (a -> Either e r) -> Either e r) + + +-- | Execute an @EitherK@ and return the concrete @Either@ encoding. +runEitherK :: EitherK e a -> Either e a +runEitherK (EK m) = m Right +{-# INLINE runEitherK #-} + + +-- | Lift an @Either@ into an @EitherK@. +toEitherK :: Either e a -> EitherK e a +toEitherK (Left e) = throwEitherK e +toEitherK (Right a) = return a +{-# INLINE toEitherK #-} + + +-- | Throw an error in the @EitherK@ monad. This is identical to +-- 'throwError'. +throwEitherK :: e -> EitherK e a +throwEitherK e = EK (\_ -> Left e) +{-# INLINE throwEitherK #-} + + +-- | Handle errors in the @EitherK@ monad. N.B., this type is more +-- general than that of 'catchError', allowing the type of the +-- errors to change. +catchEitherK :: EitherK e a -> (e -> EitherK f a) -> EitherK f a +catchEitherK m handler = eitherK handler return m +{-# INLINE catchEitherK #-} + + +-- | A version of 'either' on @EitherK@, for convenience. N.B., +-- using this function inserts a case match, reducing the range of +-- short-circuiting. +eitherK :: (e -> b) -> (a -> b) -> EitherK e a -> b +eitherK left right m = + case runEitherK m of + Left e -> left e + Right a -> right a +{-# INLINE eitherK #-} + + +instance Functor (EitherK e) where + fmap f (EK m) = EK (\k -> m (k . f)) + +instance Applicative (EitherK e) where + pure = return + (<*>) = ap + +instance Monad (EitherK e) where + return a = EK (\k -> k a) + EK m >>= f = EK (\k -> m (\a -> case f a of EK n -> n k)) + -- Using case instead of let seems to improve performance + -- considerably by removing excessive laziness. + +instance (Monoid e) => Alternative (EitherK e) where + empty = mzero + (<|>) = mplus + +instance (Monoid e) => MonadPlus (EitherK e) where + mzero = throwEitherK mempty + m `mplus` n = catchEitherK m $ \me -> + catchEitherK n $ \ne -> + throwEitherK $ me `mappend` ne + +instance MonadError e (EitherK e) where + throwError = throwEitherK + catchError = catchEitherK + +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | A monad transformer version of 'EitherK'. +newtype EitherKT e m a = + EKT (forall r. (a -> m (Either e r)) -> m (Either e r)) + + +-- | Execute an @EitherKT@ and return the concrete @Either@ encoding. +runEitherKT :: (Monad m) => EitherKT e m a -> m (Either e a) +runEitherKT (EKT m) = m (return . Right) +{-# INLINE runEitherKT #-} + + +-- | Lift an @Either@ into an @EitherKT@. +toEitherKT :: (Monad m) => Either e a -> EitherKT e m a +toEitherKT (Left e) = throwEitherKT e +toEitherKT (Right a) = return a +{-# INLINE toEitherKT #-} + + +-- TODO: isn't there a better implementation that doesn't lose shortcircuiting? +-- | Lift an @EitherK@ into an @EitherKT@. +liftEitherK :: (Monad m) => EitherK e a -> EitherKT e m a +liftEitherK = toEitherKT . runEitherK +{-# INLINE liftEitherK #-} + + +-- TODO: is there a better implementation? +-- | Lower an @EitherKT@ into an @EitherK@. +lowerEitherK :: (Monad m) => EitherKT e m a -> m (EitherK e a) +lowerEitherK = liftM toEitherK . runEitherKT +{-# INLINE lowerEitherK #-} + + +-- | Throw an error in the @EitherKT@ monad. This is identical to +-- 'throwError'. +throwEitherKT :: (Monad m) => e -> EitherKT e m a +throwEitherKT e = EKT (\_ -> return (Left e)) +{-# INLINE throwEitherKT #-} + + +-- | Handle errors in the @EitherKT@ monad. N.B., this type is more +-- general than that of 'catchError', allowing the type of the +-- errors to change. +catchEitherKT + :: (Monad m) + => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a +catchEitherKT m handler = EKT $ \k -> do + ea <- runEitherKT m + case ea of + Left e -> case handler e of EKT m' -> m' k + Right a -> k a +{-# INLINE catchEitherKT #-} + + +instance Functor (EitherKT e m) where + fmap f (EKT m) = EKT (\k -> m (k . f)) + +instance Applicative (EitherKT e m) where + pure = return + (<*>) = ap + +instance Monad (EitherKT e m) where + return a = EKT (\k -> k a) + EKT m >>= f = EKT (\k -> m (\a -> case f a of EKT n -> n k)) + +-- TODO: is there any way to define catchEitherKT so it only requires Applicative m? +instance (Monad m, Monoid e) => Alternative (EitherKT e m) where + empty = mzero + (<|>) = mplus + +instance (Monad m, Monoid e) => MonadPlus (EitherKT e m) where + mzero = throwEitherKT mempty + m `mplus` n = catchEitherKT m (catchEitherKT n . (throwEitherKT .) . mappend) + +instance (Monad m) => MonadError e (EitherKT e m) where + throwError = throwEitherKT + catchError = catchEitherKT + +instance MonadTrans (EitherKT e) where + lift m = EKT (\k -> m >>= k) + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Monad/MaybeK.hs b/src/Control/Monad/MaybeK.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/MaybeK.hs @@ -0,0 +1,180 @@ +-- The MPTCs is only for mtl:Control.Monad.Error.MonadError +{-# LANGUAGE Rank2Types, MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.06.30 +-- | +-- Module : Control.Monad.MaybeK +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : provisional +-- Portability : semi-portable (Rank2Types, MPTCs) +-- +-- A continuation-passing variant of 'Maybe' for short-circuiting +-- at failure. This is based largely on code from the Haskell Wiki +-- () which +-- was released under a simple permissive license +-- (). +-- However, various changes and extensions have been made, which +-- are subject to the BSD license of this package. +---------------------------------------------------------------- +module Control.Monad.MaybeK + ( + -- * The partiality monad + MaybeK + , runMaybeK + , toMaybeK + , maybeK + -- * The partiality monad transformer + , MaybeKT + , runMaybeKT + , toMaybeKT + , liftMaybeK + , lowerMaybeK + ) where + +import Control.Applicative (Applicative(..), Alternative(..)) +import Control.Monad (MonadPlus(..), liftM, ap) +import Control.Monad.Error (MonadError(..)) +import Control.Monad.Trans (MonadTrans(..)) +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | A continuation-passing encoding of 'Maybe'; also known as +-- @Codensity Maybe@, if you're familiar with that terminology. +-- N.B., this is not the 2-continuation implementation based on the +-- Church encoding of @Maybe@. The latter tends to have worse +-- performance than non-continuation based implementations. +-- +-- This is generally more efficient than using @Maybe@ for two +-- reasons. First is that it right associates all binds, ensuring +-- that bad associativity doesn't artificially introduce midpoints +-- in short-circuiting to the nearest handler. Second is that it +-- removes the need for intermediate case expressions. +-- +-- N.B., the 'Alternative' and 'MonadPlus' instances are left-biased +-- in @a@. Thus, they are not commutative. +newtype MaybeK a = MK (forall r. (a -> Maybe r) -> Maybe r) + + +-- | Execute the @MaybeK@ and return the concrete @Maybe@ encoding. +runMaybeK :: MaybeK a -> Maybe a +runMaybeK (MK m) = m return +{-# INLINE runMaybeK #-} + + +-- | Lift a @Maybe@ into @MaybeK@. +toMaybeK :: Maybe a -> MaybeK a +toMaybeK Nothing = mzero +toMaybeK (Just a) = return a +{-# INLINE toMaybeK #-} + + +-- | A version of 'maybe' for convenience. This is almost identical +-- to 'mplus' but allows applying a continuation to @Just@ values +-- as well as handling @Nothing@ errors. If you only want to handle +-- the errors, use 'mplus' instead. +maybeK :: b -> (a -> b) -> MaybeK a -> b +maybeK nothing just m = + case runMaybeK m of + Nothing -> nothing + Just a -> just a +{-# INLINE maybeK #-} + + +instance Functor MaybeK where + fmap f (MK m) = MK (\k -> m (k . f)) + +instance Applicative MaybeK where + pure = return + (<*>) = ap + +instance Monad MaybeK where + return a = MK (\k -> k a) + MK m >>= f = MK (\k -> m (\a -> case f a of MK n -> n k)) + -- Using case instead of let seems to improve performance + -- considerably by removing excessive laziness. + +-- This is non-commutative, but it's the same as Alternative Maybe. +instance Alternative MaybeK where + empty = mzero + (<|>) = mplus + +instance MonadPlus MaybeK where + mzero = MK (\_ -> Nothing) + m `mplus` n = maybeK n return m + +instance MonadError () MaybeK where + throwError _ = mzero + catchError m f = maybeK (f ()) return m + +---------------------------------------------------------------- + +-- | A monad transformer version of 'MaybeK'. +newtype MaybeKT m a = MKT (forall r . (a -> m (Maybe r)) -> m (Maybe r)) + + +-- | Execute a @MaybeKT@ and return the concrete @Maybe@ encoding. +runMaybeKT :: (Monad m) => MaybeKT m a -> m (Maybe a) +runMaybeKT (MKT m) = m (return . Just) +{-# INLINE runMaybeKT #-} + + +-- | Lift a @Maybe@ into an @MaybeKT@. +toMaybeKT :: (Monad m) => Maybe a -> MaybeKT m a +toMaybeKT Nothing = mzero +toMaybeKT (Just a) = return a +{-# INLINE toMaybeKT #-} + + +-- TODO: isn't there a better implementation that doesn't lose shortcircuiting? +-- | Lift an @MaybeK@ into an @MaybeKT@. +liftMaybeK :: (Monad m) => MaybeK a -> MaybeKT m a +liftMaybeK = toMaybeKT . runMaybeK +{-# INLINE liftMaybeK #-} + + +-- TODO: is there a better implementation? +-- | Lower an @MaybeKT@ into an @MaybeK@. +lowerMaybeK :: (Monad m) => MaybeKT m a -> m (MaybeK a) +lowerMaybeK = liftM toMaybeK . runMaybeKT +{-# INLINE lowerMaybeK #-} + + +instance Functor (MaybeKT m) where + fmap f (MKT m) = MKT (\k -> m (k . f)) + +instance Applicative (MaybeKT m) where + pure = return + (<*>) = ap + +instance Monad (MaybeKT m) where + return a = MKT (\k -> k a) + MKT m >>= f = MKT (\k -> m (\a -> case f a of MKT n -> n k)) + +instance (Monad m) => Alternative (MaybeKT m) where + empty = mzero + (<|>) = mplus + +instance (Monad m) => MonadPlus (MaybeKT m) where + mzero = MKT (\_ -> return Nothing) + + m `mplus` n = MKT $ \k -> do + mb <- runMaybeKT m + case mb of + Nothing -> case n of MKT n' -> n' k + Just a -> k a + +instance (Monad m) => MonadError () (MaybeKT m) where + throwError _ = mzero + catchError m f = MKT $ \k -> do + mb <- runMaybeKT m + case mb of + Nothing -> case f () of MKT n -> n k + Just a -> k a + +instance MonadTrans MaybeKT where + lift m = MKT (\k -> m >>= k) + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Monad/State/UnificationExtras.hs b/src/Control/Monad/State/UnificationExtras.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/State/UnificationExtras.hs @@ -0,0 +1,66 @@ + +{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.05 +-- | +-- Module : Control.Monad.State.UnificationExtras +-- Copyright : Copyright (c) 2008--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : perpetually unstable +-- Portability : semi-portable (MPTCs) +-- +-- This module defines some extra functions for "Control.Monad.State.Lazy". +-- This package really isn't the proper place for these, but we +-- need them to be somewhere. +-- +-- TODO: patch transformers\/mtl-2 with these functions. +---------------------------------------------------------------- +module Control.Monad.State.UnificationExtras + ( + -- * Additional functions for MTL + liftReader + , liftReaderT + , modify' + , localState + ) where + +import Control.Monad (liftM) +import Control.Monad.Reader (Reader(), ReaderT(..)) +import Control.Monad.State.Lazy (MonadState(..), State(), StateT(..)) + +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | Lift a reader into a state monad. More particularly, this +-- allows disabling mutability in a local context within @StateT@. +liftReaderT :: (Monad m) => ReaderT e m a -> StateT e m a +liftReaderT r = StateT $ \e -> liftM (\a -> (a,e)) (runReaderT r e) + + +-- | Lift a reader into a state monad. More particularly, this +-- allows disabling mutability in a local context within @State@. +liftReader :: Reader e a -> State e a +liftReader = liftReaderT + + +-- | A strict version of 'modify'. +modify' :: (MonadState s m) => (s -> s) -> m () +modify' f = do + s <- get + put $! f s +{-# INLINE modify' #-} + + +-- | Run a state action and undo the state changes at the end. +localState :: (MonadState s m) => m a -> m a +localState m = do + s <- get + x <- m + put s + return x +{-# INLINE localState #-} + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification.hs b/src/Control/Unification.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification.hs @@ -0,0 +1,653 @@ + +{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.11 +-- | +-- Module : Control.Unification +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : semi-portable (MPTCs, FlexibleContexts) +-- +-- This module provides first-order structural unification over +-- general structure types. It also provides the standard suite of +-- functions accompanying unification (applying bindings, getting +-- free variables, etc.). +-- +-- The implementation makes use of numerous optimization techniques. +-- First, we use path compression everywhere (for weighted path +-- compression see "Control.Unification.Ranked"). Second, we replace +-- the occurs-check with visited-sets. Third, we use a technique +-- for aggressive opportunistic observable sharing; that is, we +-- track as much sharing as possible in the bindings (without +-- introducing new variables), so that we can compare bound variables +-- directly and therefore eliminate redundant unifications. +---------------------------------------------------------------- +module Control.Unification + ( + -- * Data types, classes, etc + -- ** Mutable terms + MutTerm(..) + , freeze + , unfreeze + -- ** Errors + , UnificationFailure(..) + -- ** Basic type classes + , Unifiable(..) + , Variable(..) + , BindingMonad(..) + + -- * Operations on one term + , getFreeVars + , applyBindings + , freshen + -- freezeM -- apply bindings and freeze in one traversal + -- unskolemize -- convert Skolemized variables to free variables + -- skolemize -- convert free variables to Skolemized variables + -- getSkolems -- compute the skolem variables in a term; helpful? + + -- * Operations on two terms + -- ** Symbolic names + , (===) + , (=~=) + , (=:=) + , (<:=) + -- ** Textual names + , equals + , equiv + , unify + , unifyOccurs + , subsumes + + -- * Helper functions + -- | Client code should not need to use these functions, but + -- they are exposed just in case they are needed. + , fullprune + , semiprune + , occursIn + ) where + +import Prelude + hiding (mapM, mapM_, sequence, foldr, foldr1, foldl, foldl1, all, and, or) + +import qualified Data.IntMap as IM +import qualified Data.IntSet as IS +import Data.Foldable +import Data.Traversable +import Control.Applicative +import Control.Monad (MonadPlus(..)) +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.Error (MonadError(..)) +import Control.Monad.State (MonadState(..), StateT, evalStateT, execStateT) +import Control.Monad.MaybeK +import Control.Monad.State.UnificationExtras +import Control.Unification.Types +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- BUG: this assumes there are no directly-cyclic chains! +-- +-- | Canonicalize a chain of variables so they all point directly +-- to the term at the end of the chain (or the free variable, if +-- the chain is unbound), and return that end. +-- +-- N.B., this is almost never the function you want. Cf., 'semiprune'. +fullprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t) +fullprune t0 = + case t0 of + MutTerm _ -> return t0 + MutVar v -> do + mb <- lookupVar v + case mb of + Nothing -> return t0 + Just t -> do + finalTerm <- fullprune t + v `bindVar` finalTerm + return finalTerm + + +-- BUG: this assumes there are no directly-cyclic chains! +-- +-- | Canonicalize a chain of variables so they all point directly +-- to the last variable in the chain, regardless of whether it is +-- bound or not. This allows detecting many cases where multiple +-- variables point to the same term, thereby allowing us to avoid +-- re-unifying the term they point to. +semiprune :: (BindingMonad v t m) => MutTerm v t -> m (MutTerm v t) +semiprune = + \t0 -> + case t0 of + MutTerm _ -> return t0 + MutVar v0 -> loop t0 v0 + where + -- We pass the @t@ for @v@ in order to add just a little more sharing. + loop t v = do + mb <- lookupVar v + case mb of + Nothing -> return t + Just t' -> + case t' of + MutTerm _ -> return t + MutVar v' -> do + finalVar <- loop t' v' + v `bindVar` finalVar + return finalVar + + +-- | Determine if a variable appears free somewhere inside a term. +-- Since occurs checks only make sense when we're about to bind the +-- variable to the term, we do not bother checking for the possibility +-- of the variable occuring bound in the term. +occursIn :: (BindingMonad v t m) => v (MutTerm v t) -> MutTerm v t -> m Bool +occursIn v t0 = do + t <- fullprune t0 + case t of + MutTerm t' -> or <$> mapM (v `occursIn`) t' -- TODO: use foldlM instead + MutVar v' -> return $! v `eqVar` v' + + +-- TODO: use IM.insertWith or the like to do this in one pass +-- | Update the visited-set with a seclaration that a variable has +-- been seen with a given binding, or throw 'OccursIn' if the +-- variable has already been seen. +seenAs + :: ( BindingMonad v t m + , MonadTrans e + , MonadError (UnificationFailure v t) (e m) + ) + => v (MutTerm v t) -- ^ + -> MutTerm v t -- ^ + -> StateT (IM.IntMap (MutTerm v t)) (e m) () +seenAs v t = do + seenVars <- get + case IM.lookup (getVarID v) seenVars of + Just t' -> lift . throwError $ OccursIn v t' + Nothing -> put $! IM.insert (getVarID v) t seenVars +{-# INLINE seenAs #-} + +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- TODO: these assume pure variables, hence the spine cloning; but +-- we may want to make variants for impure variables with explicit +-- rollback on backtracking. + +-- TODO: See if MTL still has that overhead over doing things manually. + +-- TODO: Figure out how to abstract the left-catamorphism from these. + + +-- | Walk a term and determine what variables are still free. N.B., +-- this function does not detect cyclic terms (i.e., throw errors), +-- but it will return the correct answer for them in finite time. +getFreeVars :: (BindingMonad v t m) => MutTerm v t -> m [v (MutTerm v t)] +getFreeVars = + \t -> IM.elems <$> evalStateT (loop t) IS.empty + where + loop t0 = do + t1 <- lift $ semiprune t0 + case t1 of + MutTerm t -> fold <$> mapM loop t -- TODO: use foldlM instead? + MutVar v -> do + seenVars <- get + let i = getVarID v + if IS.member i seenVars + then return IM.empty -- no (more) free vars down here + else do + put $! IS.insert i seenVars + mb <- lift $ lookupVar v + case mb of + Just t' -> loop t' + Nothing -> return $ IM.singleton i v + + +-- | Apply the current bindings from the monad so that any remaining +-- variables in the result must, therefore, be free. N.B., this +-- expensively clones term structure and should only be performed +-- when a pure term is needed, or when 'OccursIn' exceptions must +-- be forced. This function /does/ preserve sharing, however that +-- sharing is no longer observed by the monad. +-- +-- If any cyclic bindings are detected, then an 'OccursIn' exception +-- will be thrown. +applyBindings + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +applyBindings = + \t -> evalStateT (loop t) IM.empty + where + loop t0 = do + t1 <- lift . lift $ semiprune t0 + case t1 of + MutTerm t -> MutTerm <$> mapM loop t + MutVar v -> do + let i = getVarID v + mb <- IM.lookup i <$> get + case mb of + Just (Right t) -> return t + Just (Left t) -> lift . throwError $ OccursIn v t + Nothing -> do + mb' <- lift . lift $ lookupVar v + case mb' of + Nothing -> return t1 + Just t -> do + modify' . IM.insert i $ Left t + t' <- loop t + modify' . IM.insert i $ Right t' + return t' + + +-- | Freshen all variables in a term, both bound and free. This +-- ensures that the observability of sharing is maintained, while +-- freshening the free variables. N.B., this expensively clones +-- term structure and should only be performed when necessary. +-- +-- If any cyclic bindings are detected, then an 'OccursIn' exception +-- will be thrown. +freshen + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +freshen = + \t -> evalStateT (loop t) IM.empty + where + loop t0 = do + t1 <- lift . lift $ semiprune t0 + case t1 of + MutTerm t -> MutTerm <$> mapM loop t + MutVar v -> do + let i = getVarID v + seenVars <- get + case IM.lookup i seenVars of + Just (Right t) -> return t + Just (Left t) -> lift . throwError $ OccursIn v t + Nothing -> do + mb <- lift . lift $ lookupVar v + case mb of + Nothing -> do + v' <- lift . lift $ MutVar <$> freeVar + put $! IM.insert i (Right v') seenVars + return v' + Just t -> do + put $! IM.insert i (Left t) seenVars + t' <- loop t + v' <- lift . lift $ MutVar <$> newVar t' + modify' $ IM.insert i (Right v') + return v' + +---------------------------------------------------------------- +---------------------------------------------------------------- +-- BUG: have to give the signatures for Haddock :( + +-- | 'equals' +(===) + :: (BindingMonad v t m) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> m Bool -- ^ +(===) = equals +infix 4 ===, `equals` + + +-- | 'equiv' +(=~=) + :: (BindingMonad v t m) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> m (Maybe (IM.IntMap Int)) -- ^ +(=~=) = equiv +infix 4 =~=, `equiv` + + +-- | 'unify' +(=:=) + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +(=:=) = unify +infix 4 =:=, `unify` + + +-- | 'subsumes' +(<:=) + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m Bool +(<:=) = subsumes +infix 4 <:=, `subsumes` + +---------------------------------------------------------------- + +-- TODO: should we offer a variant which gives the reason for failure? +-- +-- | Determine if two terms are structurally equal. This is essentially +-- equivalent to @('==')@ except that it does not require applying +-- bindings before comparing, so it is more efficient. N.B., this +-- function does not consider alpha-variance, and thus variables +-- with different names are considered unequal. Cf., 'equiv'. +equals + :: (BindingMonad v t m) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> m Bool -- ^ +equals = + \tl tr -> do + mb <- runMaybeKT (loop tl tr) + case mb of + Nothing -> return False + Just () -> return True + where + loop tl0 tr0 = do + tl <- lift $ semiprune tl0 + tr <- lift $ semiprune tr0 + case (tl, tr) of + (MutVar vl', MutVar vr') + | vl' `eqVar` vr' -> return () -- success + | otherwise -> do + mtl <- lift $ lookupVar vl' + mtr <- lift $ lookupVar vr' + case (mtl, mtr) of + (Nothing, Nothing ) -> mzero + (Nothing, Just _ ) -> mzero + (Just _, Nothing ) -> mzero + (Just tl', Just tr') -> loop tl' tr' -- TODO: should just jump to match + (MutVar _, MutTerm _ ) -> mzero + (MutTerm _, MutVar _ ) -> mzero + (MutTerm tl', MutTerm tr') -> + case zipMatch tl' tr' of + Nothing -> mzero + Just tlr -> mapM_ (uncurry loop) tlr + + +-- TODO: is that the most helpful return type? +-- +-- | Determine if two terms are structurally equivalent; that is, +-- structurally equal modulo renaming of free variables. Returns a +-- mapping from variable IDs of the left term to variable IDs of +-- the right term, indicating the renaming used. +equiv + :: (BindingMonad v t m) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> m (Maybe (IM.IntMap Int)) -- ^ +equiv = + \tl tr -> runMaybeKT (execStateT (loop tl tr) IM.empty) + where + loop tl0 tr0 = do + tl <- lift . lift $ fullprune tl0 + tr <- lift . lift $ fullprune tr0 + case (tl, tr) of + (MutVar vl', MutVar vr') -> do + let il = getVarID vl' + let ir = getVarID vr' + xs <- get + case IM.lookup il xs of + Just x + | x == ir -> return () + | otherwise -> lift mzero + Nothing -> put $! IM.insert il ir xs + + (MutVar _, MutTerm _ ) -> lift mzero + (MutTerm _, MutVar _ ) -> lift mzero + (MutTerm tl', MutTerm tr') -> + case zipMatch tl' tr' of + Nothing -> lift mzero + Just tlr -> mapM_ (uncurry loop) tlr + + +---------------------------------------------------------------- +-- Not quite unify2 from the benchmarks, since we do AOOS. +-- +-- | A variant of 'unify' which uses 'occursIn' instead of visited-sets. +-- This should only be used when eager throwing of 'OccursIn' errors +-- is absolutely essential (or for testing the correctness of +-- @unify@). Performing the occurs-check is expensive. Not only is +-- it slow, it's asymptotically slow since it can cause the same +-- subterm to be traversed multiple times. +unifyOccurs + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +unifyOccurs = loop + where + {-# INLINE (=:) #-} + v =: t = lift $ v `bindVar` t + + {-# INLINE acyclicBindVar #-} + acyclicBindVar v t = do + b <- lift $ v `occursIn` t + if b + then throwError $ OccursIn v t + else v =: t + + -- TODO: cf todos in 'unify' + loop tl0 tr0 = do + tl <- lift $ semiprune tl0 + tr <- lift $ semiprune tr0 + case (tl, tr) of + (MutVar vl', MutVar vr') + | vl' `eqVar` vr' -> return tr + | otherwise -> do + mtl <- lift $ lookupVar vl' + mtr <- lift $ lookupVar vr' + case (mtl, mtr) of + (Nothing, Nothing ) -> do + vl' =: tr + return tr + (Nothing, Just _ ) -> do + vl' `acyclicBindVar` tr + return tr + (Just _ , Nothing ) -> do + vr' `acyclicBindVar` tl + return tl + (Just tl', Just tr') -> do + t <- loop tl' tr' + vr' =: t + vl' =: tr + return tr + + (MutVar vl', MutTerm _) -> do + mtl <- lift $ lookupVar vl' + case mtl of + Nothing -> do + vl' `acyclicBindVar` tr + return tl + Just tl' -> do + t <- loop tl' tr + vl' =: t + return tl + + (MutTerm _, MutVar vr') -> do + mtr <- lift $ lookupVar vr' + case mtr of + Nothing -> do + vr' `acyclicBindVar` tl + return tr + Just tr' -> do + t <- loop tl tr' + vr' =: t + return tr + + (MutTerm tl', MutTerm tr') -> + case zipMatch tl' tr' of + Nothing -> throwError $ TermMismatch tl' tr' + Just tlr -> MutTerm <$> mapM (uncurry loop) tlr + + +---------------------------------------------------------------- +-- TODO: verify correctness, especially for the visited-set stuff. +-- TODO: return Maybe(MutTerm v t) in the loop so we can avoid updating bindings trivially +-- TODO: figure out why unifyOccurs is so much faster on pure ground terms!! The only difference there is in lifting over StateT... +-- +-- | Unify two terms, or throw an error with an explanation of why +-- unification failed. Since bindings are stored in the monad, the +-- two input terms and the output term are all equivalent if +-- unification succeeds. However, the returned value makes use of +-- aggressive opportunistic observable sharing, so it will be more +-- efficient to use it in future calculations than either argument. +unify + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +unify = + \tl tr -> evalStateT (loop tl tr) IM.empty + where + {-# INLINE (=:) #-} + v =: t = lift . lift $ v `bindVar` t + + -- TODO: would it be beneficial to manually fuse @x <- lift m; y <- lift n@ to @(x,y) <- lift (m;n)@ everywhere we can? + loop tl0 tr0 = do + tl <- lift . lift $ semiprune tl0 + tr <- lift . lift $ semiprune tr0 + case (tl, tr) of + (MutVar vl', MutVar vr') + | vl' `eqVar` vr' -> return tr + | otherwise -> do + mtl <- lift . lift $ lookupVar vl' + mtr <- lift . lift $ lookupVar vr' + case (mtl, mtr) of + (Nothing, Nothing ) -> do vl' =: tr ; return tr + (Nothing, Just _ ) -> do vl' =: tr ; return tr + (Just _ , Nothing ) -> do vr' =: tl ; return tl + (Just tl', Just tr') -> do + t <- localState $ do + vl' `seenAs` tl' + vr' `seenAs` tr' + loop tl' tr' -- TODO: should just jump to match + vr' =: t + vl' =: tr + return tr + + (MutVar vl', MutTerm _) -> do + t <- do + mtl <- lift . lift $ lookupVar vl' + case mtl of + Nothing -> return tr + Just tl' -> localState $ do + vl' `seenAs` tl' + loop tl' tr -- TODO: should just jump to match + vl' =: t + return tl + + (MutTerm _, MutVar vr') -> do + t <- do + mtr <- lift . lift $ lookupVar vr' + case mtr of + Nothing -> return tl + Just tr' -> localState $ do + vr' `seenAs` tr' + loop tl tr' -- TODO: should just jump to match + vr' =: t + return tr + + (MutTerm tl', MutTerm tr') -> + case zipMatch tl' tr' of + Nothing -> lift . throwError $ TermMismatch tl' tr' + Just tlr -> MutTerm <$> mapM (uncurry loop) tlr + +---------------------------------------------------------------- +-- TODO: can we find an efficient way to return the bindings directly instead of altering the monadic bindings? Maybe another StateT IntMap taking getVarID to the variable and its pseudo-bound term? +-- +-- TODO: verify correctness +-- TODO: redo with some codensity +-- TODO: there should be some way to catch OccursIn errors and repair the bindings... + +-- | Determine whether the left term subsumes the right term. That +-- is, whereas @(tl =:= tr)@ will compute the most general substitution +-- @s@ such that @(s tl === s tr)@, @(tl <:= tr)@ computes the most +-- general substitution @s@ such that @(s tl === tr)@. This means +-- that @tl@ is less defined than and consistent with @tr@. +-- +-- /N.B./, this function updates the monadic bindings just like +-- 'unify' does. However, while the use cases for unification often +-- want to keep the bindings around, the use cases for subsumption +-- usually do not. Thus, you'll probably want to use a binding monad +-- which supports backtracking in order to undo the changes. +-- Unfortunately, leaving the monadic bindings unaltered and returning +-- the necessary substitution directly imposes a performance penalty +-- or else requires specifying too much about the implementation +-- of variables. +subsumes + :: ( BindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m Bool +subsumes = + \tl tr -> evalStateT (loop tl tr) IM.empty + where + {-# INLINE (=:) #-} + v =: t = lift . lift $ do v `bindVar` t ; return True + + -- TODO: cf todos in 'unify' + loop tl0 tr0 = do + tl <- lift . lift $ semiprune tl0 + tr <- lift . lift $ semiprune tr0 + case (tl, tr) of + (MutVar vl', MutVar vr') + | vl' `eqVar` vr' -> return True + | otherwise -> do + mtl <- lift . lift $ lookupVar vl' + mtr <- lift . lift $ lookupVar vr' + case (mtl, mtr) of + (Nothing, Nothing ) -> vl' =: tr + (Nothing, Just _ ) -> vl' =: tr + (Just _ , Nothing ) -> return False + (Just tl', Just tr') -> + localState $ do + vl' `seenAs` tl' + vr' `seenAs` tr' + loop tl' tr' + + (MutVar vl', MutTerm _ ) -> do + mtl <- lift . lift $ lookupVar vl' + case mtl of + Nothing -> vl' =: tr + Just tl' -> localState $ do + vl' `seenAs` tl' + loop tl' tr + + (MutTerm _, MutVar _ ) -> return False + + (MutTerm tl', MutTerm tr') -> + case zipMatch tl' tr' of + Nothing -> return False + Just tlr -> and <$> mapM (uncurry loop) tlr + + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/IntVar.hs b/src/Control/Unification/IntVar.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/IntVar.hs @@ -0,0 +1,205 @@ + +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.06 +-- | +-- Module : Control.Unification.IntVar +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : semi-portable (MPTCs,...) +-- +-- This module defines a state monad for functional pointers +-- represented by integers as keys into an @IntMap@. This technique +-- was independently discovered by Dijkstra et al. This module +-- extends the approach by using a state monad transformer, which +-- can be made into a backtracking state monad by setting the +-- underlying monad to some 'MonadLogic' (part of the @logict@ +-- library, described by Kiselyov et al.). +-- +-- * Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008) +-- /Efficient Functional Unification and Substitution/, +-- Technical Report UU-CS-2008-027, Utrecht University. +-- +-- * Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and +-- Amr Sabry (2005) /Backtracking, Interleaving, and/ +-- /Terminating Monad Transformers/, ICFP. +---------------------------------------------------------------- +module Control.Unification.IntVar + ( IntVar(..) + , IntBindingState() + , IntBindingT() + , runIntBindingT + , evalIntBindingT + , execIntBindingT + ) where + +import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) + +import qualified Data.IntMap as IM +import Control.Applicative +import Control.Monad (MonadPlus(..), liftM) +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.State (MonadState(..), StateT, runStateT, evalStateT, execStateT, gets) +import Control.Monad.Logic (MonadLogic(..)) +import Control.Unification.Types +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | A \"mutable\" unification variable implemented by an integer. +-- This provides an entirely pure alternative to truly mutable +-- alternatives (like @STVar@), which can make backtracking easier. +-- +-- N.B., because this implementation is pure, we can use it for +-- both ranked and unranked monads. +newtype IntVar t = IntVar Int + deriving (Show) + +{- +-- BUG: This part works, but we'd want to change Show IntBindingState too. + +instance Show (IntVar t) where + show (IntVar i) = "IntVar " ++ show (boundedInt2Word i) + +-- | Convert an integer to a word, via the continuous mapping that +-- preserves @minBound@ and @maxBound@. +boundedInt2Word :: Int -> Word +boundedInt2Word i + | i < 0 = fromIntegral (i + maxBound + 1) + | otherwise = fromIntegral i + fromIntegral (maxBound :: Int) + 1 +-} + +instance Variable IntVar where + eqVar (IntVar i) (IntVar j) = i == j + + getVarID (IntVar v) = v + + +---------------------------------------------------------------- +-- | Binding state for 'IntVar'. +data IntBindingState t = IntBindingState + { nextFreeVar :: {-# UNPACK #-} !Int + , varBindings :: IM.IntMap (MutTerm IntVar t) + } + +-- Can't derive this because it's an UndecidableInstance +instance (Show (t (MutTerm IntVar t))) => + Show (IntBindingState t) + where + show (IntBindingState nr bs) = + "IntBindingState { nextFreeVar = "++show nr++ + ", varBindings = "++show bs++"}" + +-- | The initial @IntBindingState@. +emptyIntBindingState :: IntBindingState t +emptyIntBindingState = IntBindingState minBound IM.empty + + +---------------------------------------------------------------- +-- | A monad for storing 'IntVar' bindings, implemented as a 'StateT'. +-- For a plain state monad, set @m = Identity@; for a backtracking +-- state monad, set @m = Logic@. +newtype IntBindingT t m a = IBT { unIBT :: StateT (IntBindingState t) m a } + +-- For portability reasons, we're intentionally avoiding +-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like. + +instance (Functor m) => Functor (IntBindingT t m) where + fmap f = IBT . fmap f . unIBT + +-- BUG: can't reduce dependency to Applicative because of StateT's instance. +instance (Functor m, Monad m) => Applicative (IntBindingT t m) where + pure = IBT . pure + x <*> y = IBT (unIBT x <*> unIBT y) + x *> y = IBT (unIBT x *> unIBT y) + x <* y = IBT (unIBT x <* unIBT y) + +instance (Monad m) => Monad (IntBindingT t m) where + return = IBT . return + m >>= f = IBT (unIBT m >>= unIBT . f) + +instance MonadTrans (IntBindingT t) where + lift = IBT . lift + +-- BUG: can't reduce dependency to Alternative because of StateT's instance. +instance (Functor m, MonadPlus m) => Alternative (IntBindingT t m) where + empty = IBT empty + x <|> y = IBT (unIBT x <|> unIBT y) + +instance (MonadPlus m) => MonadPlus (IntBindingT t m) where + mzero = IBT mzero + mplus ml mr = IBT (mplus (unIBT ml) (unIBT mr)) + +instance (Monad m) => MonadState (IntBindingState t) (IntBindingT t m) where + get = IBT get + put = IBT . put + +-- N.B., we already have (MonadLogic m) => MonadLogic (StateT s m), +-- provided that logict is compiled against the same mtl/monads-fd +-- we're getting StateT from. Otherwise we'll get a bunch of warnings +-- here. +instance (MonadLogic m) => MonadLogic (IntBindingT t m) where + msplit (IBT m) = IBT (coerce `liftM` msplit m) + where + coerce Nothing = Nothing + coerce (Just (a, m')) = Just (a, IBT m') + + interleave (IBT l) (IBT r) = IBT (interleave l r) + + IBT m >>- f = IBT (m >>- (unIBT . f)) + + ifte (IBT b) t (IBT f) = IBT (ifte b (unIBT . t) f) + + once (IBT m) = IBT (once m) + +---------------------------------------------------------------- + +runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t) +runIntBindingT (IBT m) = runStateT m emptyIntBindingState + + +-- | N.B., you should explicitly apply bindings before calling this +-- function, or else the bindings will be lost +evalIntBindingT :: (Monad m) => IntBindingT t m a -> m a +evalIntBindingT (IBT m) = evalStateT m emptyIntBindingState + + +execIntBindingT :: (Monad m) => IntBindingT t m a -> m (IntBindingState t) +execIntBindingT (IBT m) = execStateT m emptyIntBindingState + +---------------------------------------------------------------- + +instance (Unifiable t, Applicative m, Monad m) => + BindingMonad IntVar t (IntBindingT t m) + where + + lookupVar (IntVar v) = IBT $ gets (IM.lookup v . varBindings) + + freeVar = IBT $ do + ibs <- get + let v = nextFreeVar ibs + if v == maxBound + then error "freeVar: no more variables!" + else do + put $ ibs { nextFreeVar = v+1 } + return $ IntVar v + + newVar t = IBT $ do + ibs <- get + let v = nextFreeVar ibs + if v == maxBound + then error "newVar: no more variables!" + else do + let bs' = IM.insert v t (varBindings ibs) + put $ ibs { nextFreeVar = v+1, varBindings = bs' } + return $ IntVar v + + bindVar (IntVar v) t = IBT $ do + ibs <- get + let bs' = IM.insert v t (varBindings ibs) + put $ ibs { varBindings = bs' } + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/Ranked.hs b/src/Control/Unification/Ranked.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/Ranked.hs @@ -0,0 +1,177 @@ + +{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.11 +-- | +-- Module : Control.Unification.Ranked +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : highly experimental +-- Portability : semi-portable (MPTCs, FlexibleContexts) +-- +-- This module provides the API of "Control.Unification" except +-- using 'RankedBindingMonad' where appropriate. This module (and +-- the binding implementations for it) are highly experimental and +-- subject to change in future versions. +---------------------------------------------------------------- +module Control.Unification.Ranked + ( + -- * Data types, classes, etc + module Control.Unification.Types + + -- * Operations on one term + , getFreeVars + , applyBindings + , freshen + -- freezeM -- apply bindings and freeze in one traversal + -- unskolemize -- convert Skolemized variables to free variables + -- skolemize -- convert free variables to Skolemized variables + -- getSkolems -- compute the skolem variables in a term; helpful? + + -- * Operations on two terms + -- ** Symbolic names + , (===) + , (=~=) + , (=:=) + -- (<:=) + -- ** Textual names + , equals + , equiv + , unify + -- unifyOccurs + -- subsumes + ) where + +import Prelude + hiding (mapM, mapM_, sequence, foldr, foldr1, foldl, foldl1, all, or) + +import qualified Data.IntMap as IM +import Data.Traversable +import Control.Applicative +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.Error (MonadError(..)) +import Control.Monad.State (MonadState(..), evalStateT) +import Control.Monad.State.UnificationExtras +import Control.Unification.Types +import Control.Unification hiding (unify, (=:=)) +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | 'unify' +(=:=) + :: ( RankedBindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +(=:=) = unify +infix 4 =:=, `unify` + + +-- TODO: keep in sync as we verify correctness. +-- +-- | Unify two terms, or throw an error with an explanation of why +-- unification failed. Since bindings are stored in the monad, the +-- two input terms and the output term are all equivalent if +-- unification succeeds. However, the returned value makes use of +-- aggressive opportunistic observable sharing, so it will be more +-- efficient to use it in future calculations than either argument. +unify + :: ( RankedBindingMonad v t m + , MonadTrans e + , Functor (e m) -- Grr, Monad(e m) should imply Functor(e m) + , MonadError (UnificationFailure v t) (e m) + ) + => MutTerm v t -- ^ + -> MutTerm v t -- ^ + -> e m (MutTerm v t) -- ^ +unify = + \tl tr -> evalStateT (loop tl tr) IM.empty + where + -- TODO: use IM.insertWith or the like to do this in one pass + {-# INLINE seenAs #-} + v `seenAs` t = do + seenVars <- get + case IM.lookup (getVarID v) seenVars of + Just t' -> lift . throwError $ OccursIn v t' + Nothing -> put $ IM.insert (getVarID v) t seenVars + + {-# INLINE (=:) #-} + v =: t = bindVar v t >> return t + + loop tl0 tr0 = do + tl1 <- lift . lift $ semiprune tl0 + tr1 <- lift . lift $ semiprune tr0 + case (tl1, tr1) of + (MutVar vl, MutVar vr) + | vl `eqVar` vr -> return tr1 + | otherwise -> do + Rank rl mtl <- lift . lift $ lookupRankVar vl + Rank rr mtr <- lift . lift $ lookupRankVar vr + let cmp = compare rl rr + case (mtl, mtr) of + (Nothing, Nothing) -> lift . lift $ + case cmp of + LT -> do { vl =: tr1 } + EQ -> do { incrementRank vr ; vl =: tr1 } + GT -> do { vr =: tl1 } + + (Nothing, Just tr) -> lift . lift $ + case cmp of + LT -> do { vl =: tr1 } + EQ -> do { incrementRank vr ; vl =: tr1 } + GT -> do { vl `bindVar` tr ; vr =: tl1 } + + (Just tl, Nothing) -> lift . lift $ + case cmp of + LT -> do { vr `bindVar` tl ; vl =: tr1 } + EQ -> do { incrementRank vl ; vr =: tl1 } + GT -> do { vr =: tl1 } + + (Just tl, Just tr) -> do + t <- localState $ do + vl `seenAs` tl + vr `seenAs` tr + loop tl tr + lift . lift $ + case cmp of + LT -> do { vr `bindVar` t ; vl =: tr1 } + EQ -> do { incrementBindVar vl t ; vr =: tl1 } + GT -> do { vl `bindVar` t ; vr =: tl1 } + + (MutVar vl, MutTerm _) -> do + t <- do + mtl <- lift . lift $ lookupVar vl + case mtl of + Nothing -> return tr1 + Just tl -> localState $ do + vl `seenAs` tl + loop tl tr1 + lift . lift $ do + vl `bindVar` t + return tl1 + + (MutTerm _, MutVar vr) -> do + t <- do + mtr <- lift . lift $ lookupVar vr + case mtr of + Nothing -> return tl1 + Just tr -> localState $ do + vr `seenAs` tr + loop tl1 tr + lift . lift $ do + vr `bindVar` t + return tr1 + + (MutTerm tl, MutTerm tr) -> + case zipMatch tl tr of + Nothing -> lift . throwError $ TermMismatch tl tr + Just tlr -> MutTerm <$> mapM (uncurry loop) tlr + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/Ranked/IntVar.hs b/src/Control/Unification/Ranked/IntVar.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/Ranked/IntVar.hs @@ -0,0 +1,189 @@ + +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-} +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.06 +-- | +-- Module : Control.Unification.Ranked.IntVar +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : highly experimental +-- Portability : semi-portable (MPTCs,...) +-- +-- A ranked variant of "Control.Unification.IntVar". +---------------------------------------------------------------- +module Control.Unification.Ranked.IntVar + ( IntVar(..) + , IntRBindingState() + , IntRBindingT() + , runIntRBindingT + , evalIntRBindingT + , execIntRBindingT + ) where + +import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) + +import qualified Data.IntMap as IM +import Control.Applicative +import Control.Monad (MonadPlus(..), liftM) +import Control.Monad.Trans (MonadTrans(..)) +import Control.Monad.State (MonadState(..), StateT, runStateT, evalStateT, execStateT, gets) +import Control.Monad.Logic (MonadLogic(..)) +import Control.Unification.Types +import Control.Unification.IntVar (IntVar(..)) +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | Ranked binding state for 'IntVar'. +data IntRBindingState t = IntRBindingState + { nextFreeVar :: {-# UNPACK #-} !Int + , varBindings :: IM.IntMap (Rank IntVar t) + } + +-- Can't derive this because it's an UndecidableInstance +instance (Show (t (MutTerm IntVar t))) => + Show (IntRBindingState t) + where + show (IntRBindingState nr bs) = + "IntRBindingState { nextFreeVar = "++show nr++ + ", varBindings = "++show bs++"}" + +-- | The initial @IntRBindingState@. +emptyIntRBindingState :: IntRBindingState t +emptyIntRBindingState = IntRBindingState minBound IM.empty + + +---------------------------------------------------------------- +-- | A monad for storing 'IntVar' bindings, implemented as a 'StateT'. +-- For a plain state monad, set @m = Identity@; for a backtracking +-- state monad, set @m = Logic@. +newtype IntRBindingT t m a = IRBT { unIRBT :: StateT (IntRBindingState t) m a } + +-- For portability reasons, we're intentionally avoiding +-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like. + +instance (Functor m) => Functor (IntRBindingT t m) where + fmap f = IRBT . fmap f . unIRBT + +-- BUG: can't reduce dependency to Applicative because of StateT's instance. +instance (Functor m, Monad m) => Applicative (IntRBindingT t m) where + pure = IRBT . pure + x <*> y = IRBT (unIRBT x <*> unIRBT y) + x *> y = IRBT (unIRBT x *> unIRBT y) + x <* y = IRBT (unIRBT x <* unIRBT y) + +instance (Monad m) => Monad (IntRBindingT t m) where + return = IRBT . return + m >>= f = IRBT (unIRBT m >>= unIRBT . f) + +instance MonadTrans (IntRBindingT t) where + lift = IRBT . lift + +-- BUG: can't reduce dependency to Alternative because of StateT's instance. +instance (Functor m, MonadPlus m) => Alternative (IntRBindingT t m) where + empty = IRBT empty + x <|> y = IRBT (unIRBT x <|> unIRBT y) + +instance (MonadPlus m) => MonadPlus (IntRBindingT t m) where + mzero = IRBT mzero + mplus ml mr = IRBT (mplus (unIRBT ml) (unIRBT mr)) + +instance (Monad m) => MonadState (IntRBindingState t) (IntRBindingT t m) where + get = IRBT get + put = IRBT . put + +-- N.B., we already have (MonadLogic m) => MonadLogic (StateT s m), +-- provided that logict is compiled against the same mtl/monads-fd +-- we're getting StateT from. Otherwise we'll get a bunch of warnings +-- here. +instance (MonadLogic m) => MonadLogic (IntRBindingT t m) where + msplit (IRBT m) = IRBT (coerce `liftM` msplit m) + where + coerce Nothing = Nothing + coerce (Just (a, m')) = Just (a, IRBT m') + + interleave (IRBT l) (IRBT r) = IRBT (interleave l r) + + IRBT m >>- f = IRBT (m >>- (unIRBT . f)) + + ifte (IRBT b) t (IRBT f) = IRBT (ifte b (unIRBT . t) f) + + once (IRBT m) = IRBT (once m) + +---------------------------------------------------------------- + +runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t) +runIntRBindingT (IRBT m) = runStateT m emptyIntRBindingState + + +-- | N.B., you should explicitly apply bindings before calling this +-- function, or else the bindings will be lost +evalIntRBindingT :: (Monad m) => IntRBindingT t m a -> m a +evalIntRBindingT (IRBT m) = evalStateT m emptyIntRBindingState + + +execIntRBindingT :: (Monad m) => IntRBindingT t m a -> m (IntRBindingState t) +execIntRBindingT (IRBT m) = execStateT m emptyIntRBindingState + +---------------------------------------------------------------- + +instance (Unifiable t, Applicative m, Monad m) => + BindingMonad IntVar t (IntRBindingT t m) + where + + lookupVar (IntVar v) = IRBT $ do + mb <- gets (IM.lookup v . varBindings) + case mb of + Nothing -> return Nothing + Just (Rank _ mb') -> return mb' + + freeVar = IRBT $ do + ibs <- get + let v = nextFreeVar ibs + if v == maxBound + then error "freeVar: no more variables!" + else do + put $ ibs { nextFreeVar = v+1 } + return $ IntVar v + + newVar t = IRBT $ do + ibs <- get + let v = nextFreeVar ibs + if v == maxBound + then error "newVar: no more variables!" + else do + let bs' = IM.insert v (Rank 0 (Just t)) (varBindings ibs) + put $ ibs { nextFreeVar = v+1, varBindings = bs' } + return $ IntVar v + + bindVar (IntVar v) t = IRBT $ do + ibs <- get + let bs' = IM.insertWith f v (Rank 0 (Just t)) (varBindings ibs) + f (Rank _0 jt) (Rank r _) = Rank r jt + put $ ibs { varBindings = bs' } + + +instance (Unifiable t, Applicative m, Monad m) => + RankedBindingMonad IntVar t (IntRBindingT t m) + where + lookupRankVar (IntVar v) = IRBT $ do + mb <- gets (IM.lookup v . varBindings) + case mb of + Nothing -> return (Rank 0 Nothing) + Just rk -> return rk + + incrementRank (IntVar v) = IRBT $ do + ibs <- get + let bs' = IM.insertWith f v (Rank 1 Nothing) (varBindings ibs) + f (Rank _1 _n) (Rank r mb) = Rank (r+1) mb + put $ ibs { varBindings = bs' } + + incrementBindVar (IntVar v) t = IRBT $ do + ibs <- get + let bs' = IM.insertWith f v (Rank 1 (Just t)) (varBindings ibs) + f (Rank _1 jt) (Rank r _) = Rank (r+1) jt + put $ ibs { varBindings = bs' } + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/Ranked/STVar.hs b/src/Control/Unification/Ranked/STVar.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/Ranked/STVar.hs @@ -0,0 +1,146 @@ + +{-# LANGUAGE Rank2Types + , MultiParamTypeClasses + , UndecidableInstances + , FlexibleInstances + #-} + +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.06 +-- | +-- Module : Control.Unification.Ranked.STVar +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : highly experimental +-- Portability : semi-portable (Rank2Types, MPTCs,...) +-- +-- A ranked variant of "Control.Unification.STVar". +---------------------------------------------------------------- +module Control.Unification.Ranked.STVar + ( STRVar() + , STRBinding() + , runSTRBinding + ) where + +import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) + +import Data.STRef +import Data.Word (Word8) +import Control.Applicative (Applicative(..)) +import Control.Monad (ap) +import Control.Monad.Trans (lift) +import Control.Monad.ST +import Control.Monad.Reader (ReaderT, runReaderT, ask) +import Control.Unification.Types +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | A ranked unification variable implemented by 'STRef's. In +-- addition to the @STRef@ for the term itself, we also track the +-- variable's ID (to support visited-sets) and rank (to support +-- weighted path compression). +data STRVar s t a = + STRVar + {-# UNPACK #-} !Int + {-# UNPACK #-} !(STRef s Word8) + {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STRVar s t) t))) +-- BUG: can we actually unpack STRef? +-- BUG: we need a phantom @a@ to get the kinds to work out now... + +instance Show (STRVar s t a) where + show (STRVar i _ _) = "STRVar " ++ show i + +instance Variable (STRVar s t) where + eqVar (STRVar i _ _) (STRVar j _ _) = i == j + + getVarID (STRVar i _ _) = i + + +---------------------------------------------------------------- +-- TODO: parameterize this so we can use BacktrackST too. Or course, +-- that means defining another class for STRef-like variables +-- +-- TODO: parameterize this so we can share the implementation for STVar and STRVar +-- +-- TODO: does MTL still have the overhead that'd make it worthwhile +-- to do this manually instead of using ReaderT? +-- +-- | A monad for handling 'STRVar' bindings. +newtype STRBinding s a = STRB { unSTRB :: ReaderT (STRef s Int) (ST s) a } + + +-- | Run the 'ST' ranked binding monad. N.B., because 'STRVar' are +-- rank-2 quantified, this guarantees that the return value has no +-- such references. However, in order to remove the references from +-- terms, you'll need to explicitly apply the bindings. +runSTRBinding :: (forall s. STRBinding s a) -> a +runSTRBinding stb = + runST (newSTRef minBound >>= runReaderT (unSTRB stb)) + + +-- For portability reasons, we're intentionally avoiding +-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like. + +instance Functor (STRBinding s) where + fmap f = STRB . fmap f . unSTRB + +instance Applicative (STRBinding s) where + pure = return + (<*>) = ap + (*>) = (>>) + x <* y = x >>= \a -> y >> return a + +instance Monad (STRBinding s) where + return = STRB . return + stb >>= f = STRB (unSTRB stb >>= unSTRB . f) + + +---------------------------------------------------------------- + +_newSTRVar + :: String + -> Maybe (MutTerm (STRVar s t) t) + -> STRBinding s (STRVar s t (MutTerm (STRVar s t) t)) +_newSTRVar fun mb = STRB $ do + nr <- ask + lift $ do + n <- readSTRef nr + if n == maxBound + then error $ fun ++ ": no more variables!" + else do + writeSTRef nr $! n+1 + -- BUG: no applicative ST + rk <- newSTRef 0 + ptr <- newSTRef mb + return (STRVar n rk ptr) + + +instance (Unifiable t) => BindingMonad (STRVar s t) t (STRBinding s) where + lookupVar (STRVar _ _ p) = STRB . lift $ readSTRef p + + freeVar = _newSTRVar "freeVar" Nothing + + newVar t = _newSTRVar "newVar" (Just t) + + bindVar (STRVar _ _ p) t = STRB . lift $ writeSTRef p (Just t) + + +instance (Unifiable t) => + RankedBindingMonad (STRVar s t) t (STRBinding s) + where + + lookupRankVar (STRVar _ r p) = STRB . lift $ do + n <- readSTRef r + mb <- readSTRef p + return (Rank n mb) + + incrementRank (STRVar _ r _) = STRB . lift $ do + n <- readSTRef r + writeSTRef r $! n+1 + + -- incrementBindVar = default + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/STVar.hs b/src/Control/Unification/STVar.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/STVar.hs @@ -0,0 +1,125 @@ + +{-# LANGUAGE Rank2Types + , MultiParamTypeClasses + , UndecidableInstances + , FlexibleInstances + #-} + +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} +---------------------------------------------------------------- +-- ~ 2011.07.06 +-- | +-- Module : Control.Unification.STVar +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : experimental +-- Portability : semi-portable (Rank2Types, MPTCs,...) +-- +-- This module defines an implementation of unification variables +-- using the 'ST' monad. +---------------------------------------------------------------- +module Control.Unification.STVar + ( STVar() + , STBinding() + , runSTBinding + ) where + +import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1) + +import Data.STRef +import Control.Applicative (Applicative(..), (<$>)) +import Control.Monad (ap) +import Control.Monad.Trans (lift) +import Control.Monad.ST +import Control.Monad.Reader (ReaderT, runReaderT, ask) +import Control.Unification.Types +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | Unification variables implemented by 'STRef's. In addition to +-- the @STRef@ for the term itself, we also track the variable's +-- ID (to support visited-sets). +data STVar s a = + STVar + {-# UNPACK #-} !Int + {-# UNPACK #-} !(STRef s (Maybe a)) +-- BUG: can we actually unpack STRef? + +instance Show (STVar s a) where + show (STVar i _) = "STVar " ++ show i + +instance Variable (STVar s) where + eqVar (STVar i _) (STVar j _) = i == j + + getVarID (STVar i _) = i + + +---------------------------------------------------------------- +-- TODO: parameterize this so we can use BacktrackST too. Or course, +-- that means defining another class for STRef-like variables +-- +-- TODO: parameterize this so we can share the implementation for STVar and STRVar +-- +-- TODO: does MTL still have the overhead that'd make it worthwhile +-- to do this manually instead of using ReaderT? +-- +-- | A monad for handling 'STVar' bindings. +newtype STBinding s a = STB { unSTB :: ReaderT (STRef s Int) (ST s) a } + + +-- | Run the 'ST' ranked binding monad. N.B., because 'STVar' are +-- rank-2 quantified, this guarantees that the return value has no +-- such references. However, in order to remove the references from +-- terms, you'll need to explicitly apply the bindings and ground +-- the term. +runSTBinding :: (forall s. STBinding s a) -> a +runSTBinding stb = + runST (newSTRef minBound >>= runReaderT (unSTB stb)) + + +-- For portability reasons, we're intentionally avoiding +-- -XDeriveFunctor, -XGeneralizedNewtypeDeriving, and the like. + +instance Functor (STBinding s) where + fmap f = STB . fmap f . unSTB + +instance Applicative (STBinding s) where + pure = return + (<*>) = ap + (*>) = (>>) + x <* y = x >>= \a -> y >> return a + +instance Monad (STBinding s) where + return = STB . return + stb >>= f = STB (unSTB stb >>= unSTB . f) + + +---------------------------------------------------------------- + +_newSTVar + :: String + -> Maybe (MutTerm (STVar s) t) + -> STBinding s (STVar s (MutTerm (STVar s) t)) +_newSTVar fun mb = STB $ do + nr <- ask + lift $ do + n <- readSTRef nr + if n == maxBound + then error $ fun ++ ": no more variables!" + else do + writeSTRef nr $! n+1 + STVar n <$> newSTRef mb + +instance (Unifiable t) => BindingMonad (STVar s) t (STBinding s) where + + lookupVar (STVar _ p) = STB . lift $ readSTRef p + + freeVar = _newSTVar "freeVar" Nothing + + newVar t = _newSTVar "newVar" (Just t) + + bindVar (STVar _ p) t = STB . lift $ writeSTRef p (Just t) + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/src/Control/Unification/Types.hs b/src/Control/Unification/Types.hs new file mode 100644 --- /dev/null +++ b/src/Control/Unification/Types.hs @@ -0,0 +1,256 @@ +-- 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. diff --git a/src/Data/Functor/Fixedpoint.hs b/src/Data/Functor/Fixedpoint.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Fixedpoint.hs @@ -0,0 +1,305 @@ + +-- For the Show (Fix f) instance +{-# LANGUAGE UndecidableInstances #-} +-- For 'build' and 'hmap' +{-# LANGUAGE Rank2Types #-} +-- To parse rules. The language extension is for hackery in rules. +{-# OPTIONS_GHC -O2 -fglasgow-exts #-} + +{-# OPTIONS_GHC -Wall -fwarn-tabs #-} + +---------------------------------------------------------------- +-- 2011.07.11 +-- | +-- Module : Data.Functor.Fixedpoint +-- Copyright : Copyright (c) 2007--2011 wren ng thornton +-- License : BSD +-- Maintainer : wren@community.haskell.org +-- Stability : provisional +-- Portability : semi-portable (Rank2Types) +-- +-- This module provides a fixed point operator on functor types. +-- For Haskell the least and greatest fixed points coincide, so we +-- needn't distinguish them. This abstract nonsense is helpful in +-- conjunction with other category theoretic tricks like Swierstra's +-- functor coproducts (not provided by this package). For more on +-- the utility of two-level recursive types, see: +-- +-- * Tim Sheard (2001) /Generic Unification via Two-Level Types/ +-- /and Paramterized Modules/, Functional Pearl, ICFP. +-- +-- * Tim Sheard & Emir Pasalic (2004) /Two-Level Types and/ +-- /Parameterized Modules/. JFP 14(5): 547--587. This is +-- an expanded version of Sheard (2001) with new examples. +-- +-- * Wouter Swierstra (2008) /Data types a la carte/, Functional +-- Pearl. JFP 18: 423--436. +---------------------------------------------------------------- + +module Data.Functor.Fixedpoint + ( + -- * Fixed point operator for functors + Fix(..) + -- * Maps + , hmap, hmapM + , ymap, ymapM + -- * Builders + , build + -- * Catamorphisms + , cata, cataM + , ycata, ycataM + -- * Anamorphisms + , ana, anaM + -- * Hylomorphisms + , hylo, hyloM + ) where + +import Prelude hiding (mapM, sequence) +import Control.Monad hiding (mapM, sequence) +import Data.Traversable + +---------------------------------------------------------------- +---------------------------------------------------------------- + +-- | @Fix f@ is a fix point of the 'Functor' @f@. Note that in +-- Haskell the least and greatest fixed points coincide, so we don't +-- need to distinguish between @Mu f@ and @Nu f@. This type used +-- to be called @Y@, hence the naming convention for all the @yfoo@ +-- functions. +-- +-- This type lets us invoke category theory to get recursive types +-- and operations over them without the type checker complaining +-- about infinite types. The 'Show' instance doesn't print the +-- constructors, for legibility. +newtype Fix f = Fix { unFix :: f (Fix f) } + +-- This requires UndecidableInstances because the context is larger +-- than the head and so GHC can't guarantee that the instance safely +-- terminates. It is in fact safe, however. +instance (Show (f (Fix f))) => Show (Fix f) where + show (Fix f) = show f + +instance (Eq (f (Fix f))) => Eq (Fix f) where + Fix x == Fix y = x == y + Fix x /= Fix y = x /= y + +instance (Ord (f (Fix f))) => Ord (Fix f) where + Fix x `compare` Fix y = x `compare` y + Fix x > Fix y = x > y + Fix x >= Fix y = x >= y + Fix x <= Fix y = x <= y + Fix x < Fix y = x < y + Fix x `max` Fix y = Fix (max x y) + Fix x `min` Fix y = Fix (min x y) + +---------------------------------------------------------------- + +-- | A higher-order map taking a natural transformation @(f -> g)@ +-- and lifting it to operate on @Fix@. +hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g +hmap eps = ana (eps . unFix) + -- == cata (Fix . eps) -- But the anamorphism is a better producer. +{-# INLINE [0] hmap #-} + +{-# RULES +"hmap id" + hmap id = id + +"hmap-compose" + forall (eps :: forall a. g a -> h a) (eta :: forall a. f a -> g a). + hmap eps . hmap eta = hmap (eps . eta) + #-} + + +-- | A monadic variant of 'hmap'. +hmapM + :: (Functor f, Traversable g, Monad m) + => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g) +hmapM eps = anaM (eps . unFix) +{-# INLINE [0] hmapM #-} + +{-# RULES +"hmapM return" hmapM return = return +-- "hmapM-compose" forall eps eta. hmap eps <=< hmap eta = hmapM (eps <=< eta) + #-} + + +-- | A version of 'fmap' for endomorphisms on the fixed point. That +-- is, this maps the function over the first layer of recursive +-- structure. +ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f +ymap f = Fix . fmap f . unFix +{-# INLINE [0] ymap #-} + +{-# RULES +"ymap id" ymap id = id +"ymap-compose" forall f g. ymap f . ymap g = ymap (f . g) + #-} + + +-- | A monadic variant of 'ymap'. +ymapM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f) +ymapM f = liftM Fix . mapM f . unFix +{-# INLINE ymapM #-} + +{-# RULES +"ymapM id" ymapM return = return +-- "ymapM-compose" forall f g. ymapM f <=< ymapM g = ymapM (f <=< g) + #-} + + +---------------------------------------------------------------- +-- BUG: this isn't as helful as normal build\/fold fusion as in Data.Functor.Fusable +-- +-- | Take a Church encoding of a fixed point into the data +-- representation of the fixed point. +build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f +build g = g Fix +{-# INLINE [0] build #-} + +-- N.B., the signature is required on @g@ in order to be Rank-2. +-- The signature is required on @phi@ in order to bring @f@ into +-- scope. Otherwise we'd need -XScopedTypeVariables. +{-# RULES +"build/cata" [1] + forall (phi :: f a -> a) (g :: forall r. (f r -> r) -> r). + cata phi (build g) = g phi + #-} + +---------------------------------------------------------------- +-- | A pure catamorphism over the least fixed point of a functor. +-- This function applies the @f@-algebra from the bottom up over +-- @Fix f@ to create some residual value. +cata :: (Functor f) => (f a -> a) -> (Fix f -> a) +cata phi = self + where + self = phi . fmap self . unFix +{-# INLINE [0] cata #-} + +{-# RULES +"cata-refl" + cata Fix = id + +-- TODO: do we still need eta-expanded variants of rules? +"cata-compose" + forall (eps :: forall a. f a -> g a) phi. + cata phi . cata (Fix . eps) = cata (phi . eps) + #-} + +-- We can't really use this one because of the implication constraint +{- RULES +"cata-fusion" + forall f phi. (f . phi) == (phi . fmap f) ==> + f . cata phi = cata phi +-} + + +-- | A catamorphism for monadic @f@-algebras. Alas, this isn't wholly +-- generic to @Functor@ since it requires distribution of @f@ over +-- @m@ (provided by 'sequence' or 'mapM' in 'Traversable'). +-- +-- N.B., this orders the side effects from the bottom up. +cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a) +cataM phiM = self + where + self = phiM <=< (mapM self . unFix) +{-# INLINE cataM #-} + +-- TODO: other rules for cataM +{-# RULES +"cataM-refl" + cataM (return . Fix) = return + #-} + + +-- TODO: remove this, or add similar versions for ana* and hylo*? +-- | A variant of 'cata' which restricts the return type to being +-- a new fixpoint. Though more restrictive, it can be helpful when +-- you already have an algebra which expects the outermost @Fix@. +-- +-- If you don't like either @fmap@ or @cata@, then maybe this is +-- what you were thinking? +ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f +ycata f = cata (f . Fix) +{-# INLINE ycata #-} + + +-- TODO: remove this, or add similar versions for ana* and hylo*? +-- | Monadic variant of 'ycata'. +ycataM :: (Traversable f, Monad m) + => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f) +ycataM f = cataM (f . Fix) +{-# INLINE ycataM #-} + + +---------------------------------------------------------------- +-- | A pure anamorphism generating the greatest fixed point of a +-- functor. This function applies an @f@-coalgebra from the top +-- down to expand a seed into a @Fix f@. +ana :: (Functor f) => (a -> f a) -> (a -> Fix f) +ana psi = self + where + self = Fix . fmap self . psi +{-# INLINE [0] ana #-} + + +{-# RULES +"ana-refl" + ana unFix = id + +-- BUG: I think I dualized this right... +"ana-compose" + forall (eps :: forall a. f a -> g a) psi. + ana (eps . unFix) . ana psi = ana (eps . psi) + #-} + +-- We can't really use this because of the implication constraint +{- RULES +-- BUG: I think I dualized this right... +"ana-fusion" + forall f psi. (psi . f) == (fmap f . psi) ==> + ana psi . f = ana psi +-} + + +-- | An anamorphism for monadic @f@-coalgebras. Alas, this isn't +-- wholly generic to @Functor@ since it requires distribution of +-- @f@ over @m@ (provided by 'sequence' or 'mapM' in 'Traversable'). +-- +-- N.B., this orders the side effects from the top down. +anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f)) +anaM psiM = self + where + self = (liftM Fix . mapM self) <=< psiM +{-# INLINE anaM #-} + + +---------------------------------------------------------------- +-- Is this even worth mentioning? We can amortize the construction +-- of @Fix f@ (which we'd do anyways because of laziness), but we +-- can't fuse the @f@ away unless we inline all of @psi@, @fmap@, +-- and @phi@ at the use sites. Will inlining this definition be +-- sufficient to do that? + +-- | @hylo phi psi == cata phi . ana psi@ +hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b) +hylo phi psi = self + where + self = phi . fmap self . psi +{-# INLINE hylo #-} + +-- TODO: rules for hylo? + + +-- | @hyloM phiM psiM == cataM phiM <=< anaM psiM@ +hyloM :: (Traversable f, Monad m) + => (f b -> m b) -> (a -> m (f a)) -> (a -> m b) +hyloM phiM psiM = self + where + self = phiM <=< mapM self <=< psiM +{-# INLINE hyloM #-} + +-- TODO: rules for hyloM? + +---------------------------------------------------------------- +----------------------------------------------------------- fin. diff --git a/unification-fd.cabal b/unification-fd.cabal new file mode 100644 --- /dev/null +++ b/unification-fd.cabal @@ -0,0 +1,75 @@ +---------------------------------------------------------------- +-- wren ng thornton ~ 2011.07.11 +---------------------------------------------------------------- + +Name: unification-fd +Version: 0.5.0 +-- By and large Cabal >=1.2 is fine; but >= 1.6 gives tested-with: +-- and source-repository:. +Cabal-Version: >= 1.6 +Build-Type: Simple +Stability: experimental +Copyright: Copyright (c) 2007--2011 wren ng thornton +License: BSD3 +License-File: LICENSE +Author: wren ng thornton +Maintainer: wren@community.haskell.org +Homepage: http://code.haskell.org/~wren/ +Category: Algebra, Algorithms, Compilers/Interpreters, Language, Logic, Unification +Synopsis: Simple generic unification algorithms. +Description: Simple generic unification algorithms. + +Source-Repository head + Type: darcs + Location: http://community.haskell.org/~wren/unification-fd + +---------------------------------------------------------------- +Flag base4 + Default: True + Description: base-4.0 emits "Prelude deprecated" messages in + order to get people to be explicit about which + version of base they use. + +Flag splitBase + Default: True + Description: base-3.0 (GHC 6.8) broke out the packages: array, + bytestring, containers, directory, old-locale, + old-time, packedstring, pretty, process, random. + +---------------------------------------------------------------- +Library + Hs-Source-Dirs: src + Exposed-Modules: Data.Functor.Fixedpoint + , Control.Monad.State.UnificationExtras + , Control.Monad.MaybeK + , Control.Monad.EitherK + , Control.Unification + , Control.Unification.Types + , Control.Unification.STVar + , Control.Unification.IntVar + , Control.Unification.Ranked + , Control.Unification.Ranked.STVar + , Control.Unification.Ranked.IntVar + + Build-Depends: logict >= 0.4 + -- Require a version of base with Applicative. + -- We refuse to do without it any longer. + , base >= 2.0 + -- Require mtl-2 instead of monads-fd; because + -- otherwise we get a clash mixing logict with + -- StateT. And we want stuff from monads-fd, so + -- we can't just fail over to the older mtl. + , mtl >= 2.0 + + if flag(base4) + Build-Depends: base >= 4 && < 5 + else + Build-Depends: base < 4 + + if flag(splitBase) + Build-depends: base >= 3.0, containers + else + Build-depends: base < 3.0 + +---------------------------------------------------------------- +----------------------------------------------------------- fin.