<p>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.</p>
<p>This common pattern of bitflags has the expectation of bitflags has the properties that</p>
<ol>
<li>All constants are different</li>
<li>Applying the or operation of two of the constants produces another constant</li>
</ol>
<p>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.</p>
<p>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.</p>

<types><functional-programming><type-systems>
What is the mathematical abstraction of bitflags for use in a purely functional language?
CC BY-SA 4.0
2024-02-22T23:48:13.217Z
Set / subset? You have a set of possible bitflags, and then a bitflag instance can be represented by a subset of those elements.
tarzh
CC BY-SA 4.0
2024-02-23T00:39:57.053Z
@tarzh but it does not define the operation of adding and or comparing their elements in a natural way
Delfin
CC BY-SA 4.0
2024-02-23T01:04:53.067Z
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.
chc4
<p>It is a set.</p>
<p>The bitwise OR of 2 bitflag values results in the union of the 2 sets.</p>
<p>The bitwise AND of 2 bitflag values results in the intersection of the 2 sets.</p>
<p>The bitwise NOT of a bitflag value results in the complementary set.</p>
<p>Every other operation you would care about can be constructed from those.</p>
<p>Adding a single element means getting the union of the set and the singleton set with the element. <code>flags | ELEMENT</code></p>
<p>Removing a single element means getting the intersection of the set and the complement of the singleton set with the element. <code>flags &amp; ~ELEMENT</code></p>
<p>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.</p>

CC BY-SA 4.0
2024-02-23T12:27:50.257Z
2024-02-23T12:27:50.257Z
ratchet freak
CC BY-SA 4.0
2024-02-23T12:49:58.560Z
As said we can make so that is function signature is what checks for message validity
Delfin
CC BY-SA 4.0
2024-02-23T22:32:10.580Z
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
Delfin
<p>Speaking <a href="https://en.wikipedia.org/wiki/Structural_type_system" rel="nofollow noreferrer">structurally</a>, if one has <a href="https://en.wikipedia.org/wiki/Ordinal_data_type" rel="nofollow noreferrer">ordinal types</a>, then one can encode bitsets, bitvectors, and bitflags with a single uniform signature: a mapping from ordinals to Booleans.</p>
<p>For example, consider the type <code>8 → 2</code> as a representation of octets. Each element of <code>8</code> indexes a single bit.</p>
<p>Note that there are 256 possible octets, and also that by type arithmetic, there are 256 possible (pure total) functions with signature <code>8 → 2</code>. So, the first criterion is met: all constant octets are distinct in this encoding.</p>
<p>For the second criterion, note that Boolean operations like <code>OR</code> can be lifted <a href="https://en.wikipedia.org/wiki/Pointwise" rel="nofollow noreferrer">elementwise</a> from Booleans to functions which target Booleans; if <code>f</code> and <code>g</code> are octets, then we could take the <code>OR</code> of their outputs. In Haskell syntax:</p>
<pre><code>\i -&gt; f i || g i
</code></pre>
<p>In Scheme syntax:</p>
<pre><code>(lambda (i) (or (f i) (g i)))
</code></pre>
<p>This is related to other answers, which mention sets, by the concept that the type <code>8 → 2</code> is the type of characteristic functions (<a href="https://en.wikipedia.org/wiki/Characteristic_function" rel="nofollow noreferrer">WP</a>, <a href="https://ncatlab.org/nlab/show/characteristic+function" rel="nofollow noreferrer">nLab</a>) for any eight-element set.</p>

CC BY-SA 4.0
2024-02-24T18:16:30.133Z
2024-02-24T18:16:30.133Z
Corbin
CC BY-SA 4.0
2024-02-24T19:19:17.420Z
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
Delfin
CC BY-SA 4.0
2024-02-25T16:55:13.530Z
@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."
Corbin
CC BY-SA 4.0
2024-02-25T16:59:50.697Z
@Carbin Have you heard of [Gost of the deported proofs](https://iohk.io/en/research/library/papers/ghosts-of-departed-proofs-functional-pearls/)?
Delfin
# What is the mathematical abstraction of bitflags for use in a purely functional language?
Posted by: username_0 on 2024-02-22
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.
**Tags:** types functional-programming type-systems
> **Comments:**
> **username_1**: Set / subset? You have a set of possible bitflags, and then a bitflag instance can be represented by a subset of those elements.  
> **username_0**: @tarzh but it does not define the operation of adding and or comparing their elements in a natural way  
> **username_2**: 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.  
---
## 2 answers
### Answer by username_3 on 2024-02-23. Score: 4
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.
> **Comments:**
> **username_0** (2024-02-23): As said we can make so that is function signature is what checks for message validity  
> **username_0** (2024-02-23): 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  
---
### Answer by username_4 on 2024-02-24. Score: 1
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.
> **Comments:**
> **username_0** (2024-02-24): 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  
> **username_4** (2024-02-25): @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."  
> **username_0** (2024-02-25): @Carbin Have you heard of [Gost of the deported proofs](https://iohk.io/en/research/library/papers/ghosts-of-departed-proofs-functional-pearls/)?  
---
