[ add ] product structure on `RawSetoid`

[jamesmckinna]

Lifts out the relevant constructions on RawSetoid from #2715 which is now marked blocking on this PR.

NB.

• constructions defined in named modules with explicit parametrisation, each as the relevant IsRelHomomorphism
• then defined for export in terms of the 'usual' expected names, with implicit parametrisation
• should the underlying Pointwise product of RawSetoids be lifted out (trivially) to Relation.Binary.Construct.Product? (see discussion with/comments from @JacquesCarette below...)

[jamesmckinna]

Don't really understand why the tests are failing, but seems to be a GitHub problem, rather than at my end? Ah, I'd missed the updates to the CI...

[jamesmckinna]

If anyone has any insight into why all the tests are (still!) failing on GH, please let me know!

[JacquesCarette]

The CI failure is just for ghc-9.8.4 and seems to be related to ghcup-0.0.9. Seems related to what @andreasabel did with the CI?

The exact details are:

Run "$HOME/.ghcup/bin/ghcup" install cabal 3.14.2.0 || (cat "$HOME"/.ghcup/logs/. && false) [ Info ] downloading: https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-0.0.9.yaml as file /github/home/.ghcup/cache/ghcup-0.0.9.yaml % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- 0:00:01 --:--:-- 0 0 0 0 0 0 0 0 0 --:--:-- 0:00:02 --:--:-- 0 0 22 0 0 0 0 0 0 --:--:-- 0:00:02 --:--:-- 0 curl: (22) The requested URL returned error: 429 [ Warn ] Could not get download info, trying cached version (this may not be recent!) [ ... ] If this problem persists, consider switching downloader via: [ ... ] ghcup config set downloader Wget [ Error ] [ ... ] Yaml file not found: /github/home/.ghcup/cache/ghcup-0.0.9.yaml [ ... ] Consider removing /github/home/.ghcup/cache/ghcup-0.0.9.yaml manually. Debug: Identified Platform as: Linux Ubuntu, 22.04 Info: downloading: https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-0.0.9.yaml as file /github/home/.ghcup/cache/ghcup-0.0.9.yaml Debug: Skipping and deleting etags file because destination file /github/home/.ghcup/cache/ghcup-0.0.9.yaml doesn't exist Warn: Could not get download info, trying cached version (this may not be recent!) If this problem persists, consider switching downloader via: ghcup config set downloader Wget Debug: Error was: []8;;[https://errors.haskell.org/messages/GHCup-05841\GHCup-05841]8;;] Download failed: Process "curl" with arguments ["--dump-header", "/tmp/curl-header1250-0", "-fL", "-o", "/github/home/.ghcup/cache/ghcup-0.0.9.yaml.tmp", "https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-0.0.9.yaml"] failed with exit code 22. Debug: Decoding yaml at: /github/home/.ghcup/cache/ghcup-0.0.9.yaml Error: []8;;[https://errors.haskell.org/messages/GHCup-00160\GHCup-00160]8;;]](https://errors.haskell.org/messages/GHCup-00160%1B/GHCup-00160%1B]8;;%1B/]) JSON decoding failed with: YAML exception: Yaml file not found: /github/home/.ghcup/cache/ghcup-0.0.9.yaml Consider removing /github/home/.ghcup/cache/ghcup-0.0.9.yaml manually.

[andreasabel]

curl: (22) The requested URL returned error: 429

This spells out as "too many requests". Seems like a github rate limit is hit here. GHCup downloads its metadata from github on every invocation of GHCup, so this could sometimes fail randomly because of the rate limit.

The CI failure is just for ghc-9.8.4 and seems to be related to ghcup-0.0.9. Seems related to what @andreasabel did with the CI?

Not really. This workflow is autogenerated by haskell-ci and needs to be regenerated once in a while to stay updated with the ecosystem.

It is also safe to ignore sporadic failures in this workflow since it does not test the integrity of the standard library, just the tools GenerateEverything etc.

[jamesmckinna]

Last last thought: should this be parametrised on RawSetoid, or simply on a (pair of) bare relation(s) _≈_ (as in the Function.Construct.* and existing Relation.Binary.Construct.* hierarchies)?

[JacquesCarette]

Last last thought: should this be parametrised on RawSetoid, or simply on a (pair of) bare relation(s) _≈_ (as in the Function.Construct.* and existing Relation.Binary.Construct.* hierarchies)?

Ah, the perennial (un)bundling question.

The biggest advantage of the unbundled version is that having a shared carrier of two setoids becomes easy. Having to bundle obscures things in that case and downstream uses might then struggle to recover that information.

That is, however, a pure hypothetical. However, as you mention, Relation.Binary.Construct.* seems to make the opposite decision, and being consistent with that does seem like a good idea? I would want these new functions to interact smoothly with the parts of the library that are 'related' (pun unintended) as the main design principle.

[jamesmckinna]

Will refactor to unbundle... UPDATED:

• unbundled basic definitions
• left the export versions bundled...

Easy enough to make the whole thing fully unbundled, but I had a slight wobble about whether bundling the implicit parameters as RawSetoid (usual record type disambiguation during typechecking) is better than leaving bare relations implicit and risking unsolved metas when deployed?