[Haskell-cafe] My Unification Sorrows
Stefan O'Rear
stefanor at cox.net
Wed Apr 4 17:47:39 EDT 2007
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 -----
More information about the Haskell-Cafe
mailing list