unification-fd 0.5.0 → 0.6.0
raw patch · 16 files changed
+220/−111 lines, 16 filesdep ~base
Dependency ranges changed: base
Files
- AUTHORS +44/−0
- LICENSE +1/−1
- README +55/−0
- VERSION +16/−0
- src/Control/Monad/EitherK.hs +11/−12
- src/Control/Monad/MaybeK.hs +7/−7
- src/Control/Monad/State/UnificationExtras.hs +3/−4
- src/Control/Unification.hs +8/−9
- src/Control/Unification/IntVar.hs +8/−6
- src/Control/Unification/Ranked.hs +1/−2
- src/Control/Unification/Ranked/IntVar.hs +6/−4
- src/Control/Unification/Ranked/STVar.hs +5/−9
- src/Control/Unification/STVar.hs +11/−12
- src/Control/Unification/Types.hs +17/−21
- src/Data/Functor/Fixedpoint.hs +16/−17
- unification-fd.cabal +11/−7
+ AUTHORS view
@@ -0,0 +1,44 @@+=== Haskell unification-fd package AUTHORS/THANKS file ===++The unification-fd package was written by wren ng thornton and is+released under the terms in the LICENSE file.+++=== Thanks ===++Christopher Anand --- for partially funding this work at McMaster+ University during the summer of 2011.++Nathaniel W. Filardo --- for helping to figure out the intricacies+ of unification in Dyna2 (though this code is at best loosely+ based on that work).++Edward Kmett --- for pointing out the weighted extension to path+ compression (popular in the union--find literature), and for+ suggsting the switch to having variables be of kind * rather+ than *->*+++=== Related Work ===++The two-level types approach was adapted from Tim Sheard[1]. The+initial (simple yet naive) implementation of unification was based+on Sheard's presentation of Cardelli's[2] algorithm in Modula-2.+Efficient backtracking search via the logict library is described+by Kiselyov et al.[3] The idea of functional pointers were independently+discovered by Dijkstra et al.[4] after their apperance in Dyna2.+++[1] Tim Sheard (2001) /Generic Unification via Two-Level Types and/+ /Parameterized Modules/, Functional Pearl, ICFP.++[2] Luca Cardelli (1987) /Basic polymorphic typechecking/. Science+ of Computer Programming, 8(2):147--172.++[3] Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr+ Sabry (2005) /Backtracking, Interleaving, and Terminating/+ /Monad Transformers/, ICFP.++[4] Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)+ /Efficient Functional Unification and Substitution/, Technical+ Report UU-CS-2008-027, Utrecht University.
LICENSE view
@@ -10,7 +10,7 @@ === unification-fd license === -Copyright (c) 2007, 2008, 2011, wren ng thornton.+Copyright (c) 2007, 2008, 2011, 2012, wren ng thornton. ALL RIGHTS RESERVED. Redistribution and use in source and binary forms, with or without
+ README view
@@ -0,0 +1,55 @@+unification-fd+==============++This is a simple package and should be easy to install. You should+be able to use one of the following standard methods to install it.++ -- With cabal-install and without the source:+ $> cabal install unification-fd+ + -- With cabal-install and with the source already:+ $> cd unification-fd+ $> cabal install+ + -- Without cabal-install, but with the source already:+ $> cd unification-fd+ $> runhaskell Setup.hs configure --user+ $> runhaskell Setup.hs build+ $> runhaskell Setup.hs test+ $> runhaskell Setup.hs haddock --hyperlink-source+ $> runhaskell Setup.hs install++The test step is optional and currently does nothing. If you see+some stray lines that look like this:++ mkUsageInfo: internal name? t{tv a7XM}++Feel free to ignore them. They shouldn't cause any problems, even+though they're unsightly. This should be fixed in newer versions+of GHC. For more details, see:++ http://hackage.haskell.org/trac/ghc/ticket/3955++If you get a bunch of type errors about there being no MonadLogic+instance for StateT, this means that your copy of the logict library+is not compiled against the same mtl that we're using. To fix this,+update logict to use the same mtl.+++Portability+===========++An attempt has been made to keep this library as portable as possible,+but it does rely on some common language extensions (i.e., ones+implemented by Hugs as well as GHC) as well as a couple which are+only known to be supported by GHC. All required language extensions+are:++ Rank2Types+ MultiParamTypeClasses+ FunctionalDependencies -- Alas, necessary for type inference+ FlexibleContexts -- Generally necessary for practical use of MPTCs+ FlexibleInstances -- Generally necessary for practical use of MPTCs+ UndecidableInstances -- Needed for Show instances due to two-level types++----------------------------------------------------------- fin.
+ VERSION view
@@ -0,0 +1,16 @@+0.6.0 (2012-02-17):+ - Removed the phantom type argument for Variables.+0.5.0 (2011-07-12):+ - Moved UnificationFailure to Control.Unification.Types+ - Renamed NonUnifiable to TermMismatch+ - Control.Unification: exposed fullprune, semiprune, occursIn+ - Control.Unification: added unifyOccurs, subsumes+ - Control.Unification: (re)added symbolic names for binary operators+0.4.0 (2011-07-07):+ - Removed heterogeneous unification, and rewrote practically everything.+ - Added semipruning instead of full pruning.+ - Added visited-sets instead of occurs-checks.+ - Added weightedness to path compression (a la union--find).+ - This is the version emailed for the 2011-07-07 talk at McMaster.+0.3.6 (2011-06-18):+ - Forked from the Dyna2 project.
src/Control/Monad/EitherK.hs view
@@ -1,4 +1,3 @@- -- The MPTCs and FlexibleInstances are only for -- mtl:Control.Monad.Error.MonadError {-# LANGUAGE Rank2Types, MultiParamTypeClasses, FlexibleInstances #-}@@ -68,41 +67,41 @@ -- | Execute an @EitherK@ and return the concrete @Either@ encoding. runEitherK :: EitherK e a -> Either e a-runEitherK (EK m) = m Right {-# INLINE runEitherK #-}+runEitherK (EK m) = m Right -- | Lift an @Either@ into an @EitherK@. toEitherK :: Either e a -> EitherK e a+{-# INLINE toEitherK #-} 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 #-}+throwEitherK e = EK (\_ -> Left e) -- | 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 #-}+catchEitherK m handler = eitherK handler return m -- | 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+{-# INLINE eitherK #-} eitherK left right m = case runEitherK m of Left e -> left e Right a -> right a-{-# INLINE eitherK #-} instance Functor (EitherK e) where@@ -142,36 +141,36 @@ -- | 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 #-}+runEitherKT (EKT m) = m (return . Right) -- | Lift an @Either@ into an @EitherKT@. toEitherKT :: (Monad m) => Either e a -> EitherKT e m a+{-# INLINE toEitherKT #-} 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 #-}+liftEitherK = toEitherKT . runEitherK -- 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 #-}+lowerEitherK = liftM toEitherK . runEitherKT -- | 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 #-}+throwEitherKT e = EKT (\_ -> return (Left e)) -- | Handle errors in the @EitherKT@ monad. N.B., this type is more@@ -180,12 +179,12 @@ catchEitherKT :: (Monad m) => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a+{-# INLINE catchEitherKT #-} 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
src/Control/Monad/MaybeK.hs view
@@ -59,15 +59,15 @@ -- | Execute the @MaybeK@ and return the concrete @Maybe@ encoding. runMaybeK :: MaybeK a -> Maybe a-runMaybeK (MK m) = m return {-# INLINE runMaybeK #-}+runMaybeK (MK m) = m return -- | Lift a @Maybe@ into @MaybeK@. toMaybeK :: Maybe a -> MaybeK a+{-# INLINE toMaybeK #-} toMaybeK Nothing = mzero toMaybeK (Just a) = return a-{-# INLINE toMaybeK #-} -- | A version of 'maybe' for convenience. This is almost identical@@ -75,11 +75,11 @@ -- as well as handling @Nothing@ errors. If you only want to handle -- the errors, use 'mplus' instead. maybeK :: b -> (a -> b) -> MaybeK a -> b+{-# INLINE maybeK #-} maybeK nothing just m = case runMaybeK m of Nothing -> nothing Just a -> just a-{-# INLINE maybeK #-} instance Functor MaybeK where@@ -116,29 +116,29 @@ -- | 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 #-}+runMaybeKT (MKT m) = m (return . Just) -- | Lift a @Maybe@ into an @MaybeKT@. toMaybeKT :: (Monad m) => Maybe a -> MaybeKT m a+{-# INLINE toMaybeKT #-} 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 #-}+liftMaybeK = toMaybeKT . runMaybeK -- 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 #-}+lowerMaybeK = liftM toMaybeK . runMaybeKT instance Functor (MaybeKT m) where
src/Control/Monad/State/UnificationExtras.hs view
@@ -1,11 +1,10 @@- {-# LANGUAGE MultiParamTypeClasses #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- -- ~ 2011.07.05 -- | -- Module : Control.Monad.State.UnificationExtras--- Copyright : Copyright (c) 2008--2011 wren ng thornton+-- Copyright : Copyright (c) 2008--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : perpetually unstable@@ -47,20 +46,20 @@ -- | A strict version of 'modify'. modify' :: (MonadState s m) => (s -> s) -> m ()+{-# INLINE modify' #-} 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+{-# INLINE localState #-} localState m = do s <- get x <- m put s return x-{-# INLINE localState #-} ---------------------------------------------------------------- ----------------------------------------------------------- fin.
src/Control/Unification.hs view
@@ -1,11 +1,10 @@- {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ------------------------------------------------------------------- ~ 2011.07.11+-- ~ 2012.02.17 -- | -- Module : Control.Unification--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : experimental@@ -87,7 +86,7 @@ ---------------------------------------------------------------- ---------------------------------------------------------------- --- BUG: this assumes there are no directly-cyclic chains!+-- N.B., 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@@ -108,7 +107,7 @@ return finalTerm --- BUG: this assumes there are no directly-cyclic chains!+-- N.B., 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@@ -140,7 +139,7 @@ -- 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 :: (BindingMonad v t m) => v -> MutTerm v t -> m Bool occursIn v t0 = do t <- fullprune t0 case t of@@ -157,15 +156,15 @@ , MonadTrans e , MonadError (UnificationFailure v t) (e m) )- => v (MutTerm v t) -- ^+ => v -- ^ -> MutTerm v t -- ^ -> StateT (IM.IntMap (MutTerm v t)) (e m) ()+{-# INLINE seenAs #-} 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 #-} ---------------------------------------------------------------- ----------------------------------------------------------------@@ -182,7 +181,7 @@ -- | 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 :: (BindingMonad v t m) => MutTerm v t -> m [v] getFreeVars = \t -> IM.elems <$> evalStateT (loop t) IS.empty where
src/Control/Unification/IntVar.hs view
@@ -1,11 +1,13 @@--{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}+{-# LANGUAGE MultiParamTypeClasses+ , FlexibleInstances+ , UndecidableInstances+ #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ------------------------------------------------------------------- ~ 2011.07.06+-- ~ 2012.02.17 -- | -- Module : Control.Unification.IntVar--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : experimental@@ -54,13 +56,13 @@ -- -- N.B., because this implementation is pure, we can use it for -- both ranked and unranked monads.-newtype IntVar t = IntVar Int+newtype IntVar = IntVar Int deriving (Show) {- -- BUG: This part works, but we'd want to change Show IntBindingState too. -instance Show (IntVar t) where+instance Show IntVar where show (IntVar i) = "IntVar " ++ show (boundedInt2Word i) -- | Convert an integer to a word, via the continuous mapping that
src/Control/Unification/Ranked.hs view
@@ -1,11 +1,10 @@- {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ---------------------------------------------------------------- -- ~ 2011.07.11 -- | -- Module : Control.Unification.Ranked--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : highly experimental
src/Control/Unification/Ranked/IntVar.hs view
@@ -1,11 +1,13 @@--{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}+{-# 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+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : highly experimental@@ -66,7 +68,7 @@ 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.+-- N.B., it's not possible to reduce the dependency to Applicative. instance (Functor m, Monad m) => Applicative (IntRBindingT t m) where pure = IRBT . pure x <*> y = IRBT (unIRBT x <*> unIRBT y)
src/Control/Unification/Ranked/STVar.hs view
@@ -1,16 +1,14 @@- {-# LANGUAGE Rank2Types , MultiParamTypeClasses , UndecidableInstances , FlexibleInstances #-}- {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ------------------------------------------------------------------- ~ 2011.07.06+-- ~ 2012.02.17 -- | -- Module : Control.Unification.Ranked.STVar--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : highly experimental@@ -41,15 +39,13 @@ -- 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 =+data STRVar s t = 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+instance Show (STRVar s t) where show (STRVar i _ _) = "STRVar " ++ show i instance Variable (STRVar s t) where@@ -102,7 +98,7 @@ _newSTRVar :: String -> Maybe (MutTerm (STRVar s t) t)- -> STRBinding s (STRVar s t (MutTerm (STRVar s t) t))+ -> STRBinding s (STRVar s t) _newSTRVar fun mb = STRB $ do nr <- ask lift $ do
src/Control/Unification/STVar.hs view
@@ -1,16 +1,14 @@- {-# LANGUAGE Rank2Types , MultiParamTypeClasses , UndecidableInstances , FlexibleInstances #-}- {-# OPTIONS_GHC -Wall -fwarn-tabs #-} ------------------------------------------------------------------- ~ 2011.07.06+-- ~ 2012.02.17 -- | -- Module : Control.Unification.STVar--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : experimental@@ -40,16 +38,15 @@ -- | 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 =+data STVar s t = STVar {-# UNPACK #-} !Int- {-# UNPACK #-} !(STRef s (Maybe a))--- BUG: can we actually unpack STRef?+ {-# UNPACK #-} !(STRef s (Maybe (MutTerm (STVar s t) t))) -instance Show (STVar s a) where+instance Show (STVar s t) where show (STVar i _) = "STVar " ++ show i -instance Variable (STVar s) where+instance Variable (STVar s t) where eqVar (STVar i _) (STVar j _) = i == j getVarID (STVar i _) = i@@ -99,8 +96,8 @@ _newSTVar :: String- -> Maybe (MutTerm (STVar s) t)- -> STBinding s (STVar s (MutTerm (STVar s) t))+ -> Maybe (MutTerm (STVar s t) t)+ -> STBinding s (STVar s t) _newSTVar fun mb = STB $ do nr <- ask lift $ do@@ -111,7 +108,9 @@ writeSTRef nr $! n+1 STVar n <$> newSTRef mb -instance (Unifiable t) => BindingMonad (STVar s) t (STBinding s) where+instance (Unifiable t) =>+ BindingMonad (STVar s t) t (STBinding s)+ where lookupVar (STVar _ p) = STB . lift $ readSTRef p
src/Control/Unification/Types.hs view
@@ -4,12 +4,11 @@ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-}- ------------------------------------------------------------------- ~ 2011.07.11+-- ~ 2012.02.17 -- | -- Module : Control.Unification.Types--- Copyright : Copyright (c) 2007--2011 wren ng thornton+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : experimental@@ -50,11 +49,11 @@ -- variable type should implement 'Variable'. The 'Show' instance -- doesn't show the constructors, for legibility. data MutTerm v t- = MutVar !(v (MutTerm v t))+ = MutVar !v | MutTerm !(t (MutTerm v t)) -instance (Show (v (MutTerm v t)), Show (t (MutTerm v t))) =>+instance (Show v, Show (t (MutTerm v t))) => Show (MutTerm v t) where showsPrec p (MutVar v) = showsPrec p v@@ -85,7 +84,7 @@ -- the errors), the extra complexity is not considered worth it. data UnificationFailure v t - = OccursIn (v (MutTerm v t)) (MutTerm v t)+ = OccursIn v (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@@ -117,7 +116,7 @@ -- Can't derive this because it's an UndecidableInstance-instance (Show (t (MutTerm v t)), Show (v (MutTerm v t))) =>+instance (Show (t (MutTerm v t)), Show v) => Show (UnificationFailure v t) where -- TODO: implement 'showsPrec' instead@@ -144,10 +143,7 @@ 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.+-- | An implementation of unification variables. class Variable v where -- | Determine whether two variables are equal /as variables/,@@ -155,12 +151,12 @@ -- implementation is: -- -- > eqVar x y = getVarID x == getVarID y- eqVar :: v a -> v b -> Bool+ eqVar :: v -> v -> 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+ getVarID :: v -> Int ----------------------------------------------------------------@@ -181,24 +177,24 @@ -- | 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))+ lookupVar :: v -> m (Maybe (MutTerm v t)) -- | Generate a new free variable guaranteed to be fresh in -- @m@.- freeVar :: m (v (MutTerm v t))+ freeVar :: m v -- | 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 :: MutTerm v t -> m v 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 ()+ bindVar :: v -> MutTerm v t -> m () ----------------------------------------------------------------@@ -216,7 +212,7 @@ 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))) =>+instance (Show v, Show (t (MutTerm v t))) => Show (Rank v t) where show (Rank n mb) = "Rank "++show n++" "++show mb@@ -240,16 +236,16 @@ 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)+ lookupRankVar :: v -> m (Rank v t) -- | Increase the rank of a variable by one.- incrementRank :: v (MutTerm v t) -> m ()+ incrementRank :: v -> 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 -> MutTerm v t -> m () incrementBindVar v t = do { incrementRank v ; bindVar v t } ----------------------------------------------------------------
src/Data/Functor/Fixedpoint.hs view
@@ -1,4 +1,3 @@- -- For the Show (Fix f) instance {-# LANGUAGE UndecidableInstances #-} -- For 'build' and 'hmap'@@ -7,12 +6,11 @@ {-# 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+-- Copyright : Copyright (c) 2007--2012 wren ng thornton -- License : BSD -- Maintainer : wren@community.haskell.org -- Stability : provisional@@ -97,9 +95,9 @@ -- | 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+{-# INLINE [0] hmap #-} hmap eps = ana (eps . unFix) -- == cata (Fix . eps) -- But the anamorphism is a better producer.-{-# INLINE [0] hmap #-} {-# RULES "hmap id"@@ -115,8 +113,8 @@ 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 #-}+hmapM eps = anaM (eps . unFix) {-# RULES "hmapM return" hmapM return = return@@ -128,8 +126,8 @@ -- 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 #-}+ymap f = Fix . fmap f . unFix {-# RULES "ymap id" ymap id = id@@ -138,9 +136,10 @@ -- | 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+ymapM :: (Traversable f, Monad m)+ => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f) {-# INLINE ymapM #-}+ymapM f = liftM Fix . mapM f . unFix {-# RULES "ymapM id" ymapM return = return@@ -154,8 +153,8 @@ -- | 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 #-}+build g = g Fix -- 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@@ -171,10 +170,10 @@ -- 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)+{-# INLINE [0] cata #-} cata phi = self where self = phi . fmap self . unFix-{-# INLINE [0] cata #-} {-# RULES "cata-refl"@@ -200,10 +199,10 @@ -- -- N.B., this orders the side effects from the bottom up. cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)+{-# INLINE cataM #-} cataM phiM = self where self = phiM <=< (mapM self . unFix)-{-# INLINE cataM #-} -- TODO: other rules for cataM {-# RULES@@ -220,16 +219,16 @@ -- 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 #-}+ycata f = cata (f . Fix) -- 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 #-}+ycataM f = cataM (f . Fix) ----------------------------------------------------------------@@ -237,10 +236,10 @@ -- 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)+{-# INLINE [0] ana #-} ana psi = self where self = Fix . fmap self . psi-{-# INLINE [0] ana #-} {-# RULES@@ -268,10 +267,10 @@ -- -- N.B., this orders the side effects from the top down. anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))+{-# INLINE anaM #-} anaM psiM = self where self = (liftM Fix . mapM self) <=< psiM-{-# INLINE anaM #-} ----------------------------------------------------------------@@ -283,10 +282,10 @@ -- | @hylo phi psi == cata phi . ana psi@ hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)+{-# INLINE hylo #-} hylo phi psi = self where self = phi . fmap self . psi-{-# INLINE hylo #-} -- TODO: rules for hylo? @@ -294,10 +293,10 @@ -- | @hyloM phiM psiM == cataM phiM <=< anaM psiM@ hyloM :: (Traversable f, Monad m) => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)+{-# INLINE hyloM #-} hyloM phiM psiM = self where self = phiM <=< mapM self <=< psiM-{-# INLINE hyloM #-} -- TODO: rules for hyloM?
unification-fd.cabal view
@@ -1,24 +1,28 @@ ------------------------------------------------------------------- wren ng thornton <wren@community.haskell.org> ~ 2011.07.11+-- wren ng thornton <wren@community.haskell.org> ~ 2012.02.17 ---------------------------------------------------------------- -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++Name: unification-fd+Version: 0.6.0 Stability: experimental-Copyright: Copyright (c) 2007--2011 wren ng thornton-License: BSD3-License-File: LICENSE+Homepage: http://code.haskell.org/~wren/ Author: wren ng thornton Maintainer: wren@community.haskell.org-Homepage: http://code.haskell.org/~wren/+Copyright: Copyright (c) 2007--2012 wren ng thornton+License: BSD3+License-File: LICENSE+ Category: Algebra, Algorithms, Compilers/Interpreters, Language, Logic, Unification Synopsis: Simple generic unification algorithms. Description: Simple generic unification algorithms. +Extra-source-files:+ AUTHORS, README, VERSION Source-Repository head Type: darcs Location: http://community.haskell.org/~wren/unification-fd