[ refactor ] a 'better' `Data.Integer.Base`?

[jamesmckinna]

I was experimenting with Integers, leading to agda/agda#8208 (so I don't see this going anywhere anytime soon, but the coupling between 'primitive's and Builtins looks as though it might benefit from a closer look?), towards defining instead:

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Integer.Base where

open import Data.Nat.Base as ℕ using (ℕ) hiding (module ℕ)

------------------------------------------------------------------------
-- Integers: add `NonZero` as a premise to the `negsuc` constructor

data ℤ : Set where
  pos : ∀ (n : ℕ) → ℤ
  neg : ∀ (n : ℕ) → ℕ.NonZero n → ℤ

pattern negsuc n = neg (ℕ.suc n) _

{-# BUILTIN INTEGER       ℤ    #-}
{-# BUILTIN INTEGERPOS    pos    #-}

and then most/all of the gymnastics associated with -[1+ n ] etc. ought to go away, which I think would be better for (user and developer intelligibility), esp. eg. #2878 because the Signed representation then becomes ... almost automatic.

NB. Again, for 'reasons', we can't define

data ℤ : Set where
  pos : ∀ (n : ℕ) → ℤ
  neg : ∀ (n : ℕ) → {{ℕ.NonZero n}} → ℤ

but in view of #2644 maybe making the proof explicit (but being able to finesse it via the negsuc pattern synonym where needed) isn't such a bad thing...

[JacquesCarette]

All my instincts scream no !!!ℤ should not involve a proof! Why would you want to build a 'redundant' representation that needs a proof to then eliminate that case !?!? [If this were cubical Agda, that would be different, there are likely sane HIT representations of ℤ.]

(I also object to saying that zero is positive.)

More seriously, to me the toughest question is: what should be the API to ℤ? What I mean is (regardless of Agda's actual capabilities to do this ergonomically) what should be the functions (and properties) that should be defined on the structure of ℤ that can serve as the basis for everything else by making the representation 'opaque' thereafter? [There are way too many proofs in stdlib that resort to raw induction when lemmas would be much nicer.]

[jamesmckinna]

Re:

More seriously, to me the toughest question is: what should be the API to ℤ? What I mean is (regardless of Agda's actual capabilities to do this ergonomically) what should be the functions (and properties) that should be defined on the structure of ℤ that can serve as the basis for everything else by making the representation 'opaque' thereafter? [There are way too many proofs in stdlib that resort to raw induction when lemmas would be much nicer.]

Absolutely. For whatever reasons (pattern-matching is 'too easy' to appeal to interactively?), we don't make clear separations between API and implementation as a systematic design practice in stdlib. And we should! (I think that Data.Nat.DivMod is one of the few modules which really posits a record to capture the signature of division-with-remainder, and we then make almost no no-trivial use of it...)

[jamesmckinna]

All my instincts scream no ℤ should not involve a proof! Why would you want to build a 'redundant' representation that needs a proof to then eliminate that case !?!? [If this were cubical Agda, that would be different, there are likely sane HIT representations of ℤ.]

(I also object to saying that zero is positive.)

So are you saying that you would rather impose a three-way split with

data ℤ : Set where
  pos : ∀ (n : ℕ) → ℕ.NonZero n → ℤ
  zero : ℤ
  neg : ∀ (n : ℕ) → ℕ.NonZero n → ℤ

and fix up the pragmatics with pattern synonyms?

(UPDATED: in the interests of full disclosure, I'd prefer 2^n cases over 3^n when defining an n-ary function or relation, even though in practice, it often seems to end up nearer the latter than the former...)

[JacquesCarette]

If I were to use that representation at all, I would not have ℕ.NonZero n in either pos or neg. pos represents a positive, who cares about the internal representation of its payload?

I also prefer fewer cases, whenever the cost is reasonable.

[jamesmckinna]

If I were to use that representation at all, I would not have ℕ.NonZero n in either pos or neg. pos represents a positive, who cares about the internal representation of its payload?

So... I think that means your earlier

All my instincts scream no ℤ should not involve a proof! 

perhaps has a superfluous/contradictory 'not'.

My view is that we shouldn't 'fiddle' the constructors to be off-by-one; yours, in fact, seems to be that we can (as now: so no change to the status quo) and should, possibly also with +0 as as a special case.

The purpose of this issue is to try to problematise the 'off-by-one' negsuc constructor currently used/defined in Agda.Builtin.Int, in favour of having a constructor which observes: if you want an off-by-one representation, use NonZero constraints to enforce that?

[Taneb]

I had a quick attempt at making a version of Integer which had NonZero (EDIT: as in irrelevant instance argument) in the constructors. The (first) big issue I ran into is that you end up with is that you can no longer do cong pos (or whatever you call your constructors) in the proofs

[jamesmckinna]

I had a quick attempt at making a version of Integer which had NonZero (EDIT: as in irrelevant instance argument) in the constructors. The (first) big issue I ran into is that you end up with is that you can no longer do cong pos (or whatever you call your constructors) in the proofs

Oh dear!

• I hadn't been able to use an irrelevant instance (Agda rejected it, but maybe I should try harder?!), but did succeed with just marking NonZero as irrelevant .(NonZero n) instead;
• ... but cong etc. yes that's a real annoyance. (cf. Fragile NonZero and implementation-dependent luck #2644 ; care required)

Maybe I should shelve this for a hypothetical-rewrite... but I do find the endless marshalling/unmarshalling of suc n/n in definitions and proofs very hard to get straight in my mind when reading. It's arguable whether my suggested neg/negsuc factorisation is actually an improvement (it's marginal in Base, but still an improvement in readability IMHO; but Properties required more effort than I could muster... but maybe that suggests @JacquesCarette 's comment about using (more) lemmas should bite harder...)

[Taneb]

An idea I'd like to explore more is defining an alternate type of integers (lie Data.Rational.Unnormalised), by pairs of natural numbers with the equivalence (m₁ , n₁) ≈ (m₂ , n₂) = m₁ ℕ.+ n₂ ≡ m₂ ℕ.+ n₁.

This approach is described on Wikipedia in this section.

It has the advantage in that all of the algebraic proofs are suddenly algebraic proofs on natural numbers, which we are well equipped to do.

We can translate back to our current definition with _⊖_, and the price for translating all of the proofs is one hairy proof about _⊖_

[jamesmckinna]

Yes @Taneb that is the 'INT' construction... (applies to a Monoid and yields a Group; hence also a Semiring yields a Ring etc.; commutativity also inherited in each case)

[JacquesCarette]

All my instincts scream no ℤ should not involve a proof!

perhaps has a superfluous/contradictory 'not'.

Edited to have !!! after the no. Those should have been 2 separate sentences all along.

And if I was a betting person, I would bet on the INT construction being the best compromise representation. But one has to double-down on doing quotients via setoids to have it work (in raw MLTT; it's still a good representation in cubical, but as a HIT instead.)

[jamesmckinna]

Thanks for the disambiguation!

As for raw setoids for quotients, well that's the path we're on for #2854 etc., so maybe this is the crunch moment where we discover how fit-for-purpose the current architecture in fact is in practice...

As for a 'purely inductive' approach to integers as now, it's not the principle I object to, but the pragmatics, and having the additional pattern-matching overhead that troubles me. I had been under the, possibly mistaken, impression, that a detour via NonZero might permit 'lazier' patterns, and clearer semantics (and fewer off-by-one problems: of course the system enforces 'correct' definitions, but its harder for the user to work out what those are/should be!)

[Taneb]

I personally think it's important to have the "primary" representation not-setoidy, if possible, which it clearly is for integers. I also think it would be odd to compile an integer to two integers (because that's how GHC implements its Natural type). This is why I suggested having a translation to the INT construction (aside: I've not seen that name elsewhere, is there a good citation for it? And I don't think it works for any monoid, only commutative, cancellative ones) that we can use to make proofs easier, similar for what we do for Data.Rational

[jamesmckinna]

Re: INT
Apparently this was first named in the context of traced monoidal categories (1996, so not that old, but monoidal categories form the late-1960s(Benabou)/early-1970s (Kelly et al.) got new life after linear logic woke up them up in the CS context in the 1990s), but our very own @JacquesCarette asks on MathOverflow:
https://mathoverflow.net/questions/106070/int-construction-traced-monoidal-categories-and-grothendieck-group

See also: https://mathoverflow.net/questions/284152/the-chu-construction-and-the-int-construction

I've always thought of it as 'INT' (as a content-free name; the traced stuff I failed to catch at the time; traces seem to provide an alternative to/generalisation of the cancellation required (can commutativity be finessed by 'twisting'?)), having first seen the integers-from-naturals at high school back in the late 1970s/early 1980s (one of the many legacies of 'New Math'... ;-)).

But I guess integers-from-naturals, fields-from-integral-domains go all the way back to the reformulation of abstract algebra in the 1900-1920s (1870-1920? Dedekind 1887 surely stands out here: the naturals as the Church encoding version of Peano, in modern language) in Germany (Noether et al.; van der Waerden... ?), and then popularised by the US mathematicians who went to Germany then to learn the New Math (Birkhoff, Mac Lane, ...), followed up by the wave of refugees in the 1930s... but my history is a bit shaky on this, to be sure!