Splitting Data.Char.Base

[JacquesCarette]

In #1488 , I did not notice that Data.Char defines a bunch of relations which, in other parts, are done in separate sub-modules. In particular, I suggest that

infix 4 _≈_ _≉_
_≈_ : Rel Char zero
_≈_ = _≡_ on toℕ

_≉_ : Rel Char zero
_≉_ = _≢_ on toℕ

infix 4 _≈ᵇ_
_≈ᵇ_ : (c d : Char) → Bool
c ≈ᵇ d = toℕ c ℕ.≡ᵇ toℕ d

infix 4 _<_
_<_ : Rel Char zero
_<_ = ℕ._<_ on toℕ

infix 4 _≤_
_≤_ : Rel Char zero
_≤_ = ReflClosure _<_

be moved to Data.Char.Properties.Base and re-exported by Data.Char (but not Data.Char.Base).

[MatthewDaggitt]

I did not notice that Data.Char defines a bunch of relations which, in other parts, are done in separate sub-modules

Hmm so I don't think that this is inconsistent with the current design. For datatypes such Nat, Integer, Bool, String that don't depend on other types, we define the relations in Data.X.Base. For datatypes such as List, Tree, Vec that do depend on other types and therefore require the lifting of relations from the base type to the new type we put the relations in Data.X.Relation. This is usually because you have far more freedom when defining the lifting of relations.

Do you have any concrete problems with the definitions living here? I've looked through Data.Char.Base and I don't see any serious dependency problems. The only exception is perhaps the use reflexive closure that although reasonably lightweight could probably be streamlined.

[JacquesCarette]

I could probably live with these particular relations being moved to Data.Char.Base. But I think the more principled move would be to move them to Data.Char.Relation. That one could then have slightly larger dependencies without causing much harm.

[jamesmckinna]

Does

infix 4 _≤_
_≤_ : Rel Char zero
_≤_ = ReflClosure _<_

get any use prior to defining it (and its many properties/structures/bundles...under Data.Char.Properties) instead as an instance of Relation.Binary.Construct.StrictToNonStrict?

Seemingly only System.Random, and it's clear from other imports there that Data.Char would do just as well (or some combination of Base and Properties)

UPDATED (after @JacquesCarette 's confusion below): I probably should have emphasised 'instead' (and moved it forward in the sentence) above; I was speculating about moving the definition wholesale to Properties...

[JacquesCarette]

I must be missing something "does X get any use prior to defining it" seems like a nonsensical question - how can you use something before it's been defined? So there must be some miscommunication happening somewhere.

[MatthewDaggitt]

I'd be happy to have them moved to Data.Char.Relation.... but would prefer Data.Char.Base for consistency until we decided to move all such similar relations (e.g. in Data.Rat.Base) to similar locations.

[jamesmckinna]

@JacquesCarette Sorry for my hasty typing above...

What I'd been trying to say was (something like)

• having defined the relation in Base
• does it get any other uses elsewhere by import of that module (ie as a 'bare' relation)
• before 'existing' solely for the purposes of proving its properties in Properties, which amount to no more than the generic consequences, given the corresponding properties of _<_, of it being either a ReflClosure (or a StrictToNonStrict construction, but cf. Refactoring StrictToNonStrict and Closure.Reflexive? #1344 here!?). That is to say, could its definition, and properties, be moved wholesale to Properties, if that would streamline the dependencies in Base?

The answer to the 'does it get used elsewhere?' seems to be: yes, but not in such a way that moving its definition to Properties would be a problem, because such uses (only in System.Random, AFAICT, added only very recently in #2368 ) are already in a setting where other Properties modules are being imported, moreover in a leaf in the hierarchy.

Now, that does make it a 'special case', distinct from the others (defined as primitive, or by delegation to Nat), but it already is precisely special because of its definition as a ReflClosure...

Hope this is a bit clearer!?

UPDATED: perhaps clearer still would be a wholesale refactoring of Data.Char.Properties to include all the structures previously established for _≤_ now as generic properties via Relation.Binary.Structures, and then re-exporting them?
See eg. this blob for which the deprecations could also be massively simplified by that strategy of 'make one big structure', then reopen/rename its components to bring everything else into scope... cf. #2391

UPDATED: this mostly works, but the breaking fly in the ointment would always be that for the sake of backwards-compatibility, you'd have to maintain a deprecated version of _≤_ in Data.Char.Base terms of ReflClosure...

Conclusion: suggest we tag as v3.0?

[jamesmckinna]

I tried thinking whether there is a design meta-heuristic available to be codified here (besides 'reduce dependencies in Base modules' ;-)) such as 'Rels which are primitive/inductive belong in Base; derived notions via Relation.Binary.Construct.* belong in ...' , until I realised that the current issue seems to distinguish the use of ReflClosure from that of On, plus any artificial distinction between uses of the latter, and their Bool-valued counterparts via vanilla function composition... short of agreeing to move them all... (and/or introducing a sub-hierarchy of Bool-valued unary predicates and binary... etc. relations!?)

... cf. my war against Data.Nat.Base._≤″_ (#2262 etc.) as another instance of this issue, but one which gets negotiated in a more complex way because of the knock-on dependencies of that relation...