[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:
> [..]


Nils, thank you very much.
I am going to try this approach.

------
Sergei



>   record Erased (@0 A : Set) : Set where
>     constructor [_]
>     field
>       @0 erased : A
> 
>   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))))