[Agda] proof overhead

[Nils Anders Danielsson]

On 2012-12-22 11:21, Gabriel Scherer wrote:
> What about simply delaying the computation of the proofs by using
>
>      record OrderList (xs : List Nat) : Set where
>        field
>          resList       : List Nat;
>          ordProof      : IsOrdred resList;
>          multisetProof : Unit -> multiset xs == multiset resList
>
> The two types (evidence and delayed evidence) are isomorphic, you
> should be able to do everything you want in such a setting, and the
> dynamic semantics under a weak reduction strategy should make
> multisetProof O(1), as long as you never need to compute on the proof.
>
> There are more advanced strategies based on irrelevant types, squashed
> types, or otherwise erasable values, but this is a simple first step
> and I suppose it would work.

 From the release notes for Agda 2.3.0:

   "An important example of an inferable type is the usual propositional
   equality type (_≡_). Any function returning a propositional equality
   can simply return the reflexivity constructor directly without
   computing anything."

This is implemented in the Epic backend, and only applies to compiled
code (not code run by the type-checker).

-- 
/NAD