Mandy Martino | 6 Feb 05:05 2016

how to run this rewrite example

Hi ,

when run the code directly, it return missing definition, 

how to write this definition?


Missing definition for plus-commute

The clause containing the with-abstraction has no right-hand side. Instead it is followed by a number of clauses with an extra argument on the left, separated from ...

open import Prelude

data Bool2 : Set where
 true : Bool2
 false : Bool2

not2 : Bool2 -> Bool2
not2 true = false
not2 false = true

identity2 : (A : Set) -> A -> A
identity2 A x = x

data Nat2 : Set where
 zero2 : Nat2
 suc : Nat2 -> Nat2

_or2_ : Bool2 -> Bool2 -> Bool2
false or2 x = x
true or2 _ = true

if2_then2_else2_ : (A : Set) -> Bool2 -> A -> A -> A
if2 true then2 x else2 y = x
if2 false then2 x else2 y = y

plus-commute : (a b : Nat) → a + b ≡ b + a

thm : (a b : Nat) → P (a + b) → P (b + a)
thm a b t with   a + b  | plus-commute a b
thm a b t    | .(b + a) | refl = t

main = 
 if2_then2_else2_ Bool2 true (putStrLn "it is true") (putStrLn "it is else case")
 putStrLn "Hello World"


Agda mailing list
Sergei Meshveliani | 5 Feb 21:34 2016

