[Agda] common super-structure

[Sergei Meshveliani]

On Mon, 2017-09-18 at 13:59 +0200, Guillaume Allais wrote:
> 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.


Nice! Thank you. I see.

------
Sergei



> 
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda