No, not at all. It’s a joke post, abusing the in-memory representation of the Option type to construct numbers. When nesting the Option type, it turns into a densely packed bit vector…
And if I understand the purpose of Fin correctly, you’re picking on the one ‘peasant language’ that actually has something like that built-in.
In Rust, you can specify the type of an array as e.g [u8; 3]. Which is an array containing values of type u8 (unsigned 8-bit integer) with a fixed, compile-time-guaranteed length of 3. So, [u8; 3] could be used to represent an RGB color, for example.
It is an array, not a set, but well, close enough.
Fin is a type of finite oridinals bounded by a nat. For example the WTF type in there is the same type as Fin 8.
Of course every language can have Fin with a fixed integer, like the post suggest, by just stacking options.
However for a properly defined Fin type, the input number is dynamic, serves as a bound for the element of the type. For example, Adga was able to type the fact that nth fibonacci number is a finite ordinal bounded by a function of n. Which I believe is not typable in rust?
No, not at all. It’s a joke post, abusing the in-memory representation of the
Option
type to construct numbers. When nesting theOption
type, it turns into a densely packed bit vector…And if I understand the purpose of
Fin
correctly, you’re picking on the one ‘peasant language’ that actually has something like that built-in.In Rust, you can specify the type of an array as e.g
[u8; 3]
. Which is an array containing values of typeu8
(unsigned 8-bit integer) with a fixed, compile-time-guaranteed length of3
. So,[u8; 3]
could be used to represent an RGB color, for example.It is an array, not a set, but well, close enough.
Fin
is a type of finite oridinals bounded by a nat. For example theWTF
type in there is the same type asFin 8
.Of course every language can have
Fin
with a fixed integer, like the post suggest, by just stacking options.However for a properly defined
Fin
type, the input number is dynamic, serves as a bound for the element of the type. For example, Adga was able to type the fact thatn
th fibonacci number is a finite ordinal bounded by a function ofn
. Which I believe is not typable in rust?