Main /
\ Main

The 10th Agda Implementors' Meeting

Göteborg, September 14-18, 2009

Talk overview

Detailed programme + discussion + code sprint notes is further down.

Program and notes

Sunday

13.00-?
Excursion in Slottsskogen and the Botanical garden

We will meet at Cafe Marmelad http://tinyurl.com/marmelad for lunch and then walk to the Botanical Garden through Slottskogen. You can get to Marmelad by taking tram nr 3 or 11 from the Central station to Mariaplan. Everything will be very informal, no registration, no fees. You have to pay your own expenses. Everybody is welcome!

Monday

9:00-10:00
Coffee and Registration

10:00-12:10
Talks in EL41

  • 10:00-10:40: Ulf Norell - Dependently typed database queries
  • 10:45-11:25: Wouter Swierstra - The Dutch National Flag problem
  • 11:30-12:10: Fredrik Lindblad - Agsy for current Agda

12:30-14:00
Lunch 14:00-17:00

  • 14.00 Meta Discussion Peter as the Dictator
  • Discussion Topics
    • Definitional Equality
    • Universe Polymorphism (Thierry / Darin)
    • Brain-storming
    • Future of Agda
  • CodeSprint topics
    • Documentation (Bengt) Peter, Yoshiki, Darin
      • user-manual
      • update download instruction
      • wiki overhall
    • Source-code documentation (Anton)
      • High level review
    • Eta equality (Andreas, Ulf, Kato) Changing equality checking.
    • Avoiding inspect; "with-eq" (Thorsten, Ulf, Kato)
    • External tools, SAT solver (Anton, Makoto) Anton, Makoto
    • Package management (Darin) Darin, Ulf
    • Agda Programming Thorsten, Darin
      • IO library for interactive programs (Anton) Anton, Darin
      • Library for finite types (Thorsten) Thorsten, Thierry, Bengt, Peter, Anton
    • Agsy (Fredrik)

