In general, can we list all elements of a finite type?

Stream: new members

[nrs]

Hi! In general, can we algorithmically list all elements in any finite type? Or do we have to prove some properties of a type before such a thing can be done? Or is it not possible in general?

[Johan Commelin]

It depends on what you mean by "finite". If you have an instance of Fintype X that was not constructed using the axiom of choice, then yes: such a list is included in the definition of Fintype and can be extracted algorithmically because no choice was used.

But if you mean Finite X, then it is generally not possible to get such a list. Because Finite X only gives you the information that the type is finite, but nothing about what the elements actually are.

[nrs]

Johan Commelin said:

It depends on what you mean by "finite". If you have an instance of Fintype X that was not constructed using the axiom of choice, then yes: such a list is included in the definition of Fintype and can be extracted algorithmically because no choice was used.

But if you mean Finite X, then it is generally not possible to get such a list. Because Finite X only gives you the information that the type is finite, but nothing about what the elements actually are.

Thanks for the answer! Hm. Then, the type must satisfy some sort minimal order-theoretic properties in order for this to be possible, right?

[nrs]

Ah, found a lead for investigating this. Leaving this here if anyone is interested in the same question: https://en.wikipedia.org/wiki/Computably_enumerable_set

[nrs]

hm, it seems that the most fundamental type satisfying this isMathlib.Data.List (or a literal subset of the integers), everything else that satisfies this is a List with more structure.

[Luigi Massacci]

The typeclass you want in the general case is docs#Encodable

[Violeta Hernández]

You don't need to have a linear order to define a Fintype instance. Though of course, if you can list all the elements of your type, you can surely define an ordering based on that.

[Ruben Van de Velde]

You do need an order to safely extract a list, though