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 -----