hpaste

data Sample a = Simple a
              | Complex a a

func :: Sample a -> Sample a -> SomethingElse


-- | The 2 definitions do the same thing, but flip their params.
-- Is there a simpler way to express this, requiring only a single definition?
questionFunc :: (Sample a, Sample a) -> SomethingElse
questionFunc (x@(Simple _),y) = func x y
questionFunc (y,x@(Simple _)) = func x y

data Sample a = Simple a
              | Complex a a

func :: Sample a -> Sample a -> SomethingElse


-- | The 2 definitions do the same thing, but flip their params.
-- Is there a simpler way to express this, requiring only a single definition?
questionFunc :: (Sample a, Sample a) -> SomethingElse
questionFunc (x@(Simple _),y) = func x y
questionFunc (x           ,y) = questionFunc (y, x)

-- | Substitutes a constraint in a list of constraints, and unifies the result
unifyAppend :: (Monad m, Functor m) => Type -> Type -> [Constraint] -> m [(Type, Type)]
unifyAppend tyX tyY constraints = fmap (++ [(tyX,tyY)]) (unify $ substinconstr tyX tyY constraints)


-- | Given a list of constraints, unify those constraints, 
-- finding values for the type variables
unify :: (Monad m, Functor m) => [Constraint] -> m [Constraint]
unify [] = return []
unify ((t1,t2):rest) | t1 == t2 = unify rest
unify ((tyS,tyX@(TVar _)):rest) 
  | tyX `occursIn` tyS = fail "Infinite Type"
  | otherwise          = unifyAppend tyX tyS rest
unify ((tyX@(TVar _),tyT):rest)
  | tyX `occursIn` tyT = fail "Infinite Type"
  | otherwise          = unifyAppend tyX tyT rest
unify ((tyS1 :-> tyS2,tyT1 :-> tyT2):rest) = unify $ (tyS1,tyT1) : (tyS2,tyT2) : rest
unify _ = fail "Unsolvable"

(=:=) :: (Eq (r (Binding Term r)),MonadRef m r) => Term' r -> Term' r -> LP m ()
a =:= b = case (isVar a, isVar b) of
            (Just v1, Just v2) | v1 == v2   -> success
            (Just v , _      )              -> unifyVar v b
            (_      , Just v )              -> unifyVar v a
            _                               -> unify a b

-- | Substitutes a constraint in a list of constraints, and unifies the result
unifyAppend :: (Monad m, Functor m) => Type -> Type -> [Constraint] -> m [(Type, Type)]
unifyAppend tyX tyY constraints = fmap (++ [(tyX,tyY)]) (unify $ substinconstr tyX tyY constraints)


-- | Given a list of constraints, unify those constraints, 
-- finding values for the type variables
unify :: (Monad m, Functor m) => [Constraint] -> m [Constraint]
unify []                                   = return []
unify ((t1 ,          t2)           :rest) 
  | t1 == t2                               = unify rest
unify ((tyS,          tyX@(TVar _)) :rest) 
  | tyX `occursIn` tyS                     = fail "Infinite Type"
  | otherwise                              = unifyAppend tyX tyS rest
unify ((tyX@(TVar _), tyT)          :rest) = unify $ (tyT,tyX):rest
unify ((tyS1 :-> tyS2,tyT1 :-> tyT2):rest) = unify $ (tyS1,tyT1) : (tyS2,tyT2) : rest
unify _                                    = fail "Unsolvable"

data Term v = Var v | Term String [Term v] deriving Typeable
type Term' r = Term (r (Binding Term r))
data Binding f r = Unbound | Bound (f (r (Binding f r)))

type LP m a = BacktrT m a

success :: Monad m => LP m ()
success = return ()

failed :: Monad m => LP m a
failed = mzero

unifyVar :: (Eq (r (Binding Term r)),MonadRef m r) => r (Binding Term r) -> Term' r -> LP m ()
unifyVar ref a = do
    mb <- readLPRef ref
    case mb of
        Unbound -> writeLPRef ref (Bound a)
        Bound b  -> a =:= b

(=:=) :: (Eq (r (Binding Term r)),MonadRef m r) => Term' r -> Term' r -> LP m ()
a =:= b = case (isVar a, isVar b) of
            (Just v1, Just v2) | v1 == v2   -> success
            (Just v , _      )              -> unifyVar v b
            (_      , Just v )              -> unifyVar v a
            _                               -> unify a b

isVar :: Term v -> Maybe v
isVar (Var v) = Just v
isVar _       = Nothing

unify :: (Eq (r (Binding Term r)),MonadRef m r) => Term' r -> Term' r -> LP m ()
unify (Term a as) (Term b bs) | a == b    = unifyLists as bs
                              | otherwise = failed
    where unifyLists []      []      = success
          unifyLists (h1:t1) (h2:t2) = h1 =:= h2 >> unifyLists t1 t2
          unifyLists _       _       = failed
unify _           _           = failed

Powered by HAppS. Copyright (c) 2007 glguy @ #haskell. Source via darcs.