[Agda] common super-structure

[Guillaume Allais]

Hi Sergei,

I don't really have an informed opinion on the two different approaches
but something I noticed while I was preparing the PR for the stdlib's
structure homomorphisms is that Agda will accept a record definition
with missing fields as long as they can be resolved by unification.

This means in particular that the where-clause of your g' can be reduced
to (this pattern should maybe be given a toplevel definition called
"mkSemigroup"):

==========================================================
  H  = record{ isSemigroup = isSemig
             }
  H' = record{ isSemigroup = isSemig'
             }
==========================================================

Given that this gets rid of a lot of the repetitions (at least in the
term fragment, if not the type one) it may make the stdlib's approach
more tractable for you.

Best,
--
gallais


On 15/09/17 15:27, Sergei Meshveliani wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170918/341885bc/attachment.sig>