## Stream: math-comp users

### Topic: Meaning of `ChoiceType`

#### Julin Shaji (Oct 03 2023 at 17:04):

What is the need and use for a `ChoiceType`?

I'm totally new to mathcomp and came across it in Chapter 8 of the mathcomp book (didn't read what came before it, that's the reason :grimacing:)

But still wasn't sure.

#### Karl Palmskog (Oct 03 2023 at 17:07):

the most obvious (computer science) application of `choiceType` is arguably for key-value mappings where the key type is not necessarily finite, like in finmap. Even more basic is that you can make sets with finitely many members from a type that has infinitely many members.

#### Julin Shaji (Oct 03 2023 at 17:25):

Well, I was trying out the example from the book like:

``````From mathcomp Require Import all_ssreflect all_algebra.

(* Example from Chapter 8 of mathcomp book *)

Inductive dir: predArgType :=
| South | North | East | West.

(* dir to an existing ordinal ?? *)
Definition d2o (d: dir): 'I_4 :=
match d with
| South => inord 0
| North => inord 1
| East => inord 2
| West => inord 3
end.

Definition o2d (o: 'I_4): option dir :=
match val o with
| 0 => Some South
| 1 => Some North
| 2 => Some East
| 3 => Some West
| _ => None
end.

(* d2o and o2d cancel out *)
Lemma pcan_do4: pcancel d2o o2d.
Proof.
by case; rewrite /o2d /= inordK.
Qed.

Compute (North \in dir).
(* = true : bool *)

Fail Check (North != South).  (* needs EqType *)
Fail Check (#| dir | == 4).   (* needs FinType *)

(* Give structure of ordinals to [dir] *)
Definition dir_eqMixin := PcanEqMixin pcan_do4.
Canonical dir_eqType := EqType dir dir_eqMixin.
Check (North != South).
(* North != South : bool *)

(* [CountType] implies [ChoiceType] by the way.
Here it's explicitly given though *)
Definition dir_choiceMixin := PcanChoiceMixin pcan_do4.
Canonical dir_choiceType := ChoiceType dir dir_choiceMixin.

Definition dir_countMixin := PcanCountMixin pcan_do4.
Canonical dir_countType := CountType dir dir_countMixin.

Definition dir_finMixin := PcanFinMixin pcan_do4.
Canonical dir_finType := FinType dir dir_finMixin.
Check (#| dir | == 4).
(* #|dir| == 4 : bool *)

Check (North != South) && (North \in dir) && (#| dir | == 4).
``````

I was looking for examples to illustrate what having the `choice` and `count` mixins add to the `dir` type.
What could be such examples?

As in, we can do boolean equality checks after adding the `EqType` mixin and find cardinality (that's it, right) after adding mixin for `FinType`.
Something similar.

#### Paolo Giarrusso (Oct 03 2023 at 17:59):

"Countable" means your type is isomorphic with a subset of the naturals

#### Julin Shaji (Oct 03 2023 at 18:04):

Does that entail having a function like `ord North` giving `0: nat` in this case?

#### Pierre Roux (Oct 03 2023 at 18:13):

More precisely that there exist an injection into N (finite sets are countable for instance)

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 18:21):

Indeed a motivation for having both choiceType and countable is to allow to have an instance of choiceType for the reals, which are not in bijection with N.

#### Emilio Jesús Gallego Arias (Oct 03 2023 at 18:21):

most CS applications would only care about countable

Last updated: Jul 15 2024 at 20:02 UTC