rvs314 / faster-clpset-minikanren

A fast implementation of miniKanren with CLP(Set) constraints, disequality and absento, compatible with Racket and Chez.
MIT License
0 stars 0 forks source link

The tail of a set is not enforced to be a set #1

Open webyrd opened 3 months ago

webyrd commented 3 months ago

From a discussion between Will and Raffi:

Will's question:

What happens if someone called symbolo or numbero on the tail of the set?  Would that succeed, because of the lack of seto constraint on the tail?

Raffi responded in the affirmative, with this example:

(run* (p q)
  (== p (set-cons 1 q))
  (symbolo q))
;; => '((((set* 1 _.0) _.0) (sym _.0)))

As far as I (Will) understand it, this is an error in the current implementation, unless it makes sense for a set-cons to have a non-set tail.

Maybe I don't fully understand this issue. Raffi, does it make sense for set-cons to have a non-set tail, in the same way that cons can take a non-list as its second argument? Or must a set-cons have an honest-to-goodness set as its tail?

In the latter case, I think we should enforce the set-ness of the tail.

Thanks!

rvs314 commented 1 week ago

This should be fixed by de9632fbcbf20d66b060941dca8626bfaa9808ec (if all works correctly). I've added a few test cases, but I need more.