Skip to content

Instantly share code, notes, and snippets.

@gelisam
Created April 18, 2014 23:19
Show Gist options
  • Save gelisam/11068221 to your computer and use it in GitHub Desktop.
Save gelisam/11068221 to your computer and use it in GitHub Desktop.
unification-fd example
-- in reply to http://www.reddit.com/r/haskell/comments/23dxli/why_are_examples_completely_absent_from_hackage/
{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
import Control.Unification
import Control.Unification.IntVar
import Control.Monad.Identity
import Control.Monad.Trans
import Control.Monad.Trans.Error
import Data.Foldable
import Data.Traversable
-- simple type constructors
data Term a = Con String -- ^ constant types such as "Int" and "String"
| Pair (a, a) -- ^ pairs. Each `a` stands for a `Term a`.
deriving (Show, Eq, Functor, Foldable, Traversable)
instance Unifiable Term where
zipMatch (Con s1) (Con s2) | s1 == s2 = Just $ Con s1
zipMatch (Pair (x1,y1)) (Pair (x2,y2)) = Just $ Pair (Right (x1, x2), Right (y1, y2))
zipMatch _ _ = Nothing
-- type ClosedTerm = Fix Term
type OpenTerm = UTerm Term IntVar
type IntBinding = IntBindingT Term Identity
con :: String -> OpenTerm
con = UTerm . Con
pair :: (OpenTerm, OpenTerm) -> OpenTerm
pair = UTerm . Pair
-- the pairs (a, Int) and (String, b), which unify to (String, Int)
unifiable_pairs :: IntBinding (OpenTerm, OpenTerm)
unifiable_pairs = do v1 <- freeVar
v2 <- freeVar
let t1 = pair (UVar v1, con "Int")
let t2 = pair (con "String", UVar v2)
return (t1, t2)
unify_pairs :: ErrorT (UnificationFailure Term IntVar) IntBinding OpenTerm
unify_pairs = do (t1, t2) <- lift unifiable_pairs
r <- unify t1 t2 -- Pair v1 v2, plus bindings saying:
-- v1 = con "String"
-- v2 = con "Int"
applyBindings r
-- |
-- >>> main
-- Right (Pair (Con "String",Con "Int"))
main :: IO ()
main = print $ (runIdentity . evalIntBindingT . runErrorT) unify_pairs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment