CodeSprints

AIM XV Discussions and Code Sprint Suggestions

Agda Language

• Dominique, Andreas, Steven: Strengthening Dominique's instance inference

Mo: started, printing type of FindInScope metas
Tu: instance arguments now allow hidden arguments to be solved by unification
     better error message if instance could not be found
     working on bug: instance search does not find things it should
     TODO: more regression test cases to secure features
We: More or less the same as yesterday. Regression test failing.
Fr: Optimizations: Significantly faster (better constraint economics).
    Memoizes lists of candidates.  Works well for Agda Prelude now.

• Nisse, Andreas, Peter II: Optimizing Agda (positivity graph...)

Mo (Nisse): optimizing transitive closure algo in positivity checker
Tu: 1) tc runs on sccs now
    2) pos check not run twice on same code 
    result: 25% heap space reduction on standard library
We: Trying to make "open M x using (y)" not create useless things.
Fr: Gave up on this for now.

• Nisse, Andreas, Peter I, Thorsten, Ambrus, Ramana, Peter II: Discussing improved treatment of coinduction (mixed induction)

Fr: (Thorsten, Nisse, Andreas, Ramana): 
   Discussion about sized types represented in Martin-Loef Type Theory.
   Thorsten: possible to have a cut down version very soon? (cf. universe levels)

• Andreas, Nisse, James: Discussion: Shadowing

Tu: Discussion, but no conclusion.

• Thorsten, Andreas: Smart case (Extend definitional equality): Clarify efficiency
• Ramana, Thorsten: Discussion: Flexible rewrite. Improve reflection: quoting the context.

Fr: Ramana: demo on issues with current rewrite.  Want magic tactics!!

• James, Thorsten, Andreas, Nisse, Ramana, Peter I, Bengt: Destructor patterns
• Andreas: Pattern-matching definitions of functions with varying arity
• James, Makoto: Change Agda internal syntax: preserving and printing back let-expressions; Proper functions in let

Mo (Makoto): put let-declarations into unnamed module?
Fr (Makoto): Plan: let decls in e  --> module decls; e  (similar to module of where clauses)
    Unclear: where to put the anonymous module?
    Nisse: Problems with generativity (because new module for each let)?

• Do notation for Agda; integrate pattern matching lambdas and syntax facility

We: (Removed)

• Dominique, Andreas: User-defined type errors

We: Discussion done. Whether to normalise things in error messages or not etc.
    Idea not finished or ready for implementation.

Agda Interaction

• Peter II, Paul, James, Stephan, Thorsten, Frederic, Ambrus, Ramana, Nisse, Guilhem: Agda API and Agda in a Browser on a Server

 
Mo API (Ramana, Paul, Stephan): started, thinking about design
Tu: Main uses: JavaScript web interaction (ViM interaction abandoned)
We: JS guys are tryingo talk directly to ghci, similarly to the current GhciTop.
Fr: Peter II: Refactoring GhciTop: creating functions that do not use global state, 
    but return result of function or print on standard output.

• Peter II, Ambrus: Agda in a Browser (Source Code)

Mo Browser (Peter II, Ambrus): Installing web backend for Haskell
Tu: processes literate Agda files, support for LaTeX, graphs
    syntax highlighting for Agda; fake comments to hide Agda lines: enables exercises
    open source (on github)
We: For exercise forms, proposed solutions are now written out to separte files
    and sent to the stub of a server. (Demo)
    How to construct an exercise form: write "H>" after a code block.
      \begin{code}
      _\/_ : Bool -> Bool
      true \/ y = true
      false \/ y = y
      \end{code}
      H>
    Type signature is displayed, def clauses are hidden and replaced by
    empty editing area.

    The solution file is constructed thus
      open import hiding (_\/_)
      ... original type sig ...
      ... student provided def clauses ...

    Will provide a documentation.

    JC: Can a solution depend on other solutions to the previous exercises?
Fr: Demo: Type checking works in browser.

• Stephan

Tu: adapting JavaScript code editor for Agda (for interactive editing)
We: trying to talk directly to ghci, similarly to the current GhciTop.
Fr: Fixed unicode issues, waiting for Peter II's refactoring.

• Guilhem, Nisse: Improving the emacs interface

Mo Guilhem: working on dynamic highlighting
   (Thorsten says: animated type checking slow on Aquamacs)
Tu: feature request was: blocks properly highlighted during typechecking
We: Reported a bug on Aquamacs with minimal example.
    Problem: too slow printing to a buffer. Trying to fix it with config, or a patch.
