Mateusz Kowalczyk | 23 Oct 02:02 2014

Info on interacting with the Agda process


Say I wanted to talk to Agda like emacs does: get all the type info,
highlighting &c &c. Is there a place where this process is documented,
notably the format that's expected both ways or is looking at the ELisp
and Haskell source the only way?

I would also ask whether we could just talk to Agda directly, cutting
out the process and parsing of the information: say we can talk to
Haskell natively, would it be viable to just talk straight to the Agda
library or would it be awkward to do so? I can imagine a much better
degree of freedom with this approach but I don't know whether it was
ever intended to be used this way. Notably, the package on Hackage says
“Note that the Agda library does not follow the package versioning
policy, because it is not intended to be used by third-party packages.”.



Mateusz K.
Michael Winter | 20 Oct 21:19 2014

CFP: Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

                           CALL FOR PAPERS

                  15th International Conference on
    Relational and Algebraic Methods in Computer Science (RAMiCS 2015)

            28 September to 1 October 2015, Braga, Portugal


 We invite submissions in the general area of Relational and Algebraic 
 Methods  in Computer Science. Special focus will lie on formal methods 
 for software engineering, logics of programs and links with neighbouring 

 Particular topics of interest for the conference cover,
 but are not limited to:

 * Algebraic approaches to
   - specification, development, verification, and analysis of programs
     and algorithms
   - computational logic, in particular logics of programs, modal and
     dynamic logics, interval and temporal logics
   - semantics of programming languages

(Continue reading)

Sergei Meshveliani | 19 Oct 18:06 2014

explicit irrelevance question

Dear Agda developers,

can you, please tell whether the below statement  g=f-if
must have a proof in Agda ?
If yes, then what can be a proof ?

