The Coq mailing list

[Dirk Pattinson <dirk.pattinson AT anu.edu.au>]

> > I'm trying to understand the difference between Coq's sum and sumbool when
> > applied to propositions. In particular, what are the benefits of using sumbool
> > over the use of (plain and simple disjoint) sum?
>
> > - both carry computational information
>
> sumbool does not carry information usable outside of Prop.

I agree but am struggling to understand when sum and sumbool are applied 
to arguments of type Prop. In this case, it appears that both carry one 
bit of computational information: left or right, and the computational 
information of sum P Q (where P Q: Prop) isn't usable outside Prop, either.

> > Extraction Language Haskell.
> > Extract Inductive sumbool =>
> >    "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
>
> Right, sumbool is isomorphic to Bool, and sum to Either.  The Prop witnesses
> from the sumbool are erased in the extraction.

The same is true for Prop witnesses of sum, but Extraction slots in a 
dependency on the unit type. This doesn't happen for sumbool.

Differently put: assuming I'm not interested in extraction, could I 
replace "sumbool" by "sum" throughout (assuming I would be prepared to 
also do this in the libraries)?

Dirk.