- Let q(x) be a property provable about objects x of type T. Then q(y) should be true for objects y of type S where S is a subtype of T.
My Bogus was an attempt to abstract a method by which I could get access to a variable using a syntatic-sugar idiom. The abstraction leaks. Here is how it leaks:
(should-maintain-scope-of-inner-property (with-property (value 24) (value :is (incf (value)))) (assert-equal 25 (value)))
‘incf’ is a destructive operation.
Here is a possible implementation of ‘incf’:
(defmacro my-incf (place &optional (val 1)) (let ((v (gensym)) (a (gensym))) `(let* ((,v ,val) (,a (+ ,place ,v))) (setf ,place ,a))))
It’s that last form (setf ,place ,a) that breaks the LSP. The only way we can change the actual value of my abstraction is with the keyword symbol :is. So in the end, the operation we were trying to abstract out is what causes the abstraction to leak.
I still think that there is some promise here, it just needs to be pushed on some more.
On Lisp still amazes me with the amount of information in it. My understanding if ‘incf’ comes from this. Use the on-line version and do searches.
Another nice read is “Technical Issues of Separation in Function Cells and Value Cells”.