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?
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?