[Agda] proof overhead

[Serge D. Mechveliani]

On Sat, Dec 22, 2012 at 11:21:30AM +0100, 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.


Great! Thank you.
I have forgotten of this possibility. 
I'll try it, and if it works, it would be better than programming two 
functions.

------
Sergei

п©
> On Sat, Dec 22, 2012 at 10:57 AM, Serge D. Mechveliani <mechvel at botik.ru> 
> wrote:
> > People,
> > I have certain beginner questions on the practice of the verified
> > programming with dependent types.
> > [..]
> >
> > Consider the Agda function  orderList  for sorting  xs : List Nat
> > non-decreasingly by `<'.  And let it return a record
> >
> > record OrderList (xs : List Nat) : Set where
> >                        field
> >                          resList       : List Nat;
> >                          ordProof      : IsOrdred resList;
> >                          multisetProof : multiset xs == multiset resList
> >
> > (for this letter I replace  \equiv  with  `=='),
> >
> > with  resList  standing for the resulting list,
> > IsOrdered  and  multilset  reasonably defined
> >
> > I have programmed merge sorting, which evaluation cost is  O(n*(log n))
> > -- together with  resList  and  ordProof.
> > I can easily add the value for  multisetProof
> > -- but with making the evaluation cost  O(n^2).
> > [..]