[Haskell-cafe] My Unification Sorrows

4 Apr 2007

      Ok, so I decided to implement an algorithm to build Strongly Typed Genetic
Programming trees in Haskell, in an effort to learn Haskell,
and I'm way over my head on this unification problem.

The unification seems to work well, as long as I include the occurs check.
growFullTree returns a lazy list of all possible syntax trees in random
order that are well typed. So, with the occurs check:

head $ growFullTree 4 TInt 0 [] (mkStdGen 5)

Gives me a nice, random, well typed tree.  So far so good, although
I am wary of the efficiency... perhaps I need some applySubst calls
in there somewhere to keep the constraint list down?

Anyway now, we comment out the occurs check in the unify function and
do the same thing again.  Now we get what appears to be an infinite
constraint!  The unify is supposed to be terminating without the occurs
check, so something is very wrong here!

Worse, now we run:

head $ growFullTree 5 TInt 0 [] (mkStdGen 7)

This one never even begins printing!  Although it appears the bug is
tail recursive in this case.  Other random number seeds will cause it
to blow stack.

I have gone over and over this code and cannot find the issue due to my
lack of experience with both Haskell and Unification algorithms in general.

I was hoping someone here could give pointers on where the bug might lie, eg.
what is my algorithm doing wrong that makes it a mostly, but not completely
correct unification algorithm, as well as give me pointers on how this
code could be
made cleaner and/or more concise, as I'm trying very hard to get my brain around
this language, and this problem.

Here's the basic code, which should be fully runnable:

module Evaluator
  where

import Maybe
import Random
import Monad

-- | Expressions.
data Exp = Prim String        -- A Primitive Function
         | App Exp Exp        -- An un-evaluated application
         | Func (Exp -> Exp)  -- A partially applied function
         | LitInt Integer
         | LitReal Double
           deriving Show

-- | We name type variables by uniquely picking values of this type.
type TVName = Int

-- | Describes possible types in our language
data Type = TInt
          | TReal
          | TVar TVName
          | Type :-> Type
            deriving (Eq, Show)

-- | Type arrows are right associative to match Haskell's native type arrows.
infixr 9 :->

-- | Constraints are simply a pair of Types which are equal.
type Constraint = (Type, Type)

-- | Returns a new type variable name, given an old one.
getNextName :: TVName -> TVName
getNextName n = n + 1

-- | Evaluate an expression.
eval :: Exp -> Exp
eval (Prim s)  = fst . fromJust $ lookup s primitives
eval (App f x) = apply f x
eval x         = x

-- | Apply a function.
apply :: Exp -> Exp -> Exp
apply a@(App _ _) x = eval $ App (eval a) x
apply p@(Prim _)  x = eval $ App (eval p) x
apply (Func f)    x = eval $ f x
apply f           x = error $ (show f) ++ " was applied to " ++ (show
x) ++ " and is not a valid function."

