alt-romes / hegg

Fast equality saturation in Haskell
https://hackage.haskell.org/package/hegg
BSD 3-Clause "New" or "Revised" License
75 stars 8 forks source link

VariablePattern must be greater than 0 #32

Open BinderDavid opened 10 months ago

BinderDavid commented 10 months ago

I was writing a simple set of rewrite rules for SKI combinatory logic, but I couldn't get the expressions to simplify. Here is the code (simplified) that I used:

The definition of CL Terms:

-- | CLF = CombinatoryLogicFunctor
data CLF r = S | K | I | App r r
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

type CL = Fix CLF

The rewrite rule for I x ~> x:

-- | I x ~> x
rwi :: Rewrite a CLF
rwi = lhs := rhs
  where
    lhs = NonVariablePattern (App (NonVariablePattern I) (VariablePattern 0))
    rhs = VariablePattern 0

But this rewrite rule will not match, and it took me a while to figure out why: The arguments of VariablePattern have to start with 1, if I replace the rule with the following one:

-- | I x ~> x
rwi :: Rewrite a CLF
rwi = lhs := rhs
  where
    lhs = NonVariablePattern (App (NonVariablePattern I) (VariablePattern 1))
    rhs = VariablePattern 1

Then everything works as expected.

alt-romes commented 10 months ago

Ach! That is very unfortunate. I think the API to patterns needs to be somewhat improved, possibly hiding these dark corners (if not fixing them).

For VariablePattern my assumption is that people would be using the IsString instance which uses a simple hash function on the string to determine a "unique" number for the VariablePattern. For instance:

-- | I x ~> x
rwi :: Rewrite a CLF
rwi = lhs := rhs
  where
    lhs = pat (App (pat I) "a")
    rhs = "a"

But I still think that is very crude. I think revisiting the API of patterns could be useful soon 👍.

Thanks for reporting. To fix this we ought to do either or all of

In the meantime I'm keeping this open

alt-romes commented 10 months ago

Accidentally closed while writing the comment. I've edit the response to its final form now.

BinderDavid commented 10 months ago

For VariablePattern my assumption is that people would be using the IsString instance which uses a simple hash function on the string to determine a "unique" number for the VariablePattern

Ah, okay. I wasn't following the tutorial for figuring out how to write patterns, instead I was just following the API and the Haddocks :)

Edit: And now I discovered that there is actually a haddock comment on the VariablePattern constructor which says "Should be a >0 positive number". 🤦