Fr: Efficiency bug (on cocoa platform) persists, trying to narrow it down.
    More highlighting info.

Agda Tools

• James, Ramana: Nightly build (like coq-bench)

Fr: James, Guilhem: working on bash script.  Run tests/benchs and record performance.
    Andres: NixOS has large build facility for Haskell. Includes test suites.

• Paul, Andres?, Nisse: Cabal for Agda
• Makoto, Ramana: Windows installer for Agda

We: Started. 
Fr: Makoto: Worked on two platforms (Window XP)!!

Documenting Agda

• James, Ramana: Write a reference manual by raiding the release notes

 
Mo (James): Manual is less outdated than expected.  
   Added bits of release notes (pattern matching lambdas...)
Tu (Ramana, Paul, Thorsten): New structure for reference manual
We: Reference manual. Started another one in tex rather than wiki.
    Still twiddling TOC.
    There's an issue with wiki unicode handling etc.,
    but updatable ref is most desirable. -> Fix the wiki problem
    (but^2 tex is better for displaying inference rules...)

    MediaWiki? A new plugin to wiki?(but don't want to dependent on Chalmers dator ppl)?

    Heading towards "specification". -> generally a good idea, but too early to have Agda 2012.
    Txa: Gathering info is more important now than polishing.
    Collect info from release notes. -> Done?
Fr: James: Merged new and old version and TeX.  
    Main page has new structure, old content is being ported.
    Guilhem: page for X-compose. (Relocate, because not only for emacs.)

• Ambrus and Peter II, Stephan, Frederik: Online tutorial. Without requiring much background information.
• James, Andreas: User contributions

Small set of polished examples. Maintained. Current examples are not models of good practice.

• Peter I, Bengt, Andreas, Thorsten, Yoshiki, Ambrus, Ramana, Nisse, Makoto: Reconstructing Agda from Martin-Loef Type Theory; Agda core language

Mo (Peter): Revisiting the notes from last meeting. What next? 
  Introduction to notations of dependently typed lambda-calculus 
    (typed and untyped lambda-abstraction, telescopes etc.).
  Declarations and definitions.
  Datatypes.
  Recursion.
We: Andreas' talk & ensuing discussion on 
    Subtyping. Type first or elem first, new philosophy on TT?

• Yoshiki: Documenting Unicode Input

We: done by Nisse and Paul -> on the Wiki.

Using Agda

• Yoshiki, Peter I, Thorsten, James: Coding Catoids (Category based on Setoids) [Yoneda is done, next project: Enriched or Bi-categories]

Mo (Yoshiki, James, Thorsten, Peter I): validated formalization of Yoneda for catoids 
   TODO: cat. of eq. rel. and of PERs.  Investigate equivalence of E-cats and P-cats.
We: Comments on the NBE proof in Agda are reflected. Thinking on the next move now.
Fr: Yoshiki: Generalization of currying (for n-ary functors).  Specification in progress.

• Thorsten, Nisse, James: new project to implement quotients. See Quotient.agda

and Qtest.agda.

We: Started.
      data Quotient{c l}(A : Setoid c l) : Set (c cup l)
        box : (x : Setoid.Carrier A) -> Quotient A
        -- a private constructor, not to be matched on by users.
      postulate
        [_]-cong :"related elems are equal when boxed"

      elim : ...
      elim P f _ (box f) x = f x
      rec : ...
      rec P = ... 
    Example: Integer by quotienting.
    Turns a setoid into a set.  So e.g. Cat can be defined just using Set.

    There should be more to say about proof-irrelevant quotient.
Fr: Test case works: negation . negation = id. 

• (Makoto: Relating the way formal theories are revised with "argumentation")
• Thorsten, James, Steven, Peter I, Dominique, Guilhem, Ramana: Type theory in type theory (Strongly typed syntax)

Tu (James, Thorsten): started total syntax of TT (following Harper/Licata)
Fr: continuing, on github at https://github.com/jmchapman/TT-in-TT

• Heinrich, Vivek: Agda exercise session (e.g. Ulf's tutorial, James' course, Andres' .., Conor's ...)

We: Nisse sent XX to YY

• Frederik, Ambrus, Dominique: Work on Agda prelude

Fr: Type classes work now. Fast due to Dominique's improvements to instance search.
    Thinking about IO "monad" (corecursion).  Partiality monad is similar.
    IO monad does not fit in monad structure (size, coinduction).  Relative monad?

• Fr: Discussion about views (Ex: unary and binary numbers, eliminators a la Epigram). Code about views on http://github.com/xrchz/agda-hacking