On the Distinction Between `loobean` and `boolean`

DavePearce commented 3 months ago

This is a feature request from @OlivierBBB to reconsider whether it is useful to distinguish between loobean and boolean. The argument against distinguishing them is roughly that having duplicate primitives, such as a eq vs eq! and or vs or! is awkward and can lead to confusion. I want to think through the implications here so we understand the tradeoffs.

Summary

The reason for distinguishing between loobean and boolean is that logic is interpreted different depending upon its context. In most cases, loobean semantics makes sense as we want 0 to be true (e.g. for vanishing constraints). An obvious situation where we want the opposite is with guards, which are adopt boolean semantics (i.e. because they are typically columns where 1 is used to indicate true).

Examples

Example where eq is used (there is only one occurrence in fact):

(defcolumns STAMP CT CT_MAX)

(defconstraint test ()
  (if-not-zero STAMP
        (if (eq CT CT_MAX)
            (will-inc! STAMP 1))))

This is odd and can actually be rewritten using if-eq.

Example where and is used:

(defcolumns X Y Z)

(defconstraint test ()
  (if-not-zero
   (and (will-inc! X 1) (will-remain-constant! Y))
   (vanishes! Z)))

Another example where and is used:

(module m1)
(defcolumns A)

(module m2)
(defcolumns V X Y)

(deflookup test
    ;; target
    (m1.A)
    ;; source
    ((* V (and X Y))))

An example where or! is used:

(defcolumns STAMP)

(defconstraint heartbeat ()
  (or! (will-remain-constant! STAMP) (will-inc! STAMP 1)))

Finally, I didn't find any situations where and or or! are used in guards. However, there are situations where they could be used in guards, such as:

(defcolumns STAMP X Y)

(defun (eq-stamp)
  (- STAMP (prev STAMP)))

(defconstraint test (:guard (* (eq-stamp) X))
  (vanishes! Y))

Here, the guard could have been expressed as (and (eq-stamp) X).

Notes

No columns marked as loob or bool.
and! and or are never used. However, and and or! are used.
eq is only used in one place (see example above), whilst eq! is used in many places.

delehef commented 3 months ago

Those were mostly tentatives to introduce type-safe, compiler-checked, higher-level, building blocks, but it turns out that implementors preferred to fall back on primitives such as multiplications & subtraction, specific if-eq, etc.

So if they are mostly a support burden without application, I reckon dropping them is not the worst idea.

DavePearce commented 3 months ago

Those were mostly tentatives to introduce type-safe, compiler-checked, higher-level, building blocks

Yes, I understand what you were trying to do here. It would be nice to see things move more towards being a "regular" programming language!! I can see now that that is definitely possible.

Anyway, thanks for the input. What I'm hearing is that there is nothing really major I didn't know about which would block this.

Consensys / corset