[Agda] proof overhead
Nils Anders Danielsson
nad at chalmers.se
Mon Jan 28 15:19:09 CET 2013
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
> 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
This is implemented in the Epic backend, and only applies to compiled
code (not code run by the type-checker).
More information about the Agda