17:00 - Daily report

  • Documentation: Discussion on downloading page. Cabal should be explained, including the prerequisite for it. A single page for downloading. Recommendation for emacs versions. The standard recommendation: download GHC and use cabal; plus info for those without Haskell platform. One click installer (on windows) should be made more prominent. Page organization: "Get this version of Haskell platform and type in this and this" + "trouble shooting FAQ". Out-of-date complex instruction page should be removed?(but helpful for some.)
    Darin will do some rewrite.
    Also talked about the reference manual.
  • Ulf Finite type. TrustMe. (trustme 0 0 ---> refl, trustme 0 1 ---> don't reduce). Useful to get refl from boolean equality on string.
  • Andreas: Started on eta on mini-Agda. Will talk about it tomorrow.
  • Inspect: Nothing.
  • External tools, IO lib : tomorrow.
  • package mgmt : just started.
  • Thosten: Finite types from list of strings. Products etc for finite types.
  • Fredrik: Completed the feature needed for dump(?), working on other problems.

Tuesday

9:00-12:30
Talks and discussions in ES61

12:30-14:00
Lunch

14:00-17:00
Code Sprints

  • Daily Discussion
    • Time for Universe Polymorphism and XXX decided by Peter.
    • Wednesday Starting Time 9.00 SHARP.
    • Documentation:
      • Bengt: Improvements on Wiki pages.
      • Darin: No.
      • Wouter: Page comparing Coq and Agda, feed back wanted.
  • Eta: Discussion on Observational Equality. Thorsten's PLDT paper. Implementation looks like a lot of work. Interaction with pattern matching and inductive families is difficult.
    Discussion on implementing Andreas' talk for equality.
  • external tool : Nothing
  • interactive IO library : (Anton, last night) some library implementation. need integrating to the Std Lib.
  • package mgmt : Darin. Three parts. 1. make cabal Agda-aware 2. Command line tool for manipulating Agda-package , 3. Making Agda aware of Agda-packages
  • Finite types : Thorsten. Reorganizing the yesterday's work. Enumeration type out of list of string. Utilizing '_' of Agda to automating decidable part. Connecting it with more fundamental inductive defs of finite type?
  • Agsy : (fredrik not present.) Thorsten: Maybe the group needs someone else. Ulf: did some testing.

Wednesday

9:00-12:30
Talks and discussions in ES61

  • 9:00-9:40: Thorsten Altenkirch - Mixed Induction/Coinduction
  • 9:45-10:25: Makoto Takeyama - Integrated Verification using Agda Compiler
  • 10:25-10:45: Coffee break
  • 10:45-12:30: Discussion on the future of Agda (discussion leader Peter) Chair : Peter.
  • Topics
    • Extensions of Agda
    • Compiler for Agda
    • External Tools
    • Stability of system Documentation of change. Release notes
    • KY: Statbility discussion and Improvement discussion should be separate. Ulf: Backward compatibility for Agda is impossible. Can only offer the choice of stick with older version or not. Darin: trying to make the location of lib etc. transparent. Anton: Conflict btw developers and users. 
          Developers should have more sensitivity for user needs.
   Thorsten: Distinguishing stable and experimental features.
   Darin: Agda should have options to enable/disable features.

   KY: Another problem: unicode.
   MT: matter of education? quail-show-key
   Anton: It is also a matter of coding standard.
   X: there are tools for unicode (listing similar gryph etc.)
      U: Guidlines for library writers.

   MT: Long identifier.
   Anton: Can agree on a convention to use dash
   Anton: Another convention matter: Capitalising name for Set value.

   KY: Collecting the Agda-specific reasoning styles.
   Peter: There is some in tutorials.

   Peter: What's the resposnses of Japanese engineers?
   KY: VDM was easily learned.  Agda not.
   Ulf: It's a matter of what is lacking in tutorial.

   Patrik: Logic in CS course is not using Agda.  We should find out why.
   Thierry: Nothing to with Agda per se, but because students tend to use
   any tool in a blind way.
   Anton: My experience in using Agda in teaching gave me a lot of
   insight in Agda systems. John Tucker(?) encouraged the use of Agda
   instead of mature Coq, to which I'm grateful.

   Thorsten: Using both Coq and Agda in teaching.  It's a myth that
   downloading Coq is easy.

   Anton: Students and Agda: got positive comments.  Good for making them
   do proofs without them realising it.  Agda brings theorem proving
   closer to CS students.  Generally, no negative experience.  Still,
   Agda is immature.  May be Eclipse interface is good.

   Ulf: Going back to engineers' difficulties,  collect them and write them down.
   incorporate them to tutorials.

   KY: Need them in Japanese.

   Anton: Unicode caused a printing problem.  Good latex connection wanted.
   Ulf:  Go through HTML printing. Agda-to-HTML conversion works well.
  • Peter: "moving on, ..." Peter: let's have a contest on most wanted features.
  • Universe polymorphism KY: necessary in practical terms? You don't use Set100. Patrik: Code duplication is a problem in practice. Thorsten: Reflection etc. may change the style.
    VOTE: Darin
  • Observational Equality, proof irrelevance
  • Connection with External tools VOTE: Anton
  • IO library
  • Smart case
  • lifting restriction on "let"
  • emacs-command for "with-creation"
  • support for reflection
  • meta-programming support, cf template haskell. data type of terms, data type of types, good for writing tactics in Agda.
  • Core language good for meta-theory, meta-programming, compiler, stability
  • User defined extension.
  • Induction-Recursion unnecessarily restricted.
  • the problem of dependent elimination from codata is not resolved by the current restriction.
  • Warning for 'Tainted by X'( using postulate? using extra features? ) produced by a top level tool.
  • Extensible termination checker.
  • Peter: "Moving on,..." Compiler Anton: good if agda compiled function can be used for Agda extension / tool connection.
  • Patrik: Most important: Who will be working on Agda. <<didn't catch: about the US project>> Th: Pitts is using Agda. It's spreading. Patrik: Core language could me made common with them. Peter: Their idea of Haskell + dependency may be a bit different ...
    Anton: Opening up Agda development - in view of lack of Swedish funding. Needs more core developer. Better interface for tool-connection programming etc. Looking at GHC, Coq, ...
    Ulf etc: not really that many core development.

12:30-14:00
Lunch

14:00-17:00
Code Sprints

  • 17.00 Discussion
  • Andreas: Started on Unsound Incomplete Termination Checker with Thorsten's suggestion. <discussion on mu-nu types> Hard to salvage the termination checker as it is. Untyped approach is the relic of old times anyway.
  • Thorsten: Tried on categorical properties on Stream, and got stuck. Shouldn't be difficult, just need ideas on something like inspect patterns. <discussion on semantics of termination checking in term of suspension XXX>
  • Darin: cabal stuff. discussion with Ulf on meta-programming etc.
  • Ulf: Gave a talk on implementing semantics for boolean language to Students. Discussion with Darin and Thorsten.
  • Anton & Makoto & Peter Discussed buildIn. First steps: move the primitives related data in TCM state. Consolidates haskell files to be changed in one place. <discussion on how to guarantee the correct correspondence between Agda version and native-version of a function. Without such check, it's too easy to crash type checker.> < Would be too unfortunate if everyone extended Agda in his own way.>
  • Bengt / Yoshiki Doc group has not been active today.
  • Yoshiki Kato rescue mission. Addicted to Formalising Landau's book in Agda. Stuck at arithmetics on binary numbers. <Putting up the problems or the whole book on Wiki?>
  • Peter: RE suggestion to Andreas Sicard. <Can start preparing data types for FOL.> <Ulf: magic function Set -> FOL is hopeless. reflection is so much better>

Thursday

9:00-12:00
Talks and discussions in the EDIT-room

  • 9:00-9:40: Thierry Coquand - The FORMATH project
  • 9:45-10:25: Darin Morrison - Cabal support for Agda
  • 10:25-10:55: Coffee break
  • 10:55-12:00: Discussion on organisation of Agda libraries and contributions (discussion leader Ulf)
  • 12:00-12:30: Discussion on universe polymorphism (discussion leaders Thierry and Darin)

12:30-14:00
Lunch

14:00-17:00
Code Sprints

  • Discussion
  • Ulf:
    • Ulf & Makoto & Anton : discussion on primitives & builtin. Streamline the entangled implementation. Now aiming at allowing separate compilation of extensions.
    • Ulf & Andreas: Termination checking with mixed ind-coind. Difficulties in distinguishing good cases and bad cases. Type-based checking. Need to find out the order in which nesting of data-codata occurs.
    • Ulf & X Universe polymorphism
  • Ana:
  • Darin: making various comments, a bit more on cabal stuff.
  • Thorsten: Thorsten & Thierry, properties of new def of finite types. Harder than guessed. "set is finite if taking one element eventually exhaust it." Accessibility-like definition. "X is finite if (x : X)-> (X setminus x) is finite." Hoped to make a better way to deal with, eg, reachability analysis. Question: Is not-not of this equivalent to standard? - not answered yet.
  • Patrik: Talking with ppl, a little hacking.
  • Phillip: Trying on Agsy. Agsy as Test case generator. Wanted test cases satisfying certain properties but then Agsy tries to generate proofs, and Agsy hits bugs. <Ulf: used Agsy in a lecture(Types in programming ...) on operational semantics. connecting big-step and small-step.>
  • Yoshiki: Continued formalising Landau book. Noticed most reasoning is equational. Getting into Ordering. Trying to have an ordering version of EqReasoning. <Ulf: You can use EqReasoning.>
  • Bengt: Changing documentation.
  • Makoto: See Ulf & Anton & Makoto. Finding out how to separate references to the three builtin related modules.
  • Anton: Notes about mixed induction coinduction. mailed it to interested parties. Tomorrow, cleaning up IO library.
  • Kato-san: Continued on Java implementation stuff.
  • Ulf again: Universe polymorphism. Thorsten's suggestion being implemented. Works for List. Technical difficulty for IO.
  • Peter: Changes to documentation. Refined Wouter's page comparing Coq and Agda. <good to have short examples for comparison>
  • Ulf again: Even more universe polymorphism

19:30-21:30
Workshop dinner at Le village http://www.levillage.se/

Friday

  • 9:00-9:40: Norio Kato - A new implementation of Agda written in Java

9:40-12:30
Code Sprints in the EDIT-room

12:30-14:00
Lunch

14:00-15:00
Code Sprints (EDIT room)

15:00-16:00
Final evaluation discussion about this meeting. (EDIT room -> moved to 6128)

  • Common agreement: It is better to concentrate the code sprints to the final part of the meeting. It is difficult to mix lectures and code sprints in the way we did.
  • Next Meeting
  • Individual summary
    • Makoto: Moved 3 files to one place.... Maybe CodeSprint should have been topics fixed beforehand. <Thorsten, Ulf: The main thing is to talk to ppl. Get things done is not.> <Andreas: More contiguous time should be allocated to CodeSprint, like concentrating talks.> <CodeSprint in the morning?> <Talk-day and Sprint-day organization is better.>
    • Thierry: Talks were interesting. Talk-day should come first.
      • More work on Finite Sets. (all x0 x1 ... exist i < j . R xi xj)
        Noetherian <===> equality is well quasi-order
        Weak def suited for TT.
    • Darin: More cabal stuff.
    • Wouter: Comparison page (vs Coq). Bruno gave reaction.
    • Andreas: Implementing Eta-expansion for Mini-Agda, not finished.
    • Anton: Nealy finishing packaging up interactive IO library. <Thierry: Mahlo universe? -> can be put up.>
    • Thorsten: Worked with Thierry. Reflection pattern( Boolean conjunction -> Set) 
     T : Bool -> Set
     _∧_ : Bool -> Bool -> Bool
     pair : ∀ {a b} -> T a -> T b -> T (a ∧ b)
     data PairView : ∀ a b -> T(a ∧ b) -> Set
                     -- problem a and b can't be inferred.
        _,_ : (x : T a)(y : T b)-> PairView (pair x y)
     pariview : (p : T(a ∧ b)) -> PairView p

     ... p ...        with pairview p
     ...(pair x y)...
  • Ana: Axiomatization of odd-even adder(?). Had the misfortune of talking with Thorsten. Figuring out how to use using Std library. <busy with Chalmers business> <Bengt: going outside Chalmers would be better>
  • Bengt: Looked at coinduction. Everyone talks about bisimulation in describing coinduction. Is it necessary to explain coinduction? <Thorsten: No.> Don't want final coalgebra, a more naive meaning is wanted. <Thorsten: bisimulation is simple in Agda.>
  • Phillip: I like Agda. Go Agda!.
  • Kato-san:
  • Ulf: Universe Polymorphism. New construction Set i. 
     data List {i : Nat} (A : Set i) : Set i where ...

     ns : List {0} Nat   -- 0 inferable
     ns = 0 ∷ 1 ∷ []

     xs : List {1} Set   -- 1 inferable.  Unadorned Set is Set0.
     xs = Nat ∷ List Nat ∷ []

     Matrix : ∀ {n} -> Set n -> Set n

     data IO {n} (A : Set n) : Set (suc n) where
       return : A -> IO A
       _>>=_ : ∀ {B : Set n} -> IO {n} B -> (B -> IO {n} A) -> IO {n} A

     -- These will be primitives and at least the two latter ones will be implicit
     postulate
       ↑_ : ∀ {n} Set n -> Set (suc n)
       ⇑_ : ∀ {n}{A : Set n} -> A -> ↑ A
       ⇓_ : ∀ {n}{A : Set n} -> ↑ A -> A

     ↑IO : ∀{n A} -> IO {n} A -> IO {suc n} (↑ A)
     ...

     -- join was impossible before.
     join : ∀ {n A} -> IO {suc n} (IO {n} A) -> IO{suc n}(↑ A)
     join m = m>>= λ x -> ↑IO x

     -- New sort Set ω needed to type universe polymorphic types:
     --        A : Set i    B : Set j    x ∈ FV j
     --    ---------------------------------------- 
     --            (x : A)-> B : Set ω

16:00- ...
Code Sprints

Edit | History | Recent Changes (all) | Search
Page last modified on November 28, 2009, at 09:13 pm
Powered by PmWiki