[Haskell-cafe] My Unification Sorrows

[Stefan O'Rear]

I seem to have did an accidental reply-to-sender at first:

On Wed, Apr 04, 2007 at 01:37:44PM -0700, Paul Berg wrote:
> 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:

The problem is with this type:

data Type = TInt
          | TReal
          | TVar TVName
          | Type :-> Type

Because it is impossible to observe sharing in Haskell values, we are
forced to explore the entire type; but without the occurs check the
type can be infinite! 

In my infinite-types unifier, I used this:

data Bin = Sum | Fun | Prod deriving (Eq, Show, Ord)
data Zen = ZTup deriving (Eq,Show,Ord)
data DictElt = EZen Zen | EBin Bin Type Type deriving (Eq, Show, Ord)
type Dict = M.Map Int DictElt

Changing to use Paul's set of types:

data DictElt = TInt | TReal | TVar | Int :-> Int
type Dict = M.Map Int DictElt

IE, we use Ints explicitly as pointers.  However this representation
costs a lot in terms of clarity, since everything must be explicitly
indirected through the 'heap'.  Also fixtypes was a very old project
of mine; were I to do it again I would probably use explicit mutable
references:

data Tinfo s = TInt | TReal | TVar | Type s :-> Type s
type Type s = STRef s (Tinfo s)

This may conflict with your method of backtracking tree generation; I
haven't read that far in the code yet. 

Stefan

----- End forwarded message -----