[Agda] Type-checker evaluator performance

Wed Feb 3 17:23:28 CET 2016

Abstracting from the details of this particular example, the problem is the
following: You want to construct a proof of some proposition P using some
sort of search procedure that may or may not deliver an actual proof. So
you define

  search : Maybe P

  proof : P
  proof = unMaybe search

where

  unMaybe : (m : Maybe A) {_ : IsJust m} -> A
  unMaybe nothing {}
  unMaybe (just x) _ = x

When type checking 'proof' the type checker has to run 'search' to see that
it is indeed 'just' something so that the implicit IsJust proof can be
filled in. The important thing to note here is that 'search' only needs to
be evaluated far enough to discover that it is a 'just' and no further.
This means that we should make getting to the 'just' constructor as cheap
as possible.

Consider what happens if you implement search in the most straightforward
way, simply running the search in the Maybe monad. In this case you need to
traverse the search space and build up the proof object (which may be very
large), at every step checking that all the substeps came back 'just'. You
don't get the final 'just' until you have created the entire proof object.

The alternative that I'm advocating is that you split the search procedure
into a test and a soundness proof for the test:

  test : Bool
  sound : T test -> P

Here the soundness proof is responsible for constructing the proof object,
assuming that the test came back 'true'. We can then implement the search
as follows:

  search : Maybe P
  search with T? test
  ... | yes p = just (sound p)
  ... | no _ = nothing

Now, in order to get to the 'just' constructor we only have to run 'test'
and we don't have to worry at all about constructing the proof object.

Concretely what I did in the me-em example was replace the 'ag' and 'af'
functions by two new functions 'ag-now' and 'af-now' implemented as
'search' above (with tests 'ag-test' and 'af-test', and soundness proofs
'ag-proof' and 'af-proof').

I hope this clarifies things.

/ Ulf

On Wed, Feb 3, 2016 at 3:34 PM, Jacques Carette <carette at mcmaster.ca> wrote:

> Where can one read more about "no-eta-equality" ?  I believe that some of
> my work could benefit from this as well.
>
> Similarly, I sought to learn from the changes you did
>
> https://github.com/UlfNorell/me-em/commit/5930ad6b155244a1ba85abc36a0e79c1333ca7f4
> but while I can "read the code", I can't quite understand how this matches
> your high-level description.  Could you comment a bit about this?  I
> believe that this would be well worth it, and may indeed help achieve a
> reduction in Agda-blame, as outlined in the first paragraph.
>
> Jacques
>
>
> On 2016-02-03 04:31 , Ulf Norell wrote:
>
> I think it's unfortunate, if perhaps not completely undeserved, that Agda
> gets blamed every time a program is slow or uses a lot of memory. When
> people are writing slow Haskell programs their first thoughts are "maybe I
> should try to optimise my program", not "maybe someone should optimise GHC"
> and I wish we could have a little more of that for Agda programs. There are
> certainly performance problems in Agda's compile time evaluator
> (call-by-name, interpretation overhead, etc) but that doesn't mean that you
> can't write programs that perform reasonably well.
>
> I had a look at your code and the main performance problem seems to be
> that you are too strict in the proof objects produced by the model checker.
> In your example the correctness proof of Peterson's algorithm consists of
> four (I think) complete state graphs (with ~14k states) decorated with
> proofs that you build up eagerly before deciding that you have a valid
> proof. If you instead separate the decision procedure from the construction
> of the proof object you only need to run the former to be sure that you
> have a proof, and can evaluate the latter lazily as you need it. I forked
> [1] your repo and tried this out. The Examples module checks in 26s and
> uses 900M memory on my machine. Another thing I tried is to use a pair type
> without eta equality for the models (in my experience eta equality and
> call-by-name is a major source of inefficiency). This saves you another 30%
> time and space.
>
> / Ulf
>
> [1] https://github.com/UlfNorell/me-em
>
>
> On Mon, Feb 1, 2016 at 9:46 AM, Liam O'Connor <liamoc at cse.unsw.edu.au>
> wrote:
>
>> Hi all,
>>
>> I’m currently using the development version of Agda, and I’ve been
>> working on using the evaluation in type checking to embed proof search
>> procedures inside Agda.
>>
>> https://github.com/liamoc/me-em
>>
>> Now, one of the applications of this technique is a model checker for a
>> fragment of CTL on the guarded command language (*).
>>
>> Here is an example, where I use the model checker to verify peterson’s
>> synchronisation algorithm.
>>
>> https://github.com/liamoc/me-em/blob/master/GCL/Examples.agda#L91
>>
>> Before I cleaned this code up and put it on GitHub, it was all in one
>> file. I can affirm that I was able to type check the code then. Today,
>> after splitting it into multiple files, and cleaning it up a little bit, I
>> found that Agda would just get OOM killed before finishing, and it would
>> take at least 10 minutes before getting OOM-killed, using all 8GB of my RAM
>> and 4GB of my swap.
>>
>> Going back to the original, single-file version, it now also fails to
>> finish checking and gets OOM-killed, so perhaps the multiple-files thing
>> isn’t causing the issue.
>>
>> (Perhaps I just used a bit of disk space and now it’s running out of
>> swap).
>>
>> Anyway, I’ll try this on a machine with more memory (RAM and swap) later,
>> but is there any plan to improve performance (both in time and space) of
>> the type-checker evaluator? I appreciate that what I’m trying to do is not
>> something which it was designed to handle, but it _was working_ at some
>> point.
>>
>> BTW, it seems to make no difference whether I use sharing or not, but
>> when I got it to successfully check yesterday it was using sharing.
>>
>> (*) If you’ve seen the paper I wrote on this, note that the model checker
>> is substantially different now.
>>
>> (*) Also note that originally the definition for petersons-search read:
>>
>> petersons-search
>>    = search $
>>        and′ mutex? (and′ sf? termination?)
>>        (model petersons initialState)
>>
>> but I gave it a fixed depth of 25 just to stop it doing any unnecessary
>> searching.
>>
>> Liam
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160203/c8a88f34/attachment-0001.html