Open mikeshulman opened 10 years ago
Most of these reasons apply to most records in the library, don't they?
Records with more than two fields would need to be nested sigma types; using nested projections is painful (e.g., replacing identity C x
with x.2.2.2.1
for precategories), and defining named projections would lose the benefit of primitive projections.
We also can't make pr1
and pr2
coercions, and so we'd have to define extra functions to use as coercions. Because things like rewrite
aren't up to delta, this might cause the occasional mismatch between a theorem using coercions and a theorem using pr1
.
Personally, I prefer records for everything, because this enforces more modularity, and allows us to change the underlying representation, if we wish, without having to change every use of the type. But I'd be ok with replacing the two-field records that don't register either field as a coercion, with sigma types. (I'm not sure how I feel about replacing the ones involving coercions, but if they build without much trouble, I'd probably be fine with it.)
I'm not necessarily advocating the following, but want to propose the possibilities:
Regarding 2, we can make a scope for hProp
and hSet
, and bind (_;_)
to the relevant constructors within that scope. Then, in many cases, Coq can pick up automatically which one we mean (the exception being when we're defining an hProp
/hSet
as, say, the return of a function or a top level definition, rather than to pass as an argument).
Regarding 2 and 3, we can make a coercion hProp >-> sigT
. This should eliminate the need to remember the destructors, at the cost of introducing an extra function into some definitions, and apply <TypeO theorem>
could probably be made to work in this manner.
The exists tactic works for records BTW.
We are currently not using Canonical Structures/ Type Classes a lot, so the benefits are less clear. Our statements look less nice than they could be, since we are using a completely unbundled approach. E.g.
Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A) : Contr A.
Could be
Lemma contr_inhabited_hprop (A : hProp) (x : A) : Contr A.
It's easy to find more elaborate examples. Of course, this can be done with
sig
too, but we'd lack the support for automation.
This was a choice at some point, but we may want to reconsider. Although, I've tried to play with it a bit, but it is not entirely clear how to make maximal use of this.
On Thu, Sep 18, 2014 at 8:27 AM, Andrej Bauer notifications@github.com wrote:
These reasons apply to most records in the library, don't they?
— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/514#issuecomment-55999766.
I agree that records with 3+ fields are generally preferable to nested sigmas. But for 2-field records, especially those whose second field is an hprop, I'm not convinced. I'd like to try it, with coercions, and see whether we run into any trouble.
Another possibility, which I wouldn't like as much but I think would be preferable to the current situation, would be to define a general Subset
record that is just a general sigma whose second component is an hprop. Then we could declare the first projection of Subset
to be a coercion (which we wouldn't want to do for all sigmas), and define things like hProp
using Subset
. We could duplicate the relevant parts of types/Sigma.v
in types/Subset.v
.
The advantage of the unbundled approach is that sometimes we have a type and we know that it's an hprop, but it isn't given to us as an element of hProp
. With the first projection of hProp
declared as a coercion and the second as an instance, the unbundled version is applicable wherever the bundled one would be, but not conversely. Am I wrong?
(Or maybe Subtype
would be better since its first component is not necessarily a set.)
With the first projection of hProp declared as a coercion and the second as an instance, the unbundled version is applicable wherever the bundled one would be, but not conversely. Am I wrong?
We could try harder, but it is not so clear how to do it. In fact, the unbundled approach is what we developed in our math-classes library. http://math-classes.org/ http://dx.doi.org/10.1017/S0960129511000119
The Program tactic was precisely developed to work nicely with subtypes.
On Thu, Sep 18, 2014 at 7:09 PM, Mike Shulman notifications@github.com wrote:
I agree that records with 3+ fields are generally preferable to nested sigmas. But for 2-field records, especially those whose second field is an hprop, I'm not convinced. I'd like to try it, with coercions, and see whether we run into any trouble.
Another possibility, which I wouldn't like as much but I think would be preferable to the current situation, would be to define a general Subset record that is just a general sigma whose second component is an hprop. Then we could declare the first projection of Subset to be a coercion (which we wouldn't want to do for all sigmas), and define things like hProp using Subset. We could duplicate the relevant parts of types/Sigma.v in types/Subset.v.
The advantage of the unbundled approach is that sometimes we have a type and we know that it's an hprop, but it isn't given to us as an element of hProp. With the first projection of hProp declared as a coercion and the second as an instance, the unbundled version is applicable wherever the bundled one would be, but not conversely. Am I wrong?
— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/514#issuecomment-56070910.
The discussion at #543 is very relevant to the argument against using sigmas in the presence of coercions. The confusion that I imagined, and @marcbezem experienced, shows very clearly, I think, that we don't want fields like hproptype
(rather than some renaming of them) to be coercions. An occasional mismatch requiring an extra unfold
before rewriting (which would happen after renaming the coercions whether or not the underlying record were a sigma) is, I think, a very acceptable price to pay for eliminating this confusion.
@mikeshulman Is this issue resolved now?
It should be noted that sigT is implemented itself as a record type with two fields. Therefore it stands to reason that Records and sigma types are equivalent in this case, performance wise. The only real difference being the coercions/subtyping.
So do we want to have coercions/subtyping or allow for various sigma type lemmas to work?
They are definitely not equivalent performance-wise if you work with named projections. If we want to be able to have named definitions for the protections of hProp (rather than notations), then we lose all of the benefit of primitive projections.
(There is another small cost: unification may be slightly slower to fail when trying to unify hProp against another sigma type.)
However, it may turn out that in practice these costs are negligible.
Well, point #2 in the OP suggested that we shouldn't have special names for the projections of hProp. Why would we?
Just to bump this issue, now that we have more control over how sigma types are defined, it may be useful to experiment with this again. I think there are some potential advantages to what Mike highlighted.
I know we discussed this a little bit ago, but I don't remember where or what the arguments were. It seems to me that making it a sigT would have the following advantages:
issig
. We wouldn't have to prove two copies of some theorems, likepath_equiv_biimp
andpath_equiv_biimp_rec
inepi.v
(which ought to be named something more descriptive also).hp
andhproptype
; we could just use the ordinary pairing(_;_)
and projectionspr1
andpr2
. The first time I encountered the constructorhp
I was very confused.@TypeO (truncation_modality -1)
, so we could apply any theorems about the latter to it directly.The same applies to
hSet
and toTruncType
(of whichhProp
andhSet
ought to be special cases rather than their own definitions in any case).