[Agda] no-eta-equality

[Jesper Cockx]

You can write eDSet and eUpDSet using copatterns as follows:

eDSet : DSet eDecSetoid
dSet1 eDSet = f
    where
        f : eC → eC
        f = id
 dSet2 eDSet = g
    where
        g : eC → ℕ
        g _ = 0

eUpDSet : UpDSet _ _
decSetoid eUpDSet = eDecSetoid
dSet eUpDSet = eDSet

Jesper

On Thu, Sep 29, 2016 at 1:54 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Wed, 2016-09-28 at 15:07 +0200, Andrea Vezzosi wrote:
> > Using rd' doesn't make things any better than using the constructor.
> >
> > Your suc'Rd is already somewhat improved by no-eta because the match
> > on (rd a n) will be strict now.
> >
> > However you should also consider the following version, so that
> > (suc'Rd (rd a n)) does not reduce by itself, but only when projections
> > are applied to it.
> >
> > suc'Rd :  {A : Set} → Rd A → Rd A
> > fl1 (suc'Rd (rd a n)) =  a
> > fl2 (suc'Rd (rd a n)) = n
> >
>
> Sorry, I am somewhat confused.
> Consider the example below in which the record  UpDSet   uses
> no-eta-equality,  and  eUpDSet  builds a certain instance of UpDSet.
>
> What do I need to change there concretely in order to make  eUpDSet  to
> use copatterns?
>
> My library for algebra is a small and a toy library from the point of
> view of CA practice. But it cannot type-check within  6 G byte  of
> memory (with Agda of September 16, 2016).
>
> So far I need only to understand: what is the main source of the
> expense, to find out the `bottleneck' in the current Agda with respect
> to my program.
> The first suspect is the record tower for algebraic structures:
>     DSet -- UpDSet -- Magma -- UpMagma -- Semigroup -- UpSemigroup,
>     CommutativeSemigroup -- UpCommutativeSemigroup, ...,
>     and so on, up to EuclideanRing and Field
>     (about 26 levels),
>     with higher levels having fields and also arguments of lower levels.
>
> The first experiment is only to implement the instance construction of
> Up-domains above via copatterns and `no-eta-equality', and to see the
> memory expense in type checking.
> (This does not mean that I am going to complicate the final program,
> this is only for finding the inefficiency source).
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
>
> ************************************************************
> ***************
> {-# OPTIONS --copatterns #-}
> module M where
> open import Level    using (Level; _⊔_; suc)
> open import Function using (id)
> open import Algebra.FunctionProperties as FuncProp using (Op₂)
> open import Relation.Binary   using (Rel; DecSetoid; _Preserves₂_⟶_⟶_)
> open import Data.Maybe as Mb  using (Maybe; just; nothing)
> open import Data.Nat   as Nat using (ℕ)
>
> --------------------------------------------------------------
> setoidLevel : Level → Level → Level
> setoidLevel l l' =  suc (l ⊔ l')
>
> record DSet {c l} (decS : DecSetoid c l) : Set (c ⊔ l)
>   where
>   constructor dSet′
>
>   open DecSetoid decS using (Carrier)
>
>   field  dSet1 : Carrier → Carrier        -- contrived
>          dset2 : Carrier → ℕ
>
>
> record UpDSet c l : Set (setoidLevel c l)
>        where
>        no-eta-equality         -- (1)
>        constructor upDSet′
>
>        field  decSetoid : DecSetoid c l
>               dSet      : DSet decSetoid
>
>        open DSet dSet public
>
> ---------------------------------------------------------------
> module OfMaybe-DSet (c l : Level) (upDS : UpDSet c l)
>   where
>   decSetoid = UpDSet.decSetoid upDS
>   dSet      = UpDSet.dSet upDS
>
>   eDecSetoid : DecSetoid _ _
>   eDecSetoid = Mb.decSetoid decSetoid
>
>   open DecSetoid eDecSetoid using () renaming (Carrier to eC)
>
>   eDSet : DSet eDecSetoid
>   eDSet = dSet′ f g       -- contrived
>           where
>           f : eC → eC
>           f = id
>
>           g : eC → ℕ
>           g _ = 0
>
>   eUpDSet : UpDSet _ _
>   eUpDSet = upDSet′ eDecSetoid eDSet    -- (2)
> ************************************************************
> *****************
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160929/0edc9503/attachment.html