(I am stuck with both explicit irrelevance and a dot-annotated



open import Level            using (_⊔_)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary  using (module IsEquivalence;
                                    module DecSetoid; DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty using (⊥-elim)

module _ {α α=} (A : DecSetoid α α=) (0# : DecSetoid.Carrier A)
  open DecSetoid A using (_≈_; _≟_; isEquivalence)
                                    renaming (Carrier to C)
  open IsEquivalence isEquivalence renaming (refl to ≈refl)

  record Foo : Set (α ⊔ α=)
(Continue reading)

Helmut Grohne | 15 Oct 13:15 2014

Internal error at src/full/Agda/TypeChecking/Substitute.hs:144

Dear Agda developers,

While refactoring some Agda code I ran into the following error message:

| Checking Error (../full/path/to/Error.agda).
| An internal error has occurred. Please report this as a bug.
| Location of the error: src/full/Agda/TypeChecking/Substitute.hs:144

This is produced using Agda 2.4.2 as obtained using cabal on a Linux
amd64 system with GHC 7.6.3.

I went ahead and tried to find a reproducer with less than 1000 lines.
After feeding Agda 30000 samples, I came up with the following 7 lines:

data A (B : Set) : Set where
module C where
  record D : Set where
module E (F : Set) (G : A F) where
  open C public using (module D)
module H (I : Set) (J : A I) where
  open E I J using ()

Is this also reproducible on the development version of Agda?

Andrew Harris | 14 Oct 04:13 2014

simple question


   I'm trying to follow along in the very good paper "Dependent Types At Work" written by Ana Bove and Peter Dybjer.  I'm stuck at trying to prove "eq-succ", which is one of the exercises in Section 4.4.  The closest I can make it is the following:

{- proof of eq-succ -}
eq-succ : {n m : Nat} → n == m → succ n == succ m
eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h → ((succ i) + m) == (plus (succ i) m)) m

But this does not typecheck, I get the error:

Set !=< (succ i + m) == plus (succ i) m of type Set₁
when checking that the expression (succ i + m) == plus (succ i) m
has type (succ i + m) == plus (succ i) m

I'm stuck -- I don't quite understand what I'm supposed to create an element of Set_1 that has a signature of (succ i + m) == plus (succ i) m, (if that's what I'm supposed to do).  Any hints would be appreciated!

Agda mailing list
Pepijn Kokke | 12 Oct 13:28 2014

Expanding literate Agda

Dear all,

I've implemented a pre-processor to "unlit" various styles of literate code, i.e. LaTeX-style, bird tags, Markdown-style code blocks, etcetera. I'm currently trying to integrate it into Agda. There are currently two proposals for how to do this.

The first is the following:

Try to infer the literate format from the file, making it explicit with Agda command-line arguments if necessary. 
This would mean that, for instance, if the "unlit" program would encounter a "\begin{code}" tag, it would assume the literate Agda file was was written in LaTeX style, if it encountered a "```" fence it would assume Markdown, etcetera... 
(I would personally prefer that a bird tag would also indicate Markdown, because the two formats integrate so well and are already used in this manner in the Haskell community.)
The advantages of this approach is that it can easily be integrated into the current Agda, and all literate files would have the .lagda extension.
In the case where it is desirable to mix formats in a strange way (i.e. mix bird tags and LaTeX or even LaTeX blocks and Markdown blocks) command-line arguments could be passed to Agda explicitly stating the literate style---though I'm guessing this would never be necessary.

The second proposal is the following:

Each style of literate Agda would have its own extension. For instance: LaTeX-style would ".agda.tex", Markdown would use "" and Bird-style would use ".agda.txt". 
The advantages of this approach is that there is no inference needed, as the format will be unambiguously specified in the extension. 
The problem with this approach is that it will require modifications to many parts of the Agda ecosystem. For instance, the code that resolves module names to files would have to change to also take ".agda.tex" and such into consideration. The same modifications would probably have to be made for the Emacs (and other) editing mode. This would constitute many (trivial) changes across the Agda codebase. 

I'd like to hear your thoughts on these different approaches, or---if you have proposals of dealing with this in a different manner---how you would solve this problem.

Agda mailing list
José Pedro Magalhães | 10 Oct 14:58 2014

Mathematics of Program Construction (MPC 2015): first call for papers

Apologies for multiple copies.


12th International Conference on Mathematics of Program Construction (MPC 2015)
Königswinter, Germany, 29 June - 1 July 2015


The MPC conferences aim to promote the development of mathematical principles
and techniques that are demonstrably practical and effective in the process of
constructing computer programs, broadly interpreted.

The 2015 MPC conference will be held in Königswinter, Germany, from 29th June to
1st July 2015. The previous conferences were held in Twente, The Netherlands
(1989), Oxford, UK (1992), Kloster Irsee, Germany (1995), Marstrand, Sweden
(1998), Ponte de Lima, Portugal (2000), Dagstuhl, Germany (2002), Stirling, UK
(2004, colocated with AMAST), Kuressaare, Estonia (2006, colocated with AMAST),
Marseille, France (2008), Québec City, Canada (2010, colocated with AMAST), and
Madrid, Spain (2012).


Papers are solicited on mathematical methods and tools put to use in program
construction. Topics of interest range from algorithmics to support for program
construction in programming languages and systems. The notion of "program" is
broad, from algorithms to hardware. Some typical areas are type systems, program
analysis and transformation, programming-language semantics, security, and
program logics. Theoretical contributions are welcome, provided that their
relevance to program construction is clear. Reports on applications are welcome,
provided that their mathematical basis is evident.

We also encourage the submission of "pearls": elegant, instructive, and fun
essays on the mathematics of program construction.


   * Submission of abstracts:      26 January 2015
   * Submission of full papers:     2 February 2015
   * Notification to authors:      16 March 2015
   * Final version:                13 April 2015


Submission is in two stages. Abstracts (plain text, 10 to 20 lines) must be
submitted by 26 January 2015. Full papers (pdf) adhering to the LaTeX llncs
style must be submitted by 2 February 2015. There is no official page limit, but
authors should strive for brevity. The web-based system EasyChair will be used

Papers must report previously unpublished work, and must not be submitted
concurrently to a journal or to another conference with refereed proceedings.
Accepted papers must be presented at the conference by one of the authors.
Please feel free to write to mpc2015-bC77Qfv0vuxrovVCs/ with any questions
about academic matters.

The proceedings of MPC 2015 will be published in Springer-Verlag's Lecture Notes
in Computer Science series, as have all the previous editions. Authors of
accepted papers will be expected to transfer copyright to Springer for this
purpose. After the conference, authors of the best papers will be invited to
submit revised versions to a special issue of the Elsevier journal Science of
Computer Programming.


Ralf Hinze                University of Oxford, UK (chair)

Eerke Boiten              University of Kent, UK
Jules Desharnais          Université Laval, Canada
Lindsay Groves            Victoria University of Wellington, New Zealand
Zhenjiang Hu              National Institute of Informatics, Japan
Graham Hutton             University of Nottingham, UK
Johan Jeuring             Utrecht University and Open University, The Netherlands
Jay McCarthy              Vassar College, US
Bernhard Möller           Universität Augsburg, Germany
Shin-Cheng Mu             Academia Sinica, Taiwan
Dave Naumann              Stevens Institute of Technology, US
Pablo Nogueira            Universidad Politécnica de Madrid, Spain
Ulf Norell                University of Gothenburg, Sweden
Bruno C. d. S. Oliveira   The University of Hong Kong, Hong Kong
José Nuno Oliveira        Universidade do Minho, Portugal
Alberto Pardo             Universidad de la República, Uruguay
Christine Paulin-Mohring  INRIA-Université Paris-Sud, France
Tom Schrijvers  KU Leuven, Belgium
Emil Sekerinski           McMaster University, Canada
Tim Sheard                Portland State University, US
Anya Tafliovich           University of Toronto Scarborough, Canada
Tarmo Uustalu             Institute of Cybernetics, Estonia
Janis Voigtländer         Universität Bonn, Germany


The conference will take place in Königswinter, Maritim Hotel, where
accommodation has been reserved. Königswinter is situated on the right bank of
the river Rhine, opposite Germany's former capital Bonn, at the foot of the


Ralf Hinze                      University of Oxford, UK (co-chair)
Janis Voigtländer               Universität Bonn, Germany (co-chair)
José Pedro Magalhães            University of Oxford, UK
Nicolas Wu                      University of Oxford, UK

For queries about local matters, please write to

Agda mailing list
Dmytro Starosud | 11 Oct 21:50 2014

(Stronger) double negation of law of excluded middle

Hello everyone

Could you have a look at my problem below?
I am trying to prove something that looks like just better double negation of law of excluded middle:

¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)
¬¬lem = _

Which I cannot prove, whereas following one is pretty easy to prove:

¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))

