1
$\begingroup$

A lot of C APIs like to have something called bit flags to signal the functions configuration options like Vulkan, OpenCL, SQLite and much more, it a typical pattern to it.

This common pattern of bitflags has the expectation of bitflags has the properties that

  1. All constants are different
  2. Applying the or operation of two of the constants produces another constant

The mathematical abstraction would be something similar to a Lattice or some kind of directed-complete partial order, preferably it would not allow for when there is some incompatibility constrains and mandatory constrains that may be enforced at the function signature, id est that you program does not compile if you call the function with illegal mixtures of flags and missing mandatory flags for the function.

This abstraction should give a similar experience to experience with respect to bitflags that these C APIs give to the programmer in the Purely Functional Language that implements such abstraction but also giving the some degree of protection of not mixing incompatible flags.

$\endgroup$
3
  • $\begingroup$ Set / subset? You have a set of possible bitflags, and then a bitflag instance can be represented by a subset of those elements. $\endgroup$
    – tarzh
    Commented Feb 22 at 23:48
  • 1
    $\begingroup$ @tarzh but it does not define the operation of adding and or comparing their elements in a natural way $\endgroup$
    – Delfin
    Commented Feb 23 at 0:39
  • 4
    $\begingroup$ I'm not sure why you are ruling out a Lattice - lattice join is bitwise or, and lattice meet is bitwise and. That's the mathematical backing for datalog engines with lattice relations to allow using a bitfield type, for example. The requirement to be able to express constraints doesn't seem relevant for a bitflag type and sounds like it would devolve into boolean satisfiability for arbitrary constraints. $\endgroup$
    – chc4
    Commented Feb 23 at 1:04

2 Answers 2

4
$\begingroup$

It is a set.

The bitwise OR of 2 bitflag values results in the union of the 2 sets.

The bitwise AND of 2 bitflag values results in the intersection of the 2 sets.

The bitwise NOT of a bitflag value results in the complementary set.

Every other operation you would care about can be constructed from those.

Adding a single element means getting the union of the set and the singleton set with the element. flags | ELEMENT

Removing a single element means getting the intersection of the set and the complement of the singleton set with the element. flags & ~ELEMENT

Requiring that you can create constraints on this doesn't feel worth it to bake hard into the type as those constraints can become arbitrarily complex. And in the real world you might need to have a invalid set while you are constructing the one you will eventually pass to the API. Yes even in functional programming.

$\endgroup$
2
  • $\begingroup$ As said we can make so that is function signature is what checks for message validity $\endgroup$
    – Delfin
    Commented Feb 23 at 12:49
  • 1
    $\begingroup$ The biggest problem with your proposal is the lack of structure of a set, that it either only accepts compositions of sets or accepts everyting. A Set-Universe Pair would be a better fit $\endgroup$
    – Delfin
    Commented Feb 23 at 22:32
1
$\begingroup$

Speaking structurally, if one has ordinal types, then one can encode bitsets, bitvectors, and bitflags with a single uniform signature: a mapping from ordinals to Booleans.

For example, consider the type 8 → 2 as a representation of octets. Each element of 8 indexes a single bit.

Note that there are 256 possible octets, and also that by type arithmetic, there are 256 possible (pure total) functions with signature 8 → 2. So, the first criterion is met: all constant octets are distinct in this encoding.

For the second criterion, note that Boolean operations like OR can be lifted elementwise from Booleans to functions which target Booleans; if f and g are octets, then we could take the OR of their outputs. In Haskell syntax:

\i -> f i || g i

In Scheme syntax:

(lambda (i) (or (f i) (g i)))

This is related to other answers, which mention sets, by the concept that the type 8 → 2 is the type of characteristic functions (WP, nLab) for any eight-element set.

$\endgroup$
3
  • $\begingroup$ Certainly a interesting prospect. but still does not take any time to handle the incompatibility problem and the mandatory of bitflags. Nor in function signature nor otherwise $\endgroup$
    – Delfin
    Commented Feb 24 at 19:19
  • $\begingroup$ @Delfin: Sounds like bad API design; use Boolean algebra to split the function taking flags into several functions instead. Remember, with pure total functions, there are no erroring states; it's literally not possible to invoke a function with "illegal mixtures of arguments." $\endgroup$
    – Corbin
    Commented Feb 25 at 16:55
  • $\begingroup$ @Carbin Have you heard of Gost of the deported proofs? $\endgroup$
    – Delfin
    Commented Feb 25 at 16:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .