Nicolas Wu | 23 Jul 11:44 2014
Picon
Picon

ICFP Programming Contest 2014

=====================================================================
                      Call for Participation

                The 17th ICFP Programming Contest

                    http://www.icfpcontest.org
                 Friday 25 July 2014 at 12:00 UTC
=====================================================================

The ICFP Programming Contest 2014 is starting at the end of this week!

It's nearly time to roll up your sleeves, and gain fame and glory for your
programming language of choice: prepare for sleepless nights and hours of fun!

The full details of the contest specification will appear on the contest
website at http://www.icfpcontest.org on Friday 25 July 2014 at 12:00 UTC.
No registration is required: just roll up and have some fun!

For more announcements, stay tuned on our twitter feed at:

https://twitter.com/icfpcontest2014

Good luck to all participants,

Nicolas Wu
Dan Krejsa | 21 Jul 23:53 2014
Picon

Re: Re: Data.Vec toList - fromList isomorphism

Hi,

The _=v=_ version of equality that I introduced, and the awkward 'transfer' use, turn
out not to be needed if one maps between List A and Σ ℕ (λ n -> Vec A n):

listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
listToVec [] = ℕ.zero , []
listToVec (x ∷ l) = let (n , v) = listToVec l in ℕ.suc n , x ∷ v

vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
vecToList (.ℕ.zero , []) = []
vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)

L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
L-V-L [] = refl
L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)

V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) ≡ v
V-L-V (.ℕ.zero , []) = refl
V-L-V (ℕ.suc n  , x ∷ v) with listToVec (vecToList (n , v)) | V-L-V (n , v)
V-L-V (ℕ.suc n , x ∷ v) | .n , .v | refl = refl

Figuring out how to get the equality working on the Σ type was a bit tricky for me.

- Dan



On Sun, Jul 20, 2014 at 12:44 PM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Thanks, Ulf!

In my actual application I'm using (Fin n -> A) to represent the vectors (since I want
to look at permutations / bijections of Fin n), but I may take a similar approach to
what you do above.

Also, I'll take a look at agda-prelude.
The main awkwardness I think is the need to resort to 'transport' at all, but
maybe that's unavoidable if I'm trying to get a propositional equality (at
least pointwise for Fin n -> A) rather than being content with something like VecEq.

- Dan

P.S. It may also help to extend the toList / fromList mappings to non-dependent
mappings between (List A) and Σ ℕ (λ n -> Vec A n), and maybe hide the
nasty 'transport' inside an appropriate equality operator on Σ ℕ (λ n -> Vec A n),
maybe something like this:

listToVec : ∀ {i} {A : Set i} -> List A -> Σ ℕ (λ n -> Vec A n)
listToVec [] = ℕ.zero , []
listToVec (x ∷ l) =
    let (n , v) = listToVec l
    in ℕ.suc n , x ∷ v

vecToList : ∀ {i} {A : Set i} -> Σ ℕ (λ n -> Vec A n) -> List A
vecToList (.0 , []) = []
vecToList (.(ℕ.suc _) , x ∷ v) = x ∷ vecToList (_ , v)

L-V-L : ∀ {i} {A : Set i} -> (l : List A) -> vecToList (listToVec l) ≡ l
L-V-L [] = refl
L-V-L (x ∷ l) = cong (_∷_ x) (L-V-L l)

infix 2 _=v=_

_=v=_ : ∀ {i} {A : Set i} -> (v w : Σ ℕ (λ n -> Vec A n)) -> Set i
_=v=_ {A = A} (n , v) (m , w) = Σ (n ≡ m) (λ n≡m -> transport (Vec A) n≡m v ≡ w)

_∷'_ : ∀ {i} {A : Set i} -> A ->  Σ ℕ (λ n -> Vec A n) ->  Σ ℕ (λ n -> Vec A n)
x ∷' (n , v) = ℕ.suc n , x ∷ v

=v=cons : ∀ {i} {A : Set i} {v w : Σ ℕ (λ n -> Vec A n)} (a : A) -> v =v= w -> a ∷' v =v= a ∷' w
=v=cons {v = n , v} {.n , w} a (refl , tv=w) = refl , cong (_∷_ a) tv=w

