{------------------------------------------------------------------- -- (Transcriber:) wren ng thornton ~ 2008.03.28 -- -- This module provides a generic unification engine as described in: -- -- Tim Sheard, 2001, Generic Unification via Two-Level Types -- and Paramterized Modules. ICFP -- -- Note that we've removed all the working examples in order to -- provide a truly generic module. For the worked examples, see the -- paper or my other files where I've worked things out alongside -- reading the paper. -------------------------------------------------------------------} -- N.B. This must be run with non-Haskell98 extensions because our -- modular interfaces use rank-2 polymorphism. In ghc/gchi -- this will enable those extensions (you could also pass this -- flag on the commandline), In Hugs you need to use the '-98' -- flag. {-# LANGUAGE Rank2Types #-} {-# OPTIONS_GHC -Wall -fwarn-tabs #-} -- Hugs imports the constructors and accessors for our existential -- types for free, but GHCi doesn't so we need to declare them as -- do our clients module Unification ( RSclass(..) , GT(S,MutVar,GenVar) , Ptr , GTstruct(..) , makeUnify ) where import Control.Functor.Fixedpoint (Fix(..)) import Control.Monad (ap, liftM) -- Poor man's applicative (<*>) :: (Monad m) => m (a -> b) -> m a -> m b (<*>) = ap (<$>) :: (Monad m) => (a -> b) -> m a -> m b (<$>) = liftM infixl 4 <*>, <$> ---------------------------------------------------------------- -- | The RSclass modular interface for defining -- terms \in (Stucture_T, Ref_T, ErrorMonad_T) -- -- These modular interfaces are like existential types for modules -- in ML. So the usage is that we pass an RSclass value into the -- field accessors to get our functions back out. Thus the types -- shown for the accessors are after we've curried out the initial -- RSclass argument. This usage pattern can be seen well in the -- 'makeUnify' definition for GTstruct below. data (Monad m) => RSclass s r m = RSclass { eqVarRS :: forall x . r x -> r x -> Bool , writeVarRS :: forall x . r x -> x -> m () , readVarRS :: forall x . r x -> m x , newVarRS :: forall x . x -> m (r x) , sequenceRS :: forall x . s (m x) -> m (s x) , mapRS :: forall x y . (x -> y) -> (s x -> s y) , foldRS :: forall x y . (x -> y -> y) -> s x -> y -> y , matchRS :: forall x . s x -> s x -> Maybe [(x,x)] -- Should we just use `fail` for our monad? , errorRS :: forall x . String -> m x } ---------------------------------------------------------------- -- The GTstruct modular interface for functions over GT (Appendix A) -- | Generic Terms, hence \"GT\". -- @s@ abstracts over structure, @r@ abstracts over references -- @s@ must be a type constructor, not a type; @r@ as well data GT s r = S (s (GT s r)) | MutVar (Ptr s r) | GenVar Int -- | Pointer types where @Nothing@ represents a null pointer type Ptr s r = r (Maybe (GT s r)) data (Monad m) => GTstruct s r m = GTstruct { unifyGT :: GT s r -> GT s r -> m () , matchGT :: GT s r -> GT s r -> m () , equalGT :: GT s r -> GT s r -> Bool , freshGT :: m (GT s r) , occursGT :: Ptr s r -> GT s r -> m Bool , colGT :: GT s r -> m (GT s r) , pruneGT :: GT s r -> m (GT s r) , instantiateGT :: [GT s r] -> GT s r -> m (GT s r) , tofixGT :: GT s r -> m (Fix s) , fromfixGT :: Fix s -> GT s r } ---------------------------------------------------------------- -- Generate a GTstruct library from an RSclass library makeUnify :: (Monad m) => RSclass s r m -> GTstruct s r m makeUnify lib = GTstruct { unifyGT = unify , matchGT = match , equalGT = equal , freshGT = freshVar , occursGT = occursIn , colGT = col , pruneGT = prune , instantiateGT = instantiate , tofixGT = toFix , fromfixGT = fromFix } where -- These two are just helpful shorthands for the real functions -- seqmap = (sequenceRS lib .) . mapRS lib -- if you prefer points-free seqmap f x = sequenceRS lib (mapRS lib f x) write r x = writeVarRS lib r x ------------------------------------------------------------ freshVar = MutVar <$> newVarRS lib Nothing ------------------------------------------------------------ -- Canonicalize a chain of MutVar so they all point directly -- to the real thing, and return the real thing prune typ@(MutVar ref) = do mb <- readVarRS lib ref case mb of Just t -> do t' <- prune t ref `write` Just t' return t' Nothing -> return typ prune x = return x ------------------------------------------------------------ -- Determine if a Ptr appears somewhere inside a GT (may change Ptrs) occursIn v t = do t' <- prune t case t' of S w -> do s <- seqmap (v `occursIn`) w return (foldRS lib (||) s False) MutVar z -> return (eqVarRS lib v z) GenVar _n -> return False ------------------------------------------------------------ varBind r t = do b <- r `occursIn` t if b then errorRS lib "OccursErr" else r `write` Just t ------------------------------------------------------------ unify tA tB = do t1 <- prune tA t2 <- prune tB case (t1, t2) of (MutVar r1, MutVar r2) -> if eqVarRS lib r1 r2 then return () else r1 `write` Just t2 (MutVar r1, _) -> r1 `varBind` t2 (_, MutVar r2) -> r2 `varBind` t1 (GenVar n, GenVar m) -> if n == m then return () else errorRS lib "Gen error" (S x, S y) -> case matchRS lib x y of Nothing -> errorRS lib "ShapeErr" Just pairs -> mapM_ (uncurry unify) pairs (_,_) -> errorRS lib "ShapeErr" ------------------------------------------------------------ -- This is exactly like `unify` except when MutVar are involved -- I believe this is for seeing if ground term tB matches unground tA match tA tB = do t1 <- prune tA t2 <- prune tB case (t1, t2) of (MutVar r1, _) -> r1 `write` Just t2 (GenVar n, GenVar m) -> if n == m then return () else errorRS lib "Gen error" (S x, S y) -> case matchRS lib x y of Nothing -> errorRS lib "ShapeErr" Just pairs -> mapM_ (uncurry match) pairs (_,_) -> errorRS lib "ShapeErr" ------------------------------------------------------------ -- Test if two GT are identical equal x y = case (x,y) of (MutVar r1, MutVar r2) -> eqVarRS lib r1 r2 (GenVar n, GenVar m) -> m == n (S sx, S sy) -> case matchRS lib sx sy of Nothing -> False Just pairs -> all (uncurry equal) pairs (_,_) -> False ------------------------------------------------------------ -- I'm not entirely sure what `colGT` is supposed to be... -- ...it's used by instantiate and itself only col x = do x' <- prune x case x' of MutVar r -> return (MutVar r) GenVar n -> return (GenVar n) S y -> S <$> seqmap col y ------------------------------------------------------------ -- Generic interface to templated GenVars instantiate sub x = do x' <- prune x case x' of MutVar r -> return (MutVar r) GenVar n -> col (sub !! n) S y -> S <$> seqmap (instantiate sub) y ------------------------------------------------------------ fromFix (Fix x) = S (mapRS lib fromFix x) ------------------------------------------------------------ -- To pull a GT out of the monad when it's ground toFix x = do x' <- prune x case x' of MutVar _r -> errorRS lib "No vars" GenVar _m -> errorRS lib "No generic vars" S y -> Fix <$> seqmap toFix y ---------------------------------------------------------------- ----------------------------------------------------------- fin.