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