How to encode the axiom of choice in Haskell/Functional programming?

Question

> {-# LANGUAGE RankNTypes #-}

I was wondering if there was a way to represent the axiom of choice in haskell and/or some other functional programming language.

As we know, false is represented by the type with no values (Void in haskell).

> import Data.Void

We can represent negation like so

> type Not a = a -> Void

We can express the law of excluded middle for a type a like so

> type LEM a = Either a (a -> Void)

This means we can make constructive logic into a Reader monad

> type Constructive a = (forall r. LEM r) -> a

We can, for example, do double negation elimination in it

> doubleneg :: Constructive (((a -> Void) -> Void) -> a)
> doubleneg = \lem nna -> either id (absurd . nna) lem

We can also have a monad where the law of excluded middle fails

> type AntiConstructive a = ((forall r. LEM r) -> Void) -> a

Now the question is, how can we make a type that represents the axiom of choice? The axiom of choice talks about sets of sets. This implies we would need types of types or something. Is there something equivalent to the axiom of choice that could be encoded? (If you can encode the negation, just combine it with the law of excluded middle). Maybe trickery would allow us to have types of types.

Note: Ideally, it should be a version of the axiom of choice that works with Diaconescu's theorem.

Downvoted on the grounds that this question does not show any research effort: Googling for "axiom of choice agda" gives quite a lot of discussion of how to do this. — Daniel Wagner
@DanielWagner If there is no previous discussion on stackexchange about this topic, then it is on-topic regardless of what else you can find on google. The founders of stackexchange have written about this many times. The whole philosophy is to be that resource that future people find while searching google. — Nick Alger
@NickAlger Yes; for that reason, I did not (and will not) vote to close the question, which is the action to take for off-topic things. (I think it's perfectly reasonable for the question-goodness-vote count and the close-vote count to mean different things.) — Daniel Wagner
The version of the axiom that applies to indexed sets, or are we trying to reason about even uncountable sets? — Davislor

chi chi · Accepted Answer · 2015-12-06T09:31:03

This is just a hint.

The axiom of choice can be expressed as:

If for every x : A there's a y : B such that the property P x y holds, then there's a choice function f : A -> B such that, for all x : A we have P x (f x).

More precisely

choice : {A B : Set} (P : A -> B -> Set) ->
   ((x : A) -> Σ B (λ y -> P x y)) ->
   Σ (A -> B) (λ f -> (x : A) -> P x (f x))
choice P h = ?

given

data Σ (A : Set) (P : A -> Set) : Set where
  _,_ : (x : A) -> P x -> Σ A P

Above, choice is indeed provable. Indeed, h assigns to each x a (dependent) pair whose first component y is an element of A and the second component is a proof that the first indeed satisfies P x y. Instead, the f in the thesis must assign to x only y, without any proof.

As you see, obtaining the choice function f from h is just a matter of discarding the proof component in the pair.

There's no need to extend Agda with LEM or any other axiom to prove this. The above proof is entirely constructive.

If we were using Coq, note that Coq forbids to eliminate a proof (such as h : ... -> Prop) to construct a non-proof (f), so translating this into Coq directly fails. (This is to allow program extraction.) However, if we avoid the Prop sort of Coq and use Type directly, then the above can be translated.

You may want to use the following projections for this exercise:

pr1 : ∀ {A : Set} {P} -> Σ A P -> A
pr1 (x , _) = x

pr2 : ∀ {A : Set} {P} -> (p : Σ A P) -> P (pr1 p)
pr2 (_ , y) = y

How to encode the axiom of choice in Haskell/Functional programming?

1 Answers