`with' question

Please, what is wrong in the below program?

module Useful where
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Nat   using (ℕ)
open import Data.List  using (List; []; _∷_)

module _ {α} {A : Set α}
    data Null : List A → Set α  where  isNull : Null []

    null? :  (xs : List A) → Dec (Null xs)
    null? []      = yes isNull
    null? (_ ∷ _) = no λ()

f : List ℕ  → ℕ
f []      =  1
f (_ ∷ _) =  0

postulate  ps : List ℕ

g : Dec (f ps ≡ 1)
g with null? ps
... | yes null-ps =  yes (h null-ps)
... | no _        =  no neq
                     postulate neq : f ps ≢ 1

g' : Dec (f ps ≡ 1)
   with ps | null? ps
... | _ | yes null-ps =  yes (h null-ps)
... | _ | no _        =  no neq
                         postulate neq : f ps ≢ 1

g  is type-checked,
and for  g'  it reports that  null-ps  has not the needed type.

(The Agda language is difficult in its proof composition part. 
I do not understand basics of Agda after 3 year practicing with it). 

In this example, the part  "ps |"  is dummy.
But in the real example I need to use both  ps  and  null? ps,
like this:

  ... | []           | null-ps =  foo null-ps
  ... | (_ , 0) :: _ | _       =  \bot-elim ... 0>0

g'  is a simplification for this real example.

Thank you in advance for explanation,

Sergei Meshveliani | 4 Feb 18:46 2016

"xs ≡ [] → " question

what is the most natural way to prove  g  below?

open import Data.Nat  using (ℕ)
open import Data.List using (List; []; _∷_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

f : List ℕ  → ℕ
f []      =  1
f (_ ∷ _) =  0

postulate  ps : List ℕ

g : ps ≡ [] → f ps ≡ 1
g PE.refl =  PE.refl    -- is not type-checked

I find the proof that uses

  lemma : ∀ {xs} → xs ≡ [] → f xs ≡ 1
  lemma PE.refl = PE.refl

1) why the same implementation rule does not work for  g ?
2) is there possible a simpler proof than by introducing  lemma ?


Andreas Abel | 4 Feb 17:19 2016

A quiz: what should the types of these definitions be?

Hi, this is a poll about what you would expect Agda to do about the 
hiding of parameters if you have definitions inside a parametrized 
record inside a parametrized module.

(If you want to cheat, please be aware that different versions of Agda 
might give different answers. ;-))

module _ where

-- M1/R1: visible parameter
-- M2/R2: hidden parameter

module M1 (A : Set) where

   record R1 (B : Set) : Set where
     field f : A
     g = f
     id : B → B
     id x = x

   record R2 {B : Set} : Set where
     field f : A
     g = f
     id : B → B
     id x = x

module M2 {A : Set} where

   record R1 (B : Set) : Set where
     field f : A
     g = f
     id : B → B
     id x = x

   record R2 {B : Set} : Set where
     field f : A
     g = f
     id : B → B
     id x = x

m1r1f  : ?
m1r1f  = M1.R1.f

m1r1g  : ?
m1r1g  = M1.R1.g

m1r1id : ?
m1r1id =

m1r2f  : ?
m1r2f  = M1.R2.f

m1r2g  : ?
m1r2g  = M1.R2.g

m1r2id : ?
m1r2id =

m2r1f  : ?
m2r1f  = M2.R1.f

m2r1g  : ?
m2r1g  = M2.R1.g

m2r1id : ?
m2r1id =

m2r2f  : ?
m2r2f  = M2.R2.f

m2r2g  : ?
m2r2g  = M2.R2.g

m2r2id : ?
m2r2id =


Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

Thorsten Altenkirch | 4 Feb 11:19 2016

Efficiency of type checking

I haven’t followed the ongoing discussion in detail but it seems to me that we need a different approach if we want to make dependently typed programming feasible in practice. I believe we need a programmable equality checker which has to be certified that it is sound so that equality checking can be modified by the user in a safe way. This would also alleviate the need for rewriting which is potentially unsound. I think this is vaguely in line with Andrej Bauer’s Andromeda proposal.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
Agda mailing list
Chris Kapulkin | 3 Feb 18:59 2016

Workshop on Homotopy Type Theory and Univalent Foundations, Fields Institute, May 16-20, 2016

Dear all,

This is a reminder about the Workshop on Homotopy Type Theory and
Univalent Foundations to be held at the Fields Institute in Toronto,
May 16-20, 2016. The workshop will consist of mini-courses on several
aspects of Homotopy Type Theory, as well as research talks, both
invited and contributed. The registration and abstract submission are
available at:

Limited financial support is available to cover participants' travel
and local expenses. Priority will be given to junior researchers and
those without other sources of funding. To be considered for funding,
please fill out the Funding Application Form which is a part of the
online registration.

Important dates:
* Funding application deadline: February 28, 2016.
* Contributed talk submission deadline: February 28, 2016.
* Registration deadline: May 2, 2016. (Early registration is
appreciated, to help us in our planning.)



Robert Harper (Carnegie Mellon University): Computational Higher Type Theory
Daniel R. Licata (Wesleyan University): Cubical Type Theory
Peter LeFanu Lumsdaine (Stockholm University): Homotopy-theoretic
models of type theory
Michael Shulman (University of San Diego): Synthetic Homotopy Theory

Invited speakers

Benedikt Ahrens (IAS, Princeton)
Thorsten Altenkirch (University of Nottingham)
Jeremy Avigad (Carnegie Mellon University)
Emily Riehl (Johns Hopkins University)
Michael Warren (HRL Laboratories)

We are looking forward to seeing you in Toronto!

Organizers: Dan Christensen, Rick Jardine, Chris Kapulkin
Sergei Meshveliani | 3 Feb 20:30 2016

more on type check performance

I wrote today about GHC that with GHC I always manage to sensibly
optimize my Haskell programs for performance.
But I need to add the following.
Sometimes, in rare cases, I cannot find the cost consuming place other
than by using the GHC profiling, with manually setting cost centers in
the source. This always helps me to discover the place (and this place
never occurs the one that I expected). 


Peter Achten | 2 Feb 10:28 2016

[TFP 2016] 1st call for papers

                     C A L L   F O R   P A P E R S

                     ======== TFP 2016 ===========

           17th Symposium on Trends in Functional Programming
                            June 8-10, 2016
                  University of Maryland, College Park
                          Near Washington, DC

The symposium on Trends in Functional Programming (TFP) is an
international forum for researchers with interests in all aspects of
functional programming, taking a broad view of current and future
trends in the area. It aspires to be a lively environment for
presenting the latest research results, and other contributions (see
below). Authors of draft papers will be invited to submit revised
papers based on the feedback receive at the symposium.  A
post-symposium refereeing process will then select a subset of these
articles for formal publication.

TFP 2016 will be the main event of a pair of functional programming
events. TFP 2016 will be accompanied by the International Workshop on
Trends in Functional Programming in Education (TFPIE), which will take
place on June 7nd.

The TFP symposium is the heir of the successful series of Scottish
Functional Programming Workshops. Previous TFP symposia were held in
    * Edinburgh (Scotland) in 2003;
    * Munich (Germany) in 2004;
    * Tallinn (Estonia) in 2005;
    * Nottingham (UK) in 2006;
    * New York (USA) in 2007;
    * Nijmegen (The Netherlands) in 2008;
    * Komarno (Slovakia) in 2009;
    * Oklahoma (USA) in 2010;
    * Madrid (Spain) in 2011;
    * St. Andrews (UK) in 2012;
    * Provo (Utah, USA) in 2013;
    * Soesterberg (The Netherlands) in 2014;
    * and Inria Sophia-Antipolis (France) in 2015.
For further general information about TFP please see the TFP homepage.

== SCOPE ==

The symposium recognizes that new trends may arise through various
routes.  As part of the Symposium's focus on trends we therefore
identify the following five article categories. High-quality articles
are solicited in any of these categories:

Research Articles: leading-edge, previously unpublished research work
Position Articles: on what new trends should or should not be
Project Articles: descriptions of recently started new projects
Evaluation Articles: what lessons can be drawn from a finished project
Overview Articles: summarizing work with respect to a trendy subject

Articles must be original and not simultaneously submitted for
publication to any other forum. They may consider any aspect of
functional programming: theoretical, implementation-oriented, or
experience-oriented.  Applications of functional programming
techniques to other languages are also within the scope of the

Topics suitable for the symposium include, but are not limited to:

      Functional programming and multicore/manycore computing
      Functional programming in the cloud
      High performance functional computing
      Extra-functional (behavioural) properties of functional programs
      Dependently typed functional programming
      Validation and verification of functional programs
      Debugging and profiling for functional languages
      Functional programming in different application areas:
        security, mobility, telecommunications applications, embedded
        systems, global computing, grids, etc.
      Interoperability with imperative programming languages
      Novel memory management techniques
      Program analysis and transformation techniques
      Empirical performance studies
      Abstract/virtual machines and compilers for functional languages
      (Embedded) domain specific languages
      New implementation strategies
      Any new emerging trend in the functional programming area

If you are in doubt on whether your article is within the scope of
TFP, please contact the TFP 2016 program chair, David Van Horn.


To reward excellent contributions, TFP awards a prize for the best paper
accepted for the formal proceedings.

TFP traditionally pays special attention to research students,
acknowledging that students are almost by definition part of new
subject trends. A student paper is one for which the authors state
that the paper is mainly the work of students, the students are listed
as first authors, and a student would present the paper. A prize for
the best student paper is awarded each year.

In both cases, it is the PC of TFP that awards the prize. In case the
best paper happens to be a student paper, that paper will then receive
both prizes.


TFP is financially supported by CyberPoint, Galois, Trail of Bits, and
the University of Maryland Computer Science Department.


Acceptance of articles for presentation at the symposium is based on a
lightweight peer review process of extended abstracts (4 to 10 pages
in length) or full papers (20 pages). The submission must clearly
indicate which category it belongs to: research, position, project,
evaluation, or overview paper. It should also indicate which authors
are research students, and whether the main author(s) are students.  A
draft paper for which ALL authors are students will receive additional
feedback by one of the PC members shortly after the symposium has
taken place.

We use EasyChair for the refereeing process. Papers must be submitted at:

Papers must be written in English, and written using the LNCS
style. For more information about formatting please consult the
Springer LNCS web site:


Submission of draft papers:     April 8, 2016
Notification:                   April 15, 2016
Registration:                   May 13, 2016
TFP Symposium:                  June 8-10, 2016
Student papers feedback:        June 14, 2016
Submission for formal review:   July 14, 2016
Notification of acceptance:     September 14, 2016
Camera ready paper:             October 14, 2016


Amal Ahmed              Northeastern University (US)
Nada Amin               École Polytechnique Fédérale de Lausanne (CH)
Kenichi Asai            Ochanomizu University (JP)
Małgorzata Biernacka    University of Wroclaw (PL)
Laura Castro            University of A Coruña (ES)
Ravi Chugh              University of Chicago (US)
Silvia Ghilezan         University of Novi Sad (SR)
Clemens Grelck          University of Amsterdam (NL)
John Hughes             Chalmers University of Technology (SE)
Suresh Jagannathan      Purdue University (US)
Pieter Koopman          Radboud University Nijmegen (NL)
Geoffrey Mainland       Drexel University (US)
Chris Martens           University of California, Santa Cruz (US)
Jay McCarthy            University of Massachusetts, Lowell (US)
Heather Miller          École Polytechnique Fédérale de Lausanne (CH)
Manuel Serrano          INRIA, Sophia-Antipolis (FR)
Scott Smith             Johns Hopkins University (US)
Éric Tanter             University of Chile (CL)
David Van Horn (Chair)  University of Maryland (US)
Niki Vazou              University of California, San Diego (US)
Kenichi Asai | 2 Feb 04:55 2016

pattern match for LessThan'?

In the standard library, we have:

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

Suppose we have a value:

v : m ≤′ n

for some m and n.  From the definition of the type, we see that there
must be only one choice for v: if m = n, then v must be refl, while if
m < n, then v must be step.  (And if m > n, v must be ().)

Thus, I want to refine v according to m and n.  Can I do that?  Or in
more general, can I write an inversion function that deconstructs v?
If I case split on v, I always obtain the both possibilities and I
don't see any way to remove the impossible case.

For "less than" without prime:

data _≤_ : Rel ℕ where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

we can simply case split on the value of this type, because the type
uniquely and evidently shows which constructor to take.  I want to do
the same (or similar) thing for "less than" with prime.



Kenichi Asai
Liam O'Connor | 1 Feb 09:46 2016

Type-checker evaluator performance

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.

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.

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:

   = 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.

Martin Stone Davis | 31 Jan 20:53 2016

Expose more of Agda to reflection?

Via reflection, it currently isn't straightforward to construct an agda function that invokes a rewrite. Exposing Agda's rewriting machinery to reflection would make this much easier. (Another neat idea is to expose agsy!) On the other hand, the exact same algorithms could be reproduced in the Agda language and it might be advisable to keep the reflection interface clean, especially considering that work done by "rewrite" or agsy might change in the future.

Am I correct that Agda.TypeChecking.Rewriting can now be exactly reproduced in Agda? I'm studying the algorithm and would love to know that the path ahead of me is clear.
Martin Stone Davis

1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578
Electronic Mail: martin.stone.davis <at>
Agda mailing list