CODEWITHSUNDEEP
haskellcoq
OrenIshShalom
OrenIshShalom

Reputation: 7162

Extracting Prop from Coq to Haskell results in empty type

I'm trying to make sure that a useless Prop is discarded when extracting Coq to Haskell. However, when I use the following example, I see that both divides and prime are extracted as Haskell empty types. Why is that?

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
  exists (m : nat), ((mult m n) = p).

(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
  (p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/some_file.hs" isPrime divides prime.

And here is what happens to divides and prime:

type Divides = ()

type Prime = ()

What's the use of extracting them?

Upvotes: 1

Views: 298

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15414

This is expected behavior. Things from Prop are propositions meaning those are computationally irrelevant because propositions are there to ensure correctness, e.g. to represent pre- and post- conditions of an algorithm, not to take part in computations.

The situation is analogous with that of types in statically-typed languages -- one usually wants to erase types from runtime. Here we would like to have the terms that are proofs erased too.

This is supported by Coq's type system which prohibits leaking logical information from types in Prop to Type, e.g.

Definition foo : True \/ True -> nat :=
  fun t => match t with
        | or_introl _ => 0
        | or_intror _ => 42
        end.

Results in

Error:
Incorrect elimination of "t" in the inductive type "or":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

A natural question arises:

So ideally divides and prime should be eliminated altogether from extracted file right? How come they exist there?

As Pierre Letouzey explains in his overview of extraction in Coq:

Let us summarize now the current status of Coq extraction. The theoretical extraction function described in [7] is still relevant and used as the core of the extraction system. This function collapses (but cannot completely remove) both logical parts (living in sort Prop) and types. A complete removal would induce dangerous changes in the evaluation of terms, and can even lead to errors or non- termination in some situations.

Upvotes: 5

Related Questions