Sergei Meshveliani | 26 Jul 15:12 2015

installing agda-


I am trying to install  agda-  on  ghc-7.10.1,  Debian Linux.
The commands

  > cabal update
  > cabal install Agda

produce the report

Preprocessing library data-hash-
ghc: ghc no longer supports single-file style package databases
(dist/package.conf.inplace) use 'ghc-pkg init' to create the database
with the correct format.
Failed to install data-hash-

  > ghc-pkg init
ghc-pkg: command-line syntax error
For usage information see 'ghc-pkg --help'.

  > ghc-pkg --help

  ghc-pkg init {path}

I understand this as that  {path} can be omitted.

Please, how to install Agda ?
(Continue reading)

Andreas Abel | 24 Jul 11:15 2015

Overloading atoms and operators

I see why there is a need to overload operators of ,different arity by 
the same name, for instance, unary and binary minus.

   ℤ : Set
   -_ : ℤ → ℤ
   _-_ : (x y : ℤ) → ℤ

infix 10 -_
infixl 5 _-_

test : ℤ → ℤ
test x = - x - x

But what is the point of overloading and atom with an operator of the 
same name?  This is, as far as I know, not mathematical practice, and 
would only serve obfuscation.

   A B : Set
   x a : A
   _x_ : A → A → B

infix 10 _x_

There seems no way of making Agda parse

   a x a

thus, the operator is unusable.
(Continue reading)

Guillermo Calderon | 21 Jul 17:31 2015

where definitions and with


Sometimes, I find convenient to write something like that:

	ff  x y z  with foo = ?
	     where foo =  <something  depending on x y z>

But Agda rejects it:  "not in scope foo ..."

I conclude that the scope of where definitions does not include the 
"with" construct.
Is there a good reason for this restriction?

David Van Horn | 18 Jul 18:42 2015

ICFP 2015 Call for Participation

[ Early registration ends 3 August. ]


Call for Participation

ICFP 2015
20th ACM SIGPLAN International Conference on Functional Programming
and affiliated events

August 30 - September 5, 2015
Vancouver, British Columbia, Canada


ICFP provides a forum for researchers and developers to hear
about the latest work on the design, implementations, principles, and
uses of functional programming. The conference covers the entire
spectrum of work, from practice to theory, including its peripheries.

A full week dedicated to functional programming:
1 conference, 1 symposium, 11 workshops, tutorials,
programming contest results, student research competition,
and mentoring workshop

 * Program:

 * Accepted Papers:
(Continue reading)

Andrew Pitts | 14 Jul 10:48 2015

question about a form of irrelevance elimination

Since version 2.2.8, Agda supports irrelevancy annotations
Among other things this allows one to define a form of truncation:

record ! {ℓ : Level}(A : Set ℓ) : Set ℓ where
  constructor ![_]
    .prf : A
open ! public

Since the elements of ! A are definitionally irrelevant, they are also
propositionally irrelevant, i.e. ! A is a proposition in the sense of
Homotopy Type Theory:

isProp : {ℓ : Level}(A : Set ℓ) → Set ℓ
isProp A = (x y : A) → x ≡ y
!isprop : {ℓ : Level}{A : Set ℓ} → isProp (! A)
!isprop _ _ = refl

I would like to be able to escape from an irrelevant context in the
case of propositions:

  !elim : {ℓ : Level}{A : Set ℓ}.(_ : isProp A) → (! A) → A

Does adding such a postulate destroy logical consistency?

Andy Pitts
Joachim Breitner | 13 Jul 14:43 2015

HOTT-style reals in Agda

Hi list,

I was looking at the definition of reals via Cauchy sequences in the
HOTT book, and I wonder how tricky it would be to implement that within
the hott-agda library.

Given that it has not been done before (as far as I can tell) – is that
because it is obvious and trivial, or because it is known how to do it,
and just tedious, or is it because it is expected to be challenging?



Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
Agda mailing list
effectfully | 7 Jul 05:33 2015

Agda can't find an obvious instance.

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Fin

  fz : Fin 1
  fz = zero

z : ∀ {n} {{_ : Fin n}} -> ℕ
z = 0

yellow : z ≡ 0
yellow = refl

ok : z {1} ≡ 0
ok = refl


The instance is not picked in `yellow'. Agda can't find the instance
even in this case:


record R (n m : ℕ) : Set where

  r : R 0 1
  r = _

(Continue reading)

Sergei Meshveliani | 6 Jul 14:06 2015

segmentation fault

To my 

> Also type-checking my project sometimes breaks by segmentation fault,
> and it improves after restarting Linux.

On Sun Jul 5  Andreas Abel abela at 

> Is this due to ?

I cannot tell. And cannot reliably reproduce it. I type-check several
modules under emacs 
(Agda,  ghc-7.8.3, and also ghc-7.10.1). 
For some modules, it becomes slow, and I find that it is 
easier to control memory without emacs, and start type-checking by calling 
Agda from the command line. After this (and somewhat once in a week, and 
suddenly), it happens  segmentation fault. 
And then, it repeats -- until I restart Linux.
I wonder of whether this is due to Agda.
This may be, say, due to hardware.


Andreas Abel | 6 Jul 09:33 2015

Should not _ patterns be resolvable by inaccessible patterns?

If you define transitivity of propositional equality without hiding 
value arguments, you have to explicitly choose where to put the dots:

   transV1 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
   transV1 _ ._ ._ refl refl = refl

   transV2 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
   transV2 ._ _ ._ refl refl = refl

   transV3 : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
   transV3 ._ ._ _ refl refl = refl

With hidden arguments, you need not care:

   transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
   transH refl refl = refl

Of course, when giving the hidden arguments, it is the same as for 
visible arguments:

   transH1 : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
   transH1 {a = _}{b = ._}{c = ._} refl refl = refl

The user has more flexibility when an argument is hidden.  When an 
argument is given, the user has to actively make a decision whether a 
pattern must be a dot pattern or must not be one.  There is no "I don't 
care, please figure it out for me" as there is for hidden arguments. 
This seems to be a mismatch.

(Continue reading)

Sergei Meshveliani | 5 Jul 21:50 2015

arguments in `data' pattern

Can anyone explain, please, 
what is the matter with the attached (small) code?

It includes

data DecPrime : ℕ → Set      -- constructively decided primality 
     prime    : {n : ℕ} → IsPrime n → DecPrime n
     unity    : DecPrime 1
     composed : {m n : ℕ} → IsNontrivialDivisor m n → DecPrime n

postulate  decPrime : (n : ℕ) → DecPrime n

f : ℕ → ℕ
f n = g n (decPrime n)
      g : (m : ℕ) → DecPrime m → ℕ

      g 1 unity                = 1
      g _ (prime _)            = 2
      g _ (composed {k} {_} _) = k

This is on  Agda,  ghc-7.8.3.

The last pattern in  g  is not type-checked.
And if I remove  {_}  from it, then it is type-checked.
But `composed' has two implicit arguments. 

(Continue reading)

Sergei Meshveliani | 5 Jul 12:49 2015

"Not a valid let-declaration"

The checker reports

  Not a valid let-declaration when scope checking
  <a long citation of the `let' code> 

It is desirable to point (when it is easy) say, at the first part which
is not valid.