V-L-V : ∀ {i} {A : Set i} -> (v : Σ ℕ (λ n -> Vec A n)) -> listToVec (vecToList v) =v= v
V-L-V (.0 , []) = refl , refl
V-L-V (ℕ.suc n  , x ∷ v) = =v=cons x (V-L-V (n , v))





On Sun, Jul 20, 2014 at 1:19 AM, Ulf Norell <ulf.norell <at> gmail.com> wrote:
Not sure if you find this less awkward, but here is a different, slightly less ad-hoc, approach (using my prelude library [1] rather than the standard library).

open import Prelude

-- Heterogenous equality on vectors --

VecEq : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) → Set a
VecEq []       []       = ⊤′
VecEq []       (x ∷ ys) = ⊥′
VecEq (x ∷ xs) []       = ⊥′
VecEq (x ∷ xs) (y ∷ ys) = x ≡ y × VecEq xs ys

-- If vectors are equal then the lengths are equal
vecEq-len : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) →
              VecEq xs ys → n ≡ m
vecEq-len [] [] heq = refl
vecEq-len [] (x ∷ ys) ()
vecEq-len (x ∷ xs) [] ()
vecEq-len (_ ∷ xs) (_ ∷ ys) (_ , heq) =
  cong suc (vecEq-len xs ys heq)

-- VecEq xs ys implies transport xs ≡ ys
vecEq-≡ : ∀ {a} {A : Set a} {n m} (xs : Vec A n) (ys : Vec A m) (n=m : n ≡ m) →
            VecEq xs ys → transport (Vec A) n=m xs ≡ ys
vecEq-≡ [] [] refl heq = refl
vecEq-≡ (x ∷ xs) (.x ∷ ys) refl (refl , heq) =
  cong (_∷_ x) (vecEq-≡ xs ys refl heq)

-- Vec to List round-trip --

-- This proof is super-easy
v-l-v′ : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
           VecEq (listToVec (vecToList xs)) xs
v-l-v′ []       = _
v-l-v′ (x ∷ xs) = refl , v-l-v′ xs

-- We can get the original theorem from the VecEq lemmas
lentoList : ∀ {a} {A : Set a} {n} (xs : Vec A n) → length (vecToList xs) ≡ n
lentoList xs = vecEq-len (listToVec (vecToList xs)) xs (v-l-v′ xs)

v-l-v : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
        transport (Vec A) (lentoList xs) (listToVec (vecToList xs)) ≡ xs
v-l-v xs = vecEq-≡ (listToVec (vecToList xs)) xs (lentoList xs) (v-l-v′ xs)

/ Ulf



On Sun, Jul 20, 2014 at 3:22 AM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Hi,

I figured out a proof for v-l-v using a lemma transLenSuc,

-----
transLenSuc :  ∀ {i} {A : Set i} {n m : ℕ} -> (p : n ≡ m) -> (a : A) -> (v : Vec A n)
     -> transLen (cong ℕ.suc p) (a ∷ v) ≡ a ∷ transLen p v
transLenSuc refl a v = refl


v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) = trans (transLenSuc (lentoList v) x (fromList (toList v))) (cong (_∷_ x) (v-l-v v))
-----

but the approach still seems kind of awkard, so suggestions still appreciated.

- Dan



On Sat, Jul 19, 2014 at 4:37 PM, Dan Krejsa <dan.krejsa-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org> wrote:
Hi,

It's pretty clear that the toList and fromList functions in Data.Vec are in some
sense inverses.  One direction is easy to show:

l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l
l-v-l [] = refl
l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)

In the other direction my first naive attempt

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v
v-l-v v = ?

fails with Agda complaining about (fromList (toList v) ≡ v) since equality is
homogeneous and

   fromList (toList v)

has type

  Vec A (length (toList v))

which is not judgementally equal to the type of v, which is (Vec A n),
although that equality is easy to show propositionally:

lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n
lentoList [] = refl
lentoList (x ∷ v) = cong ℕ.suc (lentoList v)

