[Agda] test report

[Nils Anders Danielsson]

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

   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))))

-- 
/NAD