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 (Not a)

This means we can make classical logic into a Reader monad

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

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

> doubleneg :: Classical (Not (Not a) -> a)
> doubleneg = \lem nna -> either id (absurd . nna) lem

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

> type AntiClassical a = Not (forall r. LEM r) -> 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.

Answer 1

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