My next attempt was to try to use the equality (lentoList v) as a 'cast' to convert the type of fromList (toList v)

transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x -> B y
transport B refl = id

transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m
transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) with lentoList v
... | eq = {! !}

but I didn't get much further since Agda does not want to case on 'eq' as a pattern
variable turning it into refl.

My guess is there's probably a standard way around this sort of problem, or
a better way to express that (fromList ∘ toList) is pointwise the same as the identity.
But I'm presently both new & rusty enough not to think of it, having done just a bit of
Agda proving in the past and having been away from it for a while...

Any hints?

- Dan


_______________________________________________
Agda mailing list
Agda-TrQ0NnR75ays1BDpvl8NfQ@public.gmane.orgmers.se
https://lists.chalmers.se/mailman/listinfo/agda




_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Dan Krejsa | 20 Jul 01:37 2014
Picon

Data.Vec toList - fromList isomorphism

Hi,

It's pretty clear that the toList and fromList functions in Data.Vec are in some
sense inverses.  One direction is easy to show:

l-v-l : ∀ {i} {A : Set i} (l : List A) -> toList (fromList l) ≡ l
l-v-l [] = refl
l-v-l (x ∷ l) = cong (λ xs → x ∷ xs) (l-v-l l)

In the other direction my first naive attempt

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> fromList (toList v) ≡ v
v-l-v v = ?

fails with Agda complaining about (fromList (toList v) ≡ v) since equality is
homogeneous and

   fromList (toList v)

has type

  Vec A (length (toList v))

which is not judgementally equal to the type of v, which is (Vec A n),
although that equality is easy to show propositionally:

lentoList : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) -> length (toList v) ≡ n
lentoList [] = refl
lentoList (x ∷ v) = cong ℕ.suc (lentoList v)

My next attempt was to try to use the equality (lentoList v) as a 'cast' to convert the type of fromList (toList v)

transport : ∀ {i j} {A : Set i} (B : A -> Set j) {x y : A} -> x ≡ y -> B x -> B y
transport B refl = id

transLen : ∀ {i} {A : Set i} {n m : ℕ} -> n ≡ m -> Vec A n -> Vec A m
transLen {A = A} n≡m v = transport (λ l -> Vec A l) n≡m v

v-l-v : ∀ {i} {A : Set i} {n : ℕ} (v : Vec A n) ->  transLen (lentoList v) (fromList (toList v)) ≡ v
v-l-v [] = refl
v-l-v (x ∷ v) with lentoList v
... | eq = {! !}

but I didn't get much further since Agda does not want to case on 'eq' as a pattern
variable turning it into refl.

My guess is there's probably a standard way around this sort of problem, or
a better way to express that (fromList ∘ toList) is pointwise the same as the identity.
But I'm presently both new & rusty enough not to think of it, having done just a bit of
Agda proving in the past and having been away from it for a while...

Any hints?

- Dan
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Christopher Jenkins | 18 Jul 17:43 2014

Strange error when trying to install Agda 2.4.0.1 from cabal

Hello all,

I recently installed Linux Mint 17 on a new computer and ran the following commands to install Agda:

# apt-get update
# apt-get install haskell-platform libncurses5-dev
# cabal update
# cabal install agda

