lurk-rs icon indicating copy to clipboard operation
lurk-rs copied to clipboard

Proposal: make nil and t first-class booleans.

Open porcuquine opened this issue 1 year ago • 0 comments

          This is paused without having been changed yet. There is a new candidate plan, which involves making `nil` and `t` both have type `Bool`, with values 0 and 1 — to maximize clarity and efficiency in circuits.

Originally posted by @porcuquine in https://github.com/lurk-lab/lurk-rs/issues/216#issuecomment-1655963489

The most important point here is that in circuits, boolean values are constrained to be either 0 or 1. Since Lurk reduction circuits (or any circuits that manipulate Lurk data as part of their logic) sometimes need to 'coerce' values between Lurk (tagged field elements) and circuit (constrained field elements) boolean. This change will allow doing so by either simply adding — or else checking and discarding a boolean type tag.

If we do this, the following should all become true:

  • All list-terminator-like expressions (i.e. "", ~()~, ()) should have value 0.
  • nil and t should become normal symbols naming constants whose values are false and true (naming/representation tbd).
  • if will continue to use 'generalized boolean' values, so any value other than false will be interpreted as true.
  • false will be the empty list, i.e. (eq false ()) will be true.
  • 'nil will just be a symbol, so (eq 'nil ()) will be false.

Open question: what should the default printed representations of false and true? Scheme uses #f and #t, and that would be simple. On the other hand, we are not going to drop equivalence of nil/#f and () — so #f may be confusing. One possible answer is #nil and #t. That would signal both the first-class boolean nature, lean on Scheme's convention, but also signal our distinct usage.

It would also minimize wtf in interactions like the following:

> nil
[1 iterations] => #nil
> t
[1 iterations] => #t
> 

Scheme also allows the alternate syntax #false and #true – which are still printed as #t and #f respectively. We already follow Common Lisp and do similarly for () and nil, which are currently alternate input syntaxes respecting the multi-modal function of the value.

At the most extreme, all of the following could be equivalent readable representations:

  • #nil => {#f, nil, (), #false}
  • #t => {#true, t }

Note that even if the above are true, nil and t will not be self-evaluating. 'nil and 't would be distinct (symbol) values.

porcuquine avatar Jul 28 '23 16:07 porcuquine