Post #4404269
2026-08-05 05:11 UTC
@ramin_hal9001@fe.disroot.org I think I said they were von Neumann bottlenecks *like* monads. If we consider this stobj.lisp :
(in-package "ACL2")
(defstobj words
(words-seen :type t :initially ()))
(defun add-word
(words word)
(declare (xargs :stobjs (words)))
(let ((words
(if (true-listp (words-seen words))
(update-words-seen
(append
(words-seen words)
(list word))
words)
words)))
(mv
words
(words-seen words))))
Replies (1)
-
@screwlisp@gamerplus.org 2026-08-05 05:13
@ramin_hal9001@fe.disroot.org Whence we can see: $ cert.pl ./stobj.lisp $ acl2 ACL2 !>(include-book "stobj") ACL2 !>(add-word words "hello") ( ("hello")) ACL2 !>(add-word words "world") ( ("hello" "world")) acl2 describes stobjs as taking the draconian approach that stobjs are so syntactically restricted that it is unambiguous that there is only ever one state. In practice, any access to a stobj must return that stobj (i.e. with mv ~ values).