Agda gets stuck compiling "src/full/Agda/Syntax/Position.hs" with the following error:
    Could not deduce (Num (NonNegative Integer))
      arising from a use of `arbitrary'
    from the context (Arbitrarlly a)
      bound by the instance declaration
      at src/full/Agda/Syntax/Position.hs:492:10-47

(full text of error in pastebin: http://pastebin.com/8izELMCB)

Has anyone seen this before, or is using LM17 and was able to get Agda working? My GHC is v7.6.3.

Thanks.

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Hugo Herbelin | 18 Jul 15:45 2014
Picon
Picon

CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)

Call for papers: Types for Proofs and Programs,
  post-proceedings of TYPES 2014 (open call)
----------------------------------------------

TYPES is a major forum for the presentation of research on all aspects
of type theory and its applications. The post-proceedings of TYPES
2014, which was held May 12-15 in Paris, are open to everyone, also
those who did not participate in the conference. We would like to
invite all researchers that study type systems to share their results
concerning type-based theorem proving environments or type-based
formal modelling, in particular we welcome submissions on any topic in
the following list:

 - Foundations of type theory and constructive mathematics
 - Applications of type theory
 - Dependently-typed programming
 - Industrial uses of type theory technology
 - Meta-theoretic studies of type systems
 - Proof-assistants and proof technology
 - Automation in computer-assisted reasoning
 - Links between type theory and functional programming
 - Formalising mathematics using type theory. 

Important dates
---------------

Abstract submission deadline:   1 September 2014
Paper submission deadline:      8 September 2014
Notification of acceptance:    15 February  2015

Details
-------

* Papers must be submitted in PDF format using EasyChair:
  "https://www.easychair.org/conferences/?conf=types14postproceedings".

* Authors have the option to include an attachment (.zip or .tgz)
  containing mechanised proofs, but reviewers are not obliged to take
  these attachments into account. Attachments will not be published.

* The post-proceedings will be published in LIPIcs (Leibniz
  International Proceedings in Informatics,
  "http://www.dagstuhl.de/en/publications/lipics"), an open-access
  series of conference proceedings. Incidentally, publication of TYPES
  2013 post-proceedings is imminent as volume 26 of the LIPIcs series
  Informatics.

* We recommend to keep the length of the contributions in the range of
  15-25 pages, and 25 pages is the upper limit for the submissions.

Editors
-------

Hugo Herbelin           Inria Paris-Rocquencourt, France
Pierre Letouzey         University Paris-Diderot, France
Matthieu Sozeau         Inria Paris-Rocquencourt, France
Dan Licata | 15 Jul 21:00 2014
Picon

unification and HITs

Hi all,

I noticed an odd thing related to unification and the trick we use to implement higher inductive types with
private data types.  It's a bit worrisome but I haven't been able to prove anything wrong from it (maybe
someone else can?).  I was hoping someone would be able to explain what's going on here.  This happens in both
2.3.2.1 and the development version.  

A self-contained file with the code is here:
https://github.com/dlicata335/hott-agda/blob/master/misc/UnificationWeirdness.agda

Here's what I notice that seems wrong: Given

bad : S¹.S¹ → S¹.S¹
bad = S¹.S¹-rec S¹.base {!!}

The goal has type S1.base == S1.base (path from base to base).  If you do agda2-show-constraints, then there
is a unification constraint
?0 := id
This seems wrong to me, because there is no reason that this path should be id.  

However, I wasn't able to exploit this to prove something incorrect:

It's clearly related to the trick for HITs, because it doesn't happen if we do the same thing with a postulate
version of S1-rec, instead of with the version that reduces:
notbad1 : S¹.S¹ → S¹.S¹
notbad1 = S¹.S¹-rec-postulate S¹.base {!!}

If we write the loop in place of that goal (which unification said had to be id), then Agda accepts it:
fillbad : S¹.S¹ → S¹.S¹
fillbad = S¹.S¹-rec S¹.base S¹.loop

If there is some variable of type base=base, then the unification constraint is not generated:
notbad2 : (S¹.base == S¹.base) → S¹.S¹ → S¹.S¹
notbad2 t = S¹.S¹-rec S¹.base {!!} -- no constraint

We cannot equate S1-rec's with loop and id by unification:
notbad3 : (S¹.S¹-rec S¹.base S¹.loop) == (S¹.S¹-rec S¹.base id)
notbad3 = {!id!} -- id doesn't work

If there is something else in scope (locally) then the constraint is not generated:
l = S¹.loop
notbad4 : S¹.S¹ → S¹.S¹
notbad4 = S¹.S¹-rec S¹.base {!!} -- no constraint is generated

Any ideas about where this constraint comes from?

Thanks!
-Dan
Andreas Abel | 15 Jul 12:49 2014
Picon

Interactive copattern splitting

I created a git-branch 'splitResult' that implements copattern splitting:

* New feature: Interactively split result.

   Make case (C-c C-c) with no variables given tries to split on the
   result to introduce projection patterns.  The hole needs to be of
   record type, of course.

     test : {A B : Set} (a : A) (b : B) → A × B
     test a b = ?

   Result-splitting ? will produce the new clauses:

     proj₁ (test a b) = ?
     proj₂ (test a b) = ?

   If hole is of function type ending in a record type, the necessary
   pattern variables will be introduced before the split.  Thus, the
   same result can be obtained by starting from:

     test : {A B : Set} (a : A) (b : B) → A × B
     test = ?

It has been on my todo-list for long, but Cezar's question on DTP 
whether such a feature would be available in Idris soon made me jealous 
enough to implement it now.

Feedback welcome.

Since this feature is release-ready, I might merge it into maint-2.4.0 
for faster dissemination.  'master' contains also features that are not 
so stable and cannot be released from one day to the next.

Opinions? Ulf?

Cheers,
Andreas

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

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

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Ulf Norell | 15 Jul 12:47 2014
Picon

Re: Without-K puzzle


On Tue, Jul 15, 2014 at 11:23 AM, Matthieu Sozeau <mattam-2hFplG4jw+0dnm+yROfE0A@public.gmane.org> wrote:

I think this is not gonna be provable, as even if y = z is not inhabited, tranport p y = z,
which is the equality you get on the second components, might be. In other words, without K you might have transport p y <> y for p : x = x. An example is if p : Bool = Bool is the negation iso, B := \x. x, y := true, z := false. So you need to assume A is an HSet here, or is decidable.

Ok, that's fair. Fortunately in my case equality on A is decidable (I'm trying to lift decidable equality on A and B to decidable equality on Σ A B). How would I use that to prove the puzzle?

/ Ulf
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Ulf Norell | 15 Jul 11:07 2014
Picon

Without-K puzzle

I've been trying to define decidable equality on sigma types without K and I run into
problems in the case where the first components are equal but the second ones are
not. It boils down to solving the puzzle below, proving the contra-positive of injectivity
of _,_ in the second argument. Any without-K wizard that can give me a hand with this?

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

data Id (A : Set) (x : A) : A → Set where
  refl : Id A x x

elim-Id : {A : Set} (P : ∀ x y → Id A x y → Set) →
          (∀ x → P x x refl) →
          ∀ x y (p : Id A x y) → P x y p
elim-Id P r x .x refl = r x

puzzle : (A : Set) (B : A → Set) (x : A) (y z : B x) →
         ¬ Id (B x) y z → ¬ Id (Σ A B) (x , y) (x , z)
puzzle A B x y z neq eq = ?

/ Ulf
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andreas Abel | 12 Jul 11:03 2014
Picon

PEPM 2015 call for papers

Please consider a contribution for PEPM 2015 (Mumbai, India).  Deadline: 
9 September 2014.

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

                      ======= PEPM 2015 ===========

ACM SIGPLAN 2015 WORKSHOP ON PARTIAL EVALUATION AND PROGRAM MANIPULATION
Tue-Wed, January 13-14, 2015, Mumbai, India, co-located with POPL'15

http://conf.researchr.org/home/pepm2015

Sponsored by ACM SIGPLAN

SCOPE

The PEPM Symposium/Workshop series aims at bringing together
researchers and practitioners working in the areas of program
manipulation, partial evaluation, and program generation.  PEPM
focuses on techniques, theory, tools, and applications of analysis
and manipulation of programs.

The 2015 PEPM workshop will be based on a broad interpretation of
semantics-based program manipulation and continue last years'
successful effort to expand the scope of PEPM significantly beyond the
traditionally covered areas of partial evaluation and specialization
and include practical applications of program transformations such as
refactoring tools, and practical implementation techniques such as
rule-based transformation systems.  In addition, the scope of PEPM
covers manipulation and transformations of program and system
representations such as structural and semantic models that occur in
the context of model-driven development.  In order to reach out to
practitioners, a separate category of tool demonstration papers will
be solicited.

Topics of interest for PEPM'15 include, but are not limited to:

* Program and model manipulation techniques such as: supercompilation,
   partial evaluation, fusion, on-the-fly program adaptation, active
   libraries, program inversion, slicing, symbolic execution,
   refactoring, decompilation, and obfuscation.

* Program analysis techniques that are used to drive program/model
   manipulation  such as: abstract interpretation, termination
   checking, binding-time analysis, constraint solving, type systems,
   automated testing and test case generation.

* Techniques that treat programs/models as data objects including
   metaprogramming, generative programming, embedded domain-specific
   languages, program synthesis by sketching and inductive programming,
   staged computation, and model-driven program generation and
   transformation.

* Application of the above techniques including case studies of
   program manipulation in real-world (industrial, open-source)
   projects and software development processes, descriptions of robust
   tools capable of effectively handling realistic applications,
   benchmarking.  Examples of application domains include legacy
   program understanding and transformation, DSL implementations,
   visual languages and end-user programming, scientific computing,
   middleware frameworks and infrastructure needed for distributed and
   web-based applications, resource-limited computation, and security.

To maintain the dynamic and interactive nature of PEPM, we will
continue the category of `short papers' for tool demonstrations and
for presentations of exciting if not fully polished research, and of
interesting academic, industrial and open-source applications that are
new or unfamiliar.