Is it actually possible to prove the first one in constructive logic (in particular in Agda)?

Thanks in advance for your help!

Best regards,

Agda mailing list
Sergei Meshveliani | 10 Oct 17:44 2014


I program mapping the _⊆_ relation on lists:


  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → {xs ys : List C} →
                                          xs ⊆ ys → map f xs ⊆' map f ys

  map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
         (x , x∈≡xs , fx≈z) = counter-map f xs z z∈f-xs
         x∈xs    = ∈≡→∈ x∈≡xs
         x∈ys    = xs⊆ys x∈xs
         fx∈f-ys = map∈ f fCong x∈ys
       cong₁∈' fx≈z fx∈f-ys

Here _≈_ and _≈'_ are of the two corresponding setoids.
This implementation uses 

 map∈ : (f : C → C')  → (f Preserves _≈_ ⟶ _≈'_) → {x : C} →
        {xs : List C} → x ∈ xs                   → f x ∈' map f xs 
 counter-map : (f : C → C') → (xs : List C) → (y : C') → y ∈' map f xs →
                                               ∃ \x → x ∈≡ xs × f x ≈' y
 cong₁∈' : {zs : List C'} → (\x → x ∈' zs) Respects _≈'_

-- which I implement in their turn.

And I wonder of whether all this is inventing a bicycle.
Can  map⊆  be expressed in a simpler way?
What Standard library has for all this?


Andrea Vezzosi | 10 Oct 17:11 2014

Re: Restrictions on 'with' introductions?

If you want to understand "with" better you can look at the "More in
depth" part of this:

I find that with enough type dependencies the "with" construct only
makes sense if you think of its desugaring into an helper function. It
should also clarify the meaning of the "w" variables in the error


On Tue, Oct 7, 2014 at 2:31 AM, Dan Krejsa <dan.krejsa@...> wrote:
> Hi,
> I'm trying to work through a self-imposed exercise in Agda, proving
> that a functional insertion sort algorithm on lists is correct (i.e., it
> produces
> an ordered list that is in fact a permutation of the original list).
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)
> In any case, I notice that I'm structuring a lot of the more difficult
> proofs / functions as a long chain of 'with' patterns  (here's a short one):
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y
> ... | fxy  with term4
> ... | term4 = ?
> However, sometimes when I try to add a well-typed term to
> the values scrutinized via the 'with' , Agda complains of some type
> error 'when checking that the type <some long type> of the generated with
> function is well-formed'.
> For instance, maybe the above example works fine, but if I also try to
> get Agda to remember that fxy = f x y using inspect-on-steroids,
> some_func : type
> some_func  args  with term1 | term 2
> ... | term1-deconstructed | term2-deconstructed  with f x y | inspect (f x)
> y
> ... | fxy | [ fxydef ] with term4
> ... | term4 = ?
> then I get a type error about the generated with-function.  (That's just an
> example, other sorts of as-far-as-I-can-see good terms sometimes also cause
> similar problems.)
> So, I don't really understand what the 'with function' is, and what are the
> restrictions on the terms that one can scrutinize using 'with'.
> Or, if this is just a shortcoming/bug in current Agda, what would be a
> workaround for such a case?
> Thanks,
> - Dan
> P.S. I could post my file, but it's pretty hairy still. (I could try to find
> a small or minimal test case if this is not already a known problem.)
> That reminds me: is there a good forum for asking for help improving
> practical Agda proving style & skills?  I'm not in school and am learning
> mostly on my own out of personal interest.  I'm hoping to improve my nose
> for 'code smells' in Agda, things like the 'green slime' mentioned in a
> recent Connor McBride paper ;-)
> _______________________________________________
> Agda mailing list
> Agda@...
Nils Anders Danielsson | 10 Oct 17:00 2014

Re: Restrictions on 'with' introductions?

On 2014-10-07 02:31, Dan Krejsa wrote:
> (The 'ordered' bit goes through pretty easy, but the 'permutation' bit
> is proving something of a pain to me.  In particular, I'm developing all the
> permutation infrastructure myself...)

Proofs of this kind are hopefully easy (but perhaps boring) if you use
the technique that I describe in "Bag Equivalence via a Proof-Relevant
Membership Relation":

For instance, here's how one can implement tree sort, and prove that the
output is a permutation of the input:

The following code by Bob Atkey uses a different approach, embedding
linear logic inside Agda to give you the permutation property "for