[Agda] test report

[mechvel at scico.botik.ru]

On 2021-03-16 23:49, Nils Anders Danielsson wrote:
> On 2021-03-15 14:34, mechvel at scico.botik.ru wrote:
>> How to force erasing by @erase as much as possible for this example?
>> Where to set @0 ?
> 
> Here is one way to erase the proofs:
> 
>   record Erased (@0 A : Set) : Set where
>     constructor [_]
>     field
>       @0 erased : A
> []

> If, instead of using Erased, you switch to a variant of Σ with an 
> erased
> second field, then the GHC backend might erase more of your code:
> 
>   record Σ (A : Set) (@0 B : A → Set) : Set where
> 


First I try Erased.
I set
   record Erased {α} (@0 A : Set α) : Set α where
     constructor [_]
     field
       @0 erased : A

   @0 from[] : ∀ {α}{A : Set α} → Erased A → A
   from[] [ x ] =  x

into my Prelude.agda.
I decided that  from[]  is useful because there are places like

   where
   ...
   u'*ₖv-withEq = foo          -- that returns a pair with erased second 
part
   u'*ₖv = proj₁ u'*ₖv-withEq

   u'vEq =  proj₂ u'*ₖv-withEq

This is not type-checked. So I changed the latter line to

   @0 u'vEq : u'*ₖv =ₚ u' *ₚ v
   u'vEq =  from[] (proj₂ u'*ₖv-withEq)

And  u'vEq  is used further as an erased thing.

`Erased' is inserted into several function signatures in Foo.agda, its 
program is complex.


The result is that  Foo.hs  has become ~11 times smaller:
from 18.181.844 byte to 1.736.180.
And Foo.o has become ~1.5 times smaller (from 5.708.416 to 3.273.360).

The run-time performance remains (it was satisfactory)
- must it remain?

I have to test how it will change the time & space expense on type 
checking and compilation.


Thanks,

------
Sergei



>   efficient+withProof : (m n : ℕ) → Σ ℕ (\s → Erased (s ≡ m + n))
> 
>   efficient+withProof 0       n =  (n , [ refl ])
>   efficient+withProof (suc m) n =
>     let
>       (eff-m-n , [ eff-m-n≡m+n ]) = efficient+withProof m n
>       s = suc eff-m-n
> 
>       @0 s≡1+m+n : s ≡ (suc m) + n
>       s≡1+m+n = cong suc eff-m-n≡m+n
>     in
>     (s , [ s≡1+m+n ])
> 
>   efficient+ : (m n : ℕ) → ℕ
>   efficient+ m =  proj₁ ∘ efficient+withProof m
> 
>   @0 efficient+comm : Commutative _≡_ efficient+
>   efficient+comm m n =
>     let
>       open EqReasoning (PE.setoid ℕ)
>       (eff[m,n] , [ eff[m,n]≡m+n ]) = efficient+withProof m n
>       (eff[n,m] , [ eff[n,m]≡n+m ]) = efficient+withProof n m
>     in
>     begin efficient+ m n  ≡⟨ eff[m,n]≡m+n ⟩
>           m + n           ≡⟨ +-comm m n ⟩
>           n + m           ≡⟨ sym eff[n,m]≡n+m ⟩
>           efficient+ n m
>     ∎
> 
> If, instead of using Erased, you switch to a variant of Σ with an 
> erased
> second field, then the GHC backend might erase more of your code:
> 
>   record Σ (A : Set) (@0 B : A → Set) : Set where
>     constructor _,_
>     field
>       proj₁    : A
>       @0 proj₂ : B proj₁
> 
> With Erased I get the following Haskell code for efficient+withProof:
> 
>   d20 :: Integer -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T14
>   d20 v0 v1
>     = case coe v0 of
>         0 -> coe MAlonzo.Code.Agda.Builtin.Sigma.C32 (coe v1) erased
>         _ -> let v2 = subInt (coe v0) (coe (1 :: Integer)) in
>              coe
>                MAlonzo.Code.Agda.Builtin.Sigma.C32
>                (coe
>                   addInt (coe (1 :: Integer))
>                   (coe
>                      MAlonzo.Code.Agda.Builtin.Sigma.d28 (coe d20 (coe
> v2) (coe v1))))
>                erased
> 
> With an erased second projection I get the following Haskell code
> instead:
> 
>   newtype T6 = C20 AgdaAny
> 
>   d16 :: T6 -> AgdaAny
>   d16 v0
>     = case coe v0 of
>         C20 v1 -> coe v1
>         _ -> MAlonzo.RTE.mazUnreachableError
> 
>   d28 :: Integer -> Integer -> T6
>   d28 v0 v1
>     = case coe v0 of
>         0 -> coe C20 v1
>         _ -> let v2 = subInt (coe v0) (coe (1 :: Integer)) in
>              coe
>                C20
>                (addInt (coe (1 :: Integer)) (coe d16 (coe d28 (coe v2)
> (coe v1))))