Student participants with accepted papers can apply for a SIGPLAN PAC
grant to help cover travel expenses and other support. PAC also offers
other support, such as for child-care expenses during the meeting or
for travel costs for companions of SIGPLAN members with physical
disabilities, as well as for travel from locations outside of North
America and Europe. For details on the PAC programme, see its web page
at: http://www.sigplan.org/PAC.htm.

All accepted papers, short papers included, will appear in formal
proceedings published by ACM Press.  Accepted papers will be included
in the ACM Digital Library.  Following the practice of recent PEPMs,
we are planning a special issue of a journal for a selection of papers
presented at the PEPM'15 workshop.

PEPM has also established a Best Paper award.  The winner will be
announced at the workshop.

SUBMISSION CATEGORIES AND GUIDELINES

Regular Research Papers must not exceed 12 pages in ACM Proceedings
style (including appendix).  Tool demonstration papers and short papers
must not exceed 6 pages in ACM Proceedings style (including appendix).
At least one author of each accepted contribution must attend the
workshop and present the work.  In the case of tool demonstration
papers, a live demonstration of the described tool is expected.
Suggested topics, evaluation criteria, and writing guidelines for both
research tool demonstration papers will be made available on the
PEPM'15 Web-site soon.  Papers should be submitted electronically via
the workshop web site.

