lurk-rs
lurk-rs copied to clipboard
Proposal: make nil and t first-class booleans.
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 value0
. -
nil
andt
should become normal symbols naming constants whose values arefalse
andtrue
(naming/representation tbd). -
if
will continue to use 'generalized boolean' values, so any value other thanfalse
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.