Mateusz Kowalczyk | 25 Apr 18:46 2015

Sane whitespace with agda --latex


It seems that agda --latex gives a result with horizontal whitespace
that often doesn't resemble the source file. Sometimes things like

foo : Bar x

will be turned into

foo : Bar x

Sometimes stuff like

x      : a -> b
longer : a -> b
foo    : a -> b

Results in some things being properly aligned and others not.

I even had a case of

foo : x
    -> let bar : a -> b
     bar = …
       in …

(Continue reading)

Sergei Meshveliani | 25 Apr 11:47 2015

DoCon-A link

Dear Agda page administrator,

please, add the  DoCon-A  link to the list 
  "Libraries and other developments"


a library for list processing and a certain initial part of computer
algebra, with providing all Agda proofs. 


N. Raghavendra | 25 Apr 10:49 2015


I'm writing a homotopy type theory library for myself, which is
independent of the Agda stdlib, and of the HoTT-Agda library available
elsewhere.  I've defined equality as in Relation.Binary.Core of Agda
stdlib.  Now, I am wondering whether to copy the pragmas

{-# BUILTIN REFL refl #-}

to my file.  I don't understand what they mean.  What is the effect of
these instructions?  Do they establish some kind of relation between
judgemental equality, and the propositional equality that's defined in
Relation.Binary.Core.  For instance, do they say that judgemental
equality implies propositional equality?

I gather from the ref. manual that BUILTIN pragmas tell Agda that the
"given name implements one of the builtin types".  refl is only a
constructor, not a type.  I'd really appreciate if someone explained all

(I apologise if all this is trivial.  I come from another area of
mathematics, and am not familiar with type theory and proof assistants.)

Thanks and cheers,

N. Raghavendra <raghu@...>,
Harish-Chandra Research Institute,
effectfully | 24 Apr 17:32 2015

Type-preserving renaming and substitutions for a dependently typed lambda calculus.

Hello. I was studying different deep embeddings of a dependently typed
lambda calculus, and I found three works: Nils Anders Danielsson's
thesis, James Chapman's thesis and Typed Syntactic Meta-programming by
Dominique Devriese and Frank Piessens (I'm not counting Conor
McBride's Outrageous but Meaningful Coincidences). However the first
work uses explicit weakening for the base encoding (there is also a
conversion to implicit terms), the second work moreover uses explicit
substitutions, and the third work is based on a homogeneous datatype,
which represents both types and terms.
I wrote some code in order to understand what are the problems with
the natural representation (a bunch of mutually defined datatypes with
the usual semantics) equipped with implicit weakening and
substitutions. A module that contains implicit weakening can be found
at [1] (some explanations can be found at [2]), but there is no
substitutions stuff and no applications at all. The code looks simple
and natural until the proving part begins, which is somewhat
complicated. I also wrote a sketch for the full system (the same +
applications and hence substitutions) with all proofs being postulated
So I'm wondering, if there is something silly with my representation,
that cause this amount of proving, and if there exist works, which
elarobate this kind of encoding.
Thank you for your attention.

Guillermo Calderon - INCO | 23 Apr 17:38 2015

record field as Instance Argument


I am working with Instance Arguments to simulate Haskell classes
as explained here:

So, I have:

  record Eq (t : Set) : Set where
    field _==_ : t → t → Bool
    _/=_ : t → t → Bool
    a /= b = not $ a == b

and the following record definition:

record A2 : Set₁ where
     A : Set
     EqA : Eq A
     a b : A
   a≠b : Bool
   a≠b =  a /= b

Agda gives an error at the last /= :
"No variable of type Eq A was found in scope".
But EqA is in the scope.  Why Agda does not consider it?

I can fix it defining an alias of EqA as an instance Eq.
The keyword instance is required.
(Continue reading)

Iain Whiteside | 21 Apr 10:56 2015

AI4FM 2015: Call for Short Contributions

AI4FM 2015 - the 6th International Workshop on
the use of AI in Formal Methods

Edinburgh, 1st September, 2015
In association with AVoCS 2015
  --- First Call for Contributions ---

Important Dates
Submission deadline: 1st August, 2015
Notification of acceptance: 10th August, 2015
Final version due: 21st August, 2015
Workshop: 1st September, 2015

This workshop will bring together researchers from formal methods, 
automated reasoning and AI; it will address the issue of how AI can 
be used to support the formal software development process, including 
requirement analysis, modelling and proof. Previous AI4FM workshops 
have included a mix of industrial and academic participants and we 
anticipate attracting a similarly diverse audience. 

Rigorous software development using formal methods allows the construction 
of an accurate characterisation of a problem domain that is firmly based 
(Continue reading)

Conor McBride | 17 Apr 10:16 2015

Strathclyde PhD Position

Applications are welcome from ANYWHERE for a Microsoft Research
sponsored PhD position in the Mathematically Structured Programming
group at the University of Strathclyde.

Project:                  Real World Data with Dependent Types:
                            Integrity and Interoperation
Strathclyde supervisor:   Dr Conor McBride
Microsoft supervisor:     Dr Don Syme
Starting:                 October 2015
Tuition fees:             fully funded or substantially subsidised,
                            depending on residency status
Stipend:                  £14,057K
Contact:                  Conor, by 8 May 2015

Project Summary

Data integrity, manipulation and analysis are key concerns in modern
software, for developers and users alike. We are often obliged to work
with a corpus of files – spreadsheets, databases, scripts – which
represent and act on aspects of data in some domain. This project
seeks to improve the integrity and efficiency with which we can
operate in such a setting by

* delivering a language for data models which expresses their
  conceptual structure, capturing what kinds of things exist in a
  given context, what data we expect to have about them, and when
  those data are consistent;

* delivering a language for data views relative to a model,
(Continue reading)

Aaron Stump | 13 Apr 23:46 2015

a puzzle about pattern matching

Dear Agda community,

For a while, I have wondered how to get Agda to understand that in a set 
of equations defining some function, the patterns in earlier equations 
must have failed to match, if we find ourselves in a later equation.  
This could save a lot of repetitious equations.  Below I have a small 
example.  It is completely self-contained (I have included the 
definitions I am using from our Iowa Agda Library). The puzzle is, can 
you prove lem in something closer to 3 equations, rather than the eight 
given?  Failing that, can you at least abstract out the eight equations 
in some reasonably modular way? The problem is that action is defined 
using default patterns, rather than explicit alternate patterns.  The 
proof of lem cannot just use default patterns, as partial evaluation of 
applications of action requires that the patterns be explicit.

While this is obviously an artificial example, I find this issue comes 
up rather frequently.


module puzzle where

{----------- start standard definitions from IAL ---------------------}

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
   refl : x ≡ x

{-# BUILTIN REFL refl #-}
(Continue reading)

N. Raghavendra | 12 Apr 21:50 2015

Implicit arguments

When defining a function or a dependent type, I'm often unsure about
which parameters can be declared as implicit.  How do I know whether the
system can infer a particular argument from the types of other
arguments?  Until now, I have been just guessing, and it hasn't been
satisfactory.  Can people describe some method of finding out which
parameters to assume as implicit?

Thanks and cheers,

N. Raghavendra <raghu@...>,
Harish-Chandra Research Institute,
Andrei Paskevich | 10 Apr 12:43 2015

Last Call for Papers, PxTP 2015

               The Fourth International Workshop on
            Proof eXchange for Theorem Proving (PxTP)


                August 2-3, 2015, Berlin, Germany

                         associated with CADE 2015

Important dates

  * Abstract submission: Thu, May 7, 2015
  * Paper submission: Thu, May 14, 2015
  * Notification: Tue, June 16, 2015
  * Camera ready versions due: Thu, June 25, 2015
  * Workshop: August 2-3, 2015


  The PxTP workshop brings together researchers working on various aspects
  of communication, integration, and cooperation between reasoning systems
  and formalisms.

  The progress in computer-aided reasoning, both automated and interactive,
  during the past decades, made it possible to build deduction tools that
  are increasingly more applicable to a wider range of problems and are
  able to tackle larger problems progressively faster. In recent years,
  cooperation of such tools in larger verification environments has
  demonstrated the potential to reduce the amount of manual intervention.
  Examples include the Sledgehammer tool providing an interface between
(Continue reading)

Andrés Sicard-Ramírez | 9 Apr 17:49 2015

Positive but not strictly positive types


Retaking the discussion in, it's known that
using *negative* types it's possible

a) to prove absurdity or
b) to write non-terminating terms.

Is there some example in *Agda* of a positive but not strictly
positive type which allows a) or b)?