Authors using LaTeX to prepare their submissions should use the new
improved SIGPLAN proceedings style (sigplanconf.cls, 9pt template)
available at: http://www.sigplan.org/Resources/Author.

IMPORTANT DATES

     Abstract submission: Tue, September 9, 2014
     Paper submission: Fri, September 12, 2014 (*FIRM*)
     Author notification: Mon, October 13, 2014
     Workshop: Tue, January 13 and Wed, January 14, 2015

Note: The paper submission deadline is firm.  Because the VISA
application to India can take a long time, all the schedule is set
earlier than previous years.  The above schedule is tight: we have
absolutely no time to wait for late submissions and we will have no
deadline extension.  So, please plan ahead.

INVITED SPEAKERS

     to be announced

PROGRAM CHAIRS

     Kenichi Asai (Ochanomizu University, Japan)
     Kostis Sagonas (Uppsala University, Sweden / NTUA, Greece)

PROGRAM COMMITTEE

     Andreas Abel (Chalmers and Gothenburg University, Sweden)
     Elvira Albert (Complutense University of Madrid, Spain)
     Malgorzata Biernacka (University of Wroclaw, Poland)
     Matthias Blume (Google, USA)
     Cristiano Calcagno (Facebook, UK)
     Jacques Carette (McMaster University, Canada)
     Jeremy Gibbons (University of Oxford, UK)
     Nao Hirokawa (Japan Advanced Institute of Science and Technology, 
Japan)
     Atsushi Igarashi (Kyoto University, Japan)
     Andrei Klimov (Russian Academy of Sciences, Russia)
     Michael Leuschel (University of Dusseldorf, Germany)
     Sam Lindley (University of Edinburgh, UK)
     Michal Moskal (Microsoft Research, USA)
     Keiko Nakata (Tallinn University of Technology, Estonia)
     Jeremy Siek (Indiana University, USA)
     Peter Thiemann (University of Freiburg, Germany)
     Janis Voigtlaender (University of Bonn, Germany)
     Kwangkeun Yi (Seoul National University, South Korea)
     Tetsuo Yokoyama (Nanzan University, Japan)

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

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

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Guillaume Brunerie | 11 Jul 12:26 2014
Picon

