Sergei Meshveliani
2017-09-15 13:27:37 UTC
People,
I have a question on the algebraic hierarchy architecture in Standard
library.
This concerns the problem of a common super-structure (super-class).
Consider the example:
having f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l,
implement
g : (H H' : Semigroup) → H and H' are on the same setoid → Semigroup
g H H' = f H H'
Consider the program
----------------------------------------------------------------------
postulate f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l
g : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l -- wrong
g H H' = f H H'
----------------------------------------------------------------------
This will not do, because the domain of g is not as required.
Below g' pretends to implement the goal:
-------------------------------------------------------------
module CommonSuper where
open import Relation.Binary using (Setoid)
open import Algebra using (Semigroup)
open import Algebra.Structures using (IsSemigroup)
open import Algebra.FunctionProperties using (Op₂)
postulate f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l
g' : ∀ {c l} → (S : Setoid c l) →
let open Setoid S using (_≈_; Carrier)
in
(_∙_ _∙'_ : Op₂ Carrier) →
IsSemigroup _≈_ _∙_ → IsSemigroup _≈_ _∙'_ → Semigroup c l
g' S _∙_ _∙'_ isSemig isSemig' = f H H'
where
open Setoid S using (_≈_; Carrier)
H = record{ Carrier = Carrier
; _≈_ = _≈_
; _∙_ = _∙_
; isSemigroup = isSemig
}
H' = record{ Carrier = Carrier
; _≈_ = _≈_
; _∙_ = _∙'_
; isSemigroup = isSemig'
}
--------------------------------------------------------------
But here g' is applied not to a pair of semigroups but to their rather
decomposed forms.
Further, g'' looks as something more close to the goal:
g'' : ∀ {c l} → (H H' : Semigroup c l) →
let S = Semigroup.setoid H
S' = Semigroup.setoid H'
in
(CoinverseSetoidIso S S') → Semigroup c l
g'' H H' _ = f H H'
Here isoPair : CoinverseSetoidIso S S'
is a pair of mutually inverse setoid isomorphisms between S and S'.
For the condition of "over the same setoid" it suggests to include a
setoid isomorphism into the signature.
Still a complication. We have two different types for setoid instead of
one.
The release 0.04.1 of the DoCon-A library applies the approach in which
the Semigroup record will have (S : Setoid) as an _argument_.
And a similar construct with super-structures as arguments is repeated
for Group, Ring, and so on.
With this approach, the examples like the above g are programmed
easier.
But this still leads to a certain complication. Because this forces
introduction of certain up-structures: Semigroup - UpSemigroup,
Group - UpGroup, and so on (see Manual on DoCon-A-0.04.1).
In DoCon-A-2.00, I return to the approach similar to Standard library,
with adding the Is-structures (IsSemigroup, IsGroup, and such).
Anyway, a spot of inadequacy is visible.
Can anybody comment on this philosophy?
Regards,
------
Sergei
I have a question on the algebraic hierarchy architecture in Standard
library.
This concerns the problem of a common super-structure (super-class).
Consider the example:
having f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l,
implement
g : (H H' : Semigroup) → H and H' are on the same setoid → Semigroup
g H H' = f H H'
Consider the program
----------------------------------------------------------------------
postulate f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l
g : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l -- wrong
g H H' = f H H'
----------------------------------------------------------------------
This will not do, because the domain of g is not as required.
Below g' pretends to implement the goal:
-------------------------------------------------------------
module CommonSuper where
open import Relation.Binary using (Setoid)
open import Algebra using (Semigroup)
open import Algebra.Structures using (IsSemigroup)
open import Algebra.FunctionProperties using (Op₂)
postulate f : ∀ {c l} → Semigroup c l → Semigroup c l → Semigroup c l
g' : ∀ {c l} → (S : Setoid c l) →
let open Setoid S using (_≈_; Carrier)
in
(_∙_ _∙'_ : Op₂ Carrier) →
IsSemigroup _≈_ _∙_ → IsSemigroup _≈_ _∙'_ → Semigroup c l
g' S _∙_ _∙'_ isSemig isSemig' = f H H'
where
open Setoid S using (_≈_; Carrier)
H = record{ Carrier = Carrier
; _≈_ = _≈_
; _∙_ = _∙_
; isSemigroup = isSemig
}
H' = record{ Carrier = Carrier
; _≈_ = _≈_
; _∙_ = _∙'_
; isSemigroup = isSemig'
}
--------------------------------------------------------------
But here g' is applied not to a pair of semigroups but to their rather
decomposed forms.
Further, g'' looks as something more close to the goal:
g'' : ∀ {c l} → (H H' : Semigroup c l) →
let S = Semigroup.setoid H
S' = Semigroup.setoid H'
in
(CoinverseSetoidIso S S') → Semigroup c l
g'' H H' _ = f H H'
Here isoPair : CoinverseSetoidIso S S'
is a pair of mutually inverse setoid isomorphisms between S and S'.
For the condition of "over the same setoid" it suggests to include a
setoid isomorphism into the signature.
Still a complication. We have two different types for setoid instead of
one.
The release 0.04.1 of the DoCon-A library applies the approach in which
the Semigroup record will have (S : Setoid) as an _argument_.
And a similar construct with super-structures as arguments is repeated
for Group, Ring, and so on.
With this approach, the examples like the above g are programmed
easier.
But this still leads to a certain complication. Because this forces
introduction of certain up-structures: Semigroup - UpSemigroup,
Group - UpGroup, and so on (see Manual on DoCon-A-0.04.1).
In DoCon-A-2.00, I return to the approach similar to Standard library,
with adding the Is-structures (IsSemigroup, IsGroup, and such).
Anyway, a spot of inadequacy is visible.
Can anybody comment on this philosophy?
Regards,
------
Sergei