-- | Given a set of constraints (possibly empty), the next available
variable name and an expression,
-- return a triple which consists of the inferred type of the
expression, the next available variable name,
-- and a list of constraints for the new type.
infer :: [Constraint] -> TVName -> Exp -> (Type, TVName, [Constraint])
infer _ nvar (LitInt _)  = (TInt, nvar, [])
infer _ nvar (LitReal _) = (TReal, nvar, [])
infer _ nvar (Prim s)    = (t, nvar', [])
  where (nvar', t, _) = substvars nvar (snd . fromJust $ lookup s primitives) []

infer ctx nvar (App t1 t2) = (TVar nvar'', getNextName nvar'',
newconstr : (ctx' ++ ctx''))
  where (tyT1, nvar', ctx')   = infer ctx nvar t1
        (tyT2, nvar'', ctx'') = infer ctx nvar' t2
        newconstr             = (tyT1, tyT2 :-> TVar nvar'')

infer _ _ (Func _) = error "Type Inferrence of partially applied
functions not supported"

-- | Given a unified constraint list and a type, return a simplified type
applySubst :: Type -> [Constraint] -> Type
applySubst tyT ctx = foldl (\tyS (tyX,tyC) -> substinty tyX tyC tyS)
tyT (reverse ctx)

-- | We need to substitute all the type variables in a primitive with new
-- ones that do not clash with the variables already defined in our
-- constraint set.  This function does that, by taking the next available
-- variable name and creating a set of substitutions over a type that
-- replace the old variable names with newly generated ones
substvars :: TVName -> Type -> [(TVName, TVName)] -> (TVName, Type,
[(TVName, TVName)])
substvars nvar (TVar n) ctx =
  case lookup n ctx of
         (Just n') -> (nvar, TVar n', ctx)
         Nothing   -> (getNextName nvar, TVar nvar, (n, nvar) : ctx)

substvars nvar (t1 :-> t2) ctx =
  (nvar'', t1' :-> t2', ctx'')
    where (nvar', t1', ctx')   = substvars nvar t1 ctx
          (nvar'', t2', ctx'') = substvars nvar' t2 ctx'

substvars nvar t ctx = (nvar, t, ctx)

-- | returns the type of an expression if it has one
typeof :: Exp -> Maybe Type
typeof e = fmap (applySubst t) (unify ctx)
  where (t, _, ctx) = infer [] 0 e

-- | Substitutes a type for a type variable
substinty :: Type -> Type -> Type -> Type
substinty tyX tyT (s1 :-> s2) = (substinty tyX tyT s1) :-> (substinty
tyX tyT s2)
substinty tyX tyT tyS@(TVar _)
  | tyS == tyX = tyT
  | otherwise  = tyS

substinty _ _ tyS = tyS

-- | Substitutes a type for another type in a constraint set.
substinconstr :: Type -> Type -> [Constraint] -> [Constraint]
substinconstr tyX tyT = map (\(x,y) -> (substinty tyX tyT x, substinty
tyX tyT y))

-- | Checks to see if a type occurs in another type.  This is used to identify
-- infinite types.
occursIn :: Type -> Type -> Bool
occursIn tx (ty1 :-> ty2) = (occursIn tx ty1) || (occursIn tx ty2)
occursIn tx ty            = tx == ty

-- | 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)
  -- Problems start by commenting out this line
  | tyX `occursIn` tyS                     = fail "Infinite Type"
  | otherwise                              = fmap (++ [(tyX,tyS)])
(unify $ substinconstr tyX tyS (reverse 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"

-- | The basic primitives used to construct expressions.
primitives :: [(String, (Exp, Type))]
primitives = [("B",   (b_, ((TVar 0) :-> (TVar 1)) :-> ((TVar 2) :->
(TVar 0)) :-> (TVar 2) :-> (TVar 1))),
              ("I",   (i_, (TVar 0) :-> (TVar 0))),
              ("K",   (k_, (TVar 0) :-> (TVar 1) :-> (TVar 0))),
              ("S",   (s_, ((TVar 0) :-> (TVar 1) :-> (TVar 2)) :->
((TVar 0) :-> (TVar 1)) :-> (TVar 0) :-> (TVar 2))),
              ("Add", (add, TInt :-> TInt :-> TInt)),
              -- ("Y",   (y_, (TVar 0 :-> TVar 0) :-> TVar 0)),
              ("Uno", (LitInt 1, TInt))]

-- Some primitives to play with
s_ = Func (\x -> Func (\y -> Func (\z -> App (App x z) (App y z))))
k_ = Func (\x -> Func (\_ -> x))
i_ = Func (\x -> x)
y_ = Func (\f -> let x = (App f x) in x)
b_ = Func (\f -> Func (\g -> Func (\x -> App f (App g x))))
add = Func (\x -> Func (\y -> case (eval x,eval y) of
                                ((LitInt x', LitInt y')) -> LitInt $ x' + y'
                                _                        -> error
"Addition applied to non integers not implemented"))

-- | given a Type and a list of constraints for that type, and another
primitive type and the next available type variable,
-- return a new next available type variable, the type of the
primitive and a new list of constraints, if the type
-- is unifiable.
primitiveUnifies :: (Monad m, Functor m) => Type -> [Constraint] ->
Type -> TVName -> m (TVName, Type, [Constraint])
primitiveUnifies t1 cs t2 nvar = fmap construct (unify $ (t2',t1):cs)
  where (nvar',t2',_) = substvars nvar t2 []
        construct x   = (nvar', t2', x)

-- | Given a type, the next available type variable, and a list of constraints,
-- return a list of primitives which unify to that type, the type of
the primitive, a new next available
-- type variable, and a new list of constraints
findTypeMatch :: Type -> TVName -> [Constraint] -> [(String, Type,
TVName, [Constraint])]
findTypeMatch t nvar c = foldr foldFunc [] primitives
  where construct name (nvar', ty, constr) = (name, ty, nvar', constr)
        foldFunc (name,(_,ty)) xs = let result = primitiveUnifies t c ty nvar in
                                        maybe xs (:xs) $ fmap
(construct name) result

-- | Give the depth of the tree, they type to return, the next
available type variable, a list of constraints on type variables,
-- and a random generator, and this will return a list of full-depth
trees meeting those constraints from the primitives.
growFullTree :: Int -> Type -> TVName -> [Constraint] -> StdGen ->
[(Exp, TVName, [Constraint], StdGen)]
growFullTree 0 ty nvar c g
  | optionlist == [] = mzero
  | otherwise        = do (func, _, nvar', c') <- optionlist
                          return (Prim func, nvar', c', g')
  where (optionlist, g') = shuffle (findTypeMatch ty nvar c) g
growFullTree depth ty nvar c g = do (func,  nvar',  c', g')   <-
growFullTree (depth - 1) (TVar nvar :-> ty) (getNextName nvar) c  g
                                    (param, nvar'', c'', g'') <-
growFullTree (depth - 1) (TVar nvar)        nvar'              c' g'
                                    return ((App func param), nvar'', c'', g'')

-- | Insert a value into a list at the given index
insert_ix :: Int -> a -> [a] -> [a]
insert_ix 0 a lst = a : lst
insert_ix (k + 1) a (l:ls) = l : insert_ix k a ls

-- | insert a value into a list at a random index
insert_rand :: (RandomGen g) => a -> [a] -> g -> ([a], g)
insert_rand a lst g1 = let (ix,g2) = randomR (0,length lst) g1 in
                         (insert_ix ix a lst, g2)

-- | Shuffle a list
shuffle :: (RandomGen g) => [a] -> g -> ([a], g)
shuffle [] g1 = ([], g1)
shuffle (x:xs) g1 = let (xs', g2) = shuffle xs g1 in
                      insert_rand x xs' g2

[Haskell-cafe] My Unification Sorrows

Paul Berg