Recursive instance search

Hello all,

As some of you know, I started working on recursive instance search
during the previous AIM and the code is now available on my GitHub
here : https://github.com/guillaumebrunerie/agda (should I open a pull
request against the official Agda?)

The main outstanding issue is that there is no termination check yet
so if you’re not careful when defining your instances you can easily
make Agda loop.
Also, I haven’t really thought about namespace management, for
instance 'hiding' does not hide instances (but serialization should
work, though).

I copy-pasted the relevant part of the CHANGELOG below (I borrowed
part of the text in issue 938) and you can also look at the two files
test/succeed/RecursiveInstanceSearch{,Level}.agda to see some more
advanced examples of recursive instance search.

Of course I welcome any feedback/bug reports.

Cheers,
Guillaume

* Instance search is now more efficient and recursive (see issue 938)
  (but without termination check yet)

  A new keyword `instance' has been introduced (in the style of
  `abstract' and  `private') which must now be used for every
  definition/postulate that has to be taken into account during instance
  resolution. For example:

    {-# OPTIONS --copatterns #-}

    record RawMonoid (A : Set) : Set where
      field
        nil  : A
        _++_ : A -> A -> A
    open RawMonoid

    instance
      rawMonoidList : {A : Set} -> RawMonoid (List A)
      rawMonoidList = record { nil = []; _++_ = List._++_ }

      -- using copatterns to define this recursive instance:

      rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
      nil rawMonoidMaybe = nothing
      _++_ rawMonoidMaybe nothing mb = mb
      _++_ rawMonoidMaybe ma nothing = ma
      _++_ (rawMonoidMaybe {{m}}) (just a) (just b) = just (_++_ m a b)

  Moreover, each type of an instance must end in (something that reduces
  to) a named type (e.g. a record, a datatype or a postulate). This
  allows us to build a simple index structure

    data/record name  -->  possible instances

  that speeds up instance search.

  Instance search takes into account all local bindings and all global
  'instance' bindings and the search is recursive. For instance,
  searching for

    ? : RawMonoid (Maybe (List A))

  will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to
  unify the first one, succeeding with the second one

    ? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))

  and continue with goal

    ?m : RawMonoid (List A)

  This will then find

    ?m = rawMonoidList {A = A}

  and putting together we have the solution.

  Be careful that there is no termination check for now, you can easily
  make Agda loop by declaring the identity function as an instance. But
  it shouldn’t be possible to make Agda loop by only declaring
  structurally recursive instances (whatever that means).

  Additionally:

  * Uniqueness of instances is up to definitional equality (see issue 899)

  * Instance search will not be attempted if there are unsolved metas in
    the goal. The issue is that trying to typecheck [? ++ ?] would
    generate a constraint of type `RawMonoid ?' to be solved by instance
    search, but unification with `rawMonoidMaybe' will succeed and
    generate a new constraint of type `RawMonoid ?2' to be solved by
    instance search, and so on, so Agda would loop.

    As a special case, if none of the instances declared for that type
    is recursive, then instance search is attempted as usual even if
    there are unsolved metas (no risk of looping here).

  * Instances of the following form are allowed:

        Π-level : {n : ℕ} {A : Set} {B : A → Set}
                  {{_ : (a : A) → has-level n (B a)}}
                  → has-level n ((a : A) → B a)

      When searching recursively for an instance of type `(a : A) →
      has-level n (B a)', a lambda will automatically be introduced and
      instance search will search for something of type `has-level n (B
      a)' in the context extended by `a : A'.

  * There is no longer any attempt to solve irrelevant metas by instance
    search

  * Constructors of records and datatypes are automatically added to the
    instance table

Gmane