Created
August 10, 2017 21:55
-
-
Save cakemanny/639c26a3ddb6b1abc79c3c5facbdbfef to your computer and use it in GitHub Desktop.
Unification Algorithm in Haskell
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main where | |
import Data.List (intersperse) | |
type Name = String | |
type Equations = [(Expr,Expr)] | |
data Expr | |
= Func Name [Expr] -- if [Expr] is [], then it's a constant | |
| Var Name | |
deriving (Eq) | |
instance Show Expr where | |
show (Var name) = name | |
show (Func name []) = name | |
show (Func name args) = concat $ [ name, "(", shownArgs, ")"] | |
where shownArgs = concat $ intersperse "," $ map show args | |
{- | |
The unification algorithm from wikipedia: | |
- https://en.wikipedia.org/wiki/Unification_(computer_science) | |
- we ought to change this to return a Maybe or an Either or Failure | |
-} | |
unify :: Equations -> Equations | |
unify eqns = unify' [] eqns | |
where -- here we use g, a set of equations we have already transformed | |
-- to accumulate the result | |
-- delete | |
unify' g ((t1, t2) : xs) | |
| t1 == t2 = unify' g xs | |
-- decompose | |
unify' g ((Func name1 args1, Func name2 args2) : xs) | |
| name1 == name2 && length args1 == length args2 | |
= unify' g $ (args1 `zip` args2) ++ xs | |
-- conflict | |
| otherwise = [] -- fail, function names or arg lengths don't match | |
-- swap | |
unify' g ((f@(Func _ _), v@(Var _)) : xs) = unify' g ((v,f) : xs) | |
-- eliminate | |
unify' g ((Var x, t) : xs) | |
| not (x `elem` vars t) = unify' ((Var x, t) : subst x t g) (subst x t xs) | |
-- check | |
unify' g ((Var x, t@(Func _ _)) : xs) | |
| x `elem` vars t = [] | |
-- does this next case ever actually happen? (Var x, Var y), so yes | |
unify' g (x : xs) = unify' (x : g) xs -- do we recycle x for later? | |
unify' g [] = g | |
subst :: Name -> Expr -> Equations -> Equations | |
subst x t = map substPair | |
where substPair (ex1, ex2) = (subst' ex1, subst' ex2) | |
subst' (Func name exps) = Func name (subst' `map` exps) | |
subst' (Var name) | |
| x == name = t | |
| otherwise = Var name | |
vars :: Expr -> [Name] | |
vars (Func _ exprs) = exprs >>= vars | |
vars (Var name) = [name] | |
main :: IO () | |
main = do putStrLn $ display exampleInput | |
putStrLn " -> " | |
putStrLn $ display $ unify exampleInput | |
where exampleInput = [(Func "list" [Var "y"] , Var "x"), | |
(Func "list" [lit "int"] , Var "x"), | |
(Func "f" [Var "z", Func "g" [Var "w"]], | |
Func "f" [lit "1", Func "g" [Var "z" ]])] | |
lit n = Func n [] | |
display = let displayEqn (g,h) = (show g) ++ " = " ++ (show h) | |
in concat . intersperse "\n" . map displayEqn | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment