[ refactor ] Data.Product.Relation.Binary.Pointwise.NonDependent - #3081
[ refactor ] Data.Product.Relation.Binary.Pointwise.NonDependent#3081jamesmckinna wants to merge 9 commits into
Data.Product.Relation.Binary.Pointwise.NonDependent#3081Conversation
|
NB. The new definition of ... and the knock-ons for |
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Definitely need to crack that zip nut, as that is the 'right' way to define a number of the things that are now done 'by hand'.
| ------------------------------------------------------------------------ | ||
|
|
||
| {-# OPTIONS --without-K --safe #-} | ||
| {-# OPTIONS --without-K --allow-unsolved-metas #-} |
There was a problem hiding this comment.
I know it's Draft, but I'm leaving this as a note to make sure this doesn't slip through!
There was a problem hiding this comment.
Yes, but this arises from yet more of the same regarding the need to rebind Pointwise-local versions of the Product.* combinators. Very frustrating! Esp. as even with map, it seems necessary to fully apply it, which somewhat defeats the purpose of having the combinators in the first place!
|
|
||
| open Pointwise public | ||
|
|
||
| Pointwise′ : REL A B ℓ₁ → REL C D ℓ₂ → REL (A × C) (B × D) (ℓ₁ ⊔ ℓ₂) |
There was a problem hiding this comment.
Do we need this at all?
There was a problem hiding this comment.
This was part of the experiment:
- to retain the old definition, perhaps with some kind of backwards compatibility in mind (naming stymies this of course)
- but also in case I needed to convert back-and-forth in order to be able to invoke
Product.*combinators... such as insymmetricbelow.
It's why this is still DRAFT!
|
|
||
| ×-symmetric : Symmetric R → Symmetric S → Symmetric (Pointwise R S) | ||
| ×-symmetric sym₁ sym₂ = Product.map sym₁ sym₂ | ||
| ×-symmetric {R = R} {S = S} sym₁ sym₂ (x₁Rx₂ , y₁Sy₂) = sym₁ x₁Rx₂ , sym₂ y₁Sy₂ |
There was a problem hiding this comment.
You don't need to bind R and S on the lhs. And wasn't the map version more elegant? That way you can prove things about ×-symmetric by using results about map instead of having to do them from scratch.
There was a problem hiding this comment.
Re: R and S: yes, you're right. This is debris from earlier versions of this module.
Re: map. The Product version works precisely because Pointwise isn't wrapped as a record... ;-) With the wrapped version, we have
×-symmetric : Symmetric R → Symmetric S → Symmetric (Pointwise R S)
×-symmetric sym₁ sym₂ xR×Sy = map sym₁ sym₂ {!xR×Sy!}but any attempt to refine the last goal with the indicated hypothesis (and hope for an eta-contraction downstream), is thwarted by the fact that
Pointwise (flip R) (flip S) y x(essentially the type of the goal), and(Pointwise R S) x y
are not definitionally equal. Whereas they are if Pointwise is given the old way. Maddening!
There was a problem hiding this comment.
Even with eta-equality for the record type, and making map 'lazier' via
map : ≈₁ ⇒ R → ≈₂ ⇒ S → Pointwise ≈₁ ≈₂ ⇒ Pointwise R S
map f g xR×Sy = f (proj₁ xR×Sy) , g (proj₂ xR×Sy)I find I still have to write
×-symmetric : Symmetric R → Symmetric S → Symmetric (Pointwise R S)
×-symmetric sym₁ sym₂ xR×Sy = map sym₁ sym₂ (proj₁ xR×Sy , proj₂ xR×Sy)Suggestions welcome!
2 participants
Fixes #2174 (or rather: will at some point).
Currently:
zipso that existing uses ofProduct.zipcan be drop-in replacedmapdoesn't work for egsymmetricAdvice welcome!
Alternative strategy: try to make this module a specialisation of
Data.Product.Relation.Binary.Pointwise.Dependent? UPDATED no because the use ofIRELthere opens the door to unsolved metavariables when considering the constantIRELgenerated from a givenREL...NB. Universe levels for the definitions in
{Non}Dependenthave been corrected!UPDATED: I'm abandoning this. The knock-on consequences are so/too painful to fix/figure out... anyone else is welcome to attempt this!