Refactoring `StrictToNonStrict` and `Closure.Reflexive`?

[gallais]

At the moment we have:

_≤_ : Rel A _
x ≤ y = (x < y) ⊎ (x ≈ y)

and

data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  refl : Reflexive (ReflClosure _∼_)
  [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y

Should we merge the two definitions by introducing a separate inductive type for _≤_ and implementing ReflClosure in terms of it?

This would make ReflClosure more lazy by changing the type of refl from Reflexive _ to x ≡ y → ReflClosure _∼_ x y.

[MatthewDaggitt]

Hmm intuitively it seems to me that StrictToNonStrict should be a specialised instance of ReflClosure, but my intuition is wrong it's not because the former has arbitrary equalities whereas the latter only considers propositional equality.

The problem with making _≤_ a separate inductive type is that we'd have to name its constructors inj₁ and inj₂ for backwards compatibility, which might in turn lead to clashes in other files where Data.Sum is used alongside it? Would defining inj₁ and inj₂ as patterns improve things? We can't mark patterns as deprecated correct?

I have no objection to making ReflClosure more lazy, in my experience that is almost always the right way to go.

[JacquesCarette]

Can you explain what order you have in mind that makes ReflClosure a special case of _≤_? Right now, I'm not seeing it. Maybe that propositional is always contained in any other equivalence relation?

[MatthewDaggitt]

Sorry for the long reply @JacquesCarette. To make ReflClosure more general it should really be defined as follows:

data ReflClosure {A : Set a} (_≈_ : Rel A ℓ) (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  refl : ∀ {x y} (x≈y : x ≈ y) → ReflClosure _≈_ _∼_ x y
  [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _≈_ _∼_ x y

so that you can specify the equality relation that you are reflexive in respect to. The current definition of _≤_ would then be isomorphic to ReflClosure _≈_ _∼_ and the current definition of ReflClosure _∼_ would become ReflClosure _≡_ _∼_

I'm in favour of making this change in v2.0.

[JacquesCarette]

This still seems different to me. With ReflClosure, you build up an explicit path that relates things, but that seems to rule out other kinds of evidence? Unless _~_ does not have to be symmetric? [I tend to not use a symmetric symbol for non-symmetric relations]. The names seem to indicate some kinds of properties of the relation are assumed (such as _≈_ actually being reflexive!). Perhaps that's what confusing me?

[MatthewDaggitt]

With ReflClosure, you build up an explicit path that relates things, but that seems to rule out other kinds of evidence?

I'm afraid I don't quite understand what you mean here?

Unless ~ does not have to be symmetric? [I tend to not use a symmetric symbol for non-symmetric relations]. The names seem to indicate some kinds of properties of the relation are assumed (such as ≈ actually being reflexive!). Perhaps that's what confusing me?

No, _~_ does not have to be symmetric, and this assumption would not be needed to prove most properties about ReflClosure. _≈_ does not have to be reflexive, but it would need to be assumed to be reflexive to prove most properties about ReflClosure.

[MatthewDaggitt]

As @Taneb points out this is really just an instance of Relation.Binary.Construct.Union as well.

[MatthewDaggitt]

The conclusion is to change to use Union instead of defining own datatype + rename constructors via pattern synonyms. @jamesmckinna suggests refl and incl?

[wenkokke]

Having done part of this rewrite, I'd say we should either not use Union to implement ReflClosure or block that rewrite on typed pattern synonyms.

The synonym for refl clashes with _≡_.refl, and type inference becomes more difficult, e.g., I had to make the following change in Data.Char.Properties amongst others:

  ≤-reflexive : _≡_ ⇒ _≤_
- ≤-reflexive = Refl.reflexive
+ ≤-reflexive = Refl.reflexive {R = _<_}

@jamesmckinna The [_] actually has an analogue in the singleton list syntax, which is pushes through TransClosure as well:

data ReflClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  refl : Reflexive (ReflClosure _∼_)
  [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _∼_ x y

data TransClosure {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  [_] : ∀ {x y} (x∼y : x ∼ y) → TransClosure _∼_ x y
  _∷_ : ∀ {x y z} (x∼y : x ∼ y) (y∼⁺z : TransClosure _∼_ y z) → TransClosure _∼_ x z

Unfortunately, it is immediately abandoned in ReflTransClosure, better known as Star:

data Star {i t} {I : Set i} (T : Rel I t) : Rel I (i ⊔ t) where
  ε   : Reflexive (Star T)
  _◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k

And the analogue breaks down in SymClosure and EqClosure.

There are also an alternative definition for TransClosure called Plus:

data Plus {A : Set a} (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  [_]     : ∀ {x y} (x∼y : x ∼ y) → x [ _∼_ ]⁺ y
  _∼⁺⟨_⟩_ : ∀ x {y z} (x∼⁺y : x [ _∼_ ]⁺ y) (y∼⁺z : y [ _∼_ ]⁺ z) →
            x [ _∼_ ]⁺ z

And an extra definition called Plus⇔ which doesn't have a corresponding SymTransClosure:

data Plus⇔ : Rel A (a ⊔ ℓ) where
  forth  : ∀ {x y} → x ≤ y → Plus⇔ x y
  back   : ∀ {x y} → y ≤ x → Plus⇔ x y
  forth⁺ : ∀ {x y z} → x ≤ y → Plus⇔ y z → Plus⇔ x z
  back⁺  : ∀ {x y z} → y ≤ x → Plus⇔ y z → Plus⇔ x z

So I think redefining ReflClosure using unions without taking all these others into account is a bit short sighted.

[wenkokke]

None of these seem generic in the equality relation, so I do think @MatthewDaggitt's suggestion to generalise ReflClosure and TransClosure makes a lot of sense. However, at that point they do become literal aliases of Union, so I'd prefer blocking any such rewrite on typed pattern synonyms.

[jamesmckinna]

Sorry for the long reply @JacquesCarette. To make ReflClosure more general it should really be defined as follows:

data ReflClosure {A : Set a} (_≈_ : Rel A ℓ) (_∼_ : Rel A ℓ) : Rel A (a ⊔ ℓ) where
  refl : ∀ {x y} (x≈y : x ≈ y) → ReflClosure _≈_ _∼_ x y
  [_]  : ∀ {x y} (x∼y : x ∼ y) → ReflClosure _≈_ _∼_ x y

so that you can specify the equality relation that you are reflexive in respect to. The current definition of _≤_ would then be isomorphic to ReflClosure _≈_ _∼_ and the current definition of ReflClosure _∼_ would become ReflClosure _≡_ _∼_

I'm in favour of making this change in v2.0.

As an alternative, why not redefine in the opposite direction, by defining ReflClosure _∼_ to be StrictToNonStruct _≡_ _∼_? Notwithstanding @wenkokke 's defence of the use (and abuse) of [_] across the Closure.* constructions...

Part of my reasoning comes precisely from looking at @JacquesCarette 's #1489 where the properties of _≤_ seem to be an uneasy negotiation of properties generic to ReflClosure and ad hoc ones cut-to-fit the _≡_ case...

And FWIW, I'm not wedded to whether ReflClosure is defined inductively or not (by contrast with the other, actually inductive, closure operators). And the knock-on effects of having to add an additional implicit parameter seem... just the cost of achieving a simplification...

... but I suppose the discussion of unifying the Permutation definitions cf. #1354 / #1761 also bears on this... the refl/reflexive distinction is not always as innocent as we might like.

UPDATED: D'oh: @gallais 's original suggestion! Minus the separate inductive definition...

[MatthewDaggitt]

We should almost have a new label entirely for being "blocked on typed pattern synonyms" :sweat_smile: