Start implementing a Number moduleHEADmaster

The nascent Number module also serves as a proof of concept for dealing
with records in the Agda standard library that are parameterized by
levels instead of sets, like those in the Algebra hierarchy.  These
records are difficult to use as type classes, because Agda’s normal
mechanism for generating type classes ('open SomeRecord ⦃...⦄') will
make the levels the instance arguments, rather than the actual set the
record’s functions operate on.

To work around this, I defined wrapper records (effectively just named
dependent pairs) parameterized in the way I desire.  Each contains an
underlying algebraic structure and a proof of type equality (usually
just 'refl') between the parameter and the structure’s carrier.  Then, I
define functions over my wrapper record to rewrite with the type
equality and use the underlying structure’s code.

This work is related to standard library bug #35
<https://github.com/agda/agda-stdlib/issues/35>;; fixing this bug would
obviate the need for my workaround.

1 files changed, 60 insertions, 0 deletions

diff --git a/Prelude/Number.agda b/Prelude/Number.agda
new file mode 100644
index 0000000..02024d0
--- /dev/null
+++ b/Prelude/Number.agda
@@ -0,0 +1,60 @@
+{- Copyright © 2015 Benjamin Barenblat
+
+Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
+this file except in compliance with the License.  You may obtain a copy of the
+License at
+
+    http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software distributed
+under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
+CONDITIONS OF ANY KIND, either express or implied.  See the License for the
+specific language governing permissions and limitations under the License. -}
+
+module B.Prelude.Number where
+
+import Algebra
+import Data.Integer
+import Data.Integer.Properties
+import Data.Nat
+import Data.Nat.Properties
+open import Level using (_⊔_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open Data.Integer using (ℤ) public
+open Data.Nat using (ℕ) public
+
+record NearSemiring {c} {ℓ} (A : Set c) : Set (Level.suc (c ⊔ ℓ)) where
+  field
+    structure : Algebra.NearSemiring c ℓ
+    typeEquality : A ≡ Algebra.NearSemiring.Carrier structure
+
+NearSemiringInstance : ∀ {c ℓ}
+                     → (structure : Algebra.NearSemiring c ℓ)
+                     → NearSemiring (Algebra.NearSemiring.Carrier structure)
+NearSemiringInstance structure =
+  record { structure = structure; typeEquality = refl }
+
+private
+  change₂ : ∀ {c ℓ A′}
+          → ⦃ witness : NearSemiring {c} {ℓ} A′ ⦄
+          → ((r : Algebra.NearSemiring c ℓ)
+             → let A = Algebra.NearSemiring.Carrier r in
+               A → A → A)
+          → A′ → A′ → A′
+  change₂ ⦃ witness ⦄ f rewrite NearSemiring.typeEquality witness =
+    f (NearSemiring.structure witness)
+
+_*_ : ∀ {c ℓ A} → ⦃ _ : NearSemiring {c} {ℓ} A ⦄ → A → A → A
+_*_ = change₂ Algebra.NearSemiring._*_
+
+instance
+  NearSemiring-ℕ : NearSemiring ℕ
+  NearSemiring-ℕ =
+    NearSemiringInstance (Algebra.CommutativeSemiring.nearSemiring
+                            Data.Nat.Properties.commutativeSemiring)
+
+  NearSemiring-ℤ : NearSemiring ℤ
+  NearSemiring-ℤ =
+    NearSemiringInstance (Algebra.CommutativeRing.nearSemiring
+                            Data.Integer.Properties.commutativeRing)