CodeSprintDiscussion

Code Sprint Discussions

(20110406 - raw memo with dropped suggestions Attach:CodeSprintDiscussion20110406PM-raw.txt )

The record of Day3(Friday) has been lost. Leaders are requested to fill in ...

Next? code freeze target date: sometime arond next AIM.

Day 5: Andreas Abel Presentation of a bottle of wine

• Unification. eta friendly, record, iso btw records-> A and curried form.
  • Leader : Andreas
  • Day2: Started
  • Day3: (lost)
  • Day4: done: freezing of metavar at a block end. Test suite run ok. Eta thing still not done yet.
  • Day5: -- new mutual block syntax with separate sigs and defs -- explicitly specifying dependencies.
    module Mutual where mutual

     data Vec (A : Set) : Nat -> SEt
     record Sigma ...
     bla : Bla

     data Vec A where
       nil : ...
       cons : ...
     bla = ...

   mutual
     data U : Set
     El : U -> Set

     data U where
       base : U
       pi : (a : U) -> (El a -> U) -> U

     El base = Nat
     El (pi a b) = (x : El a) -> El (b x)

-- requires rewrites of existing code.

  (automatically figuring out dependencies and grouping is a bit hard.)

  ---------------------

  Changed metavar lifetime (day 4)

  one : N
  one = _

  force : one \equiv suc zero
  force = refl 
  -- this no longer solves _ of one that is in a different group.

  mutual
    one : N
    one = _

    force : one \equiv suc zero
    force = refl 
  -- this is as before, _ is solved.

  force : let one : N
              one = _
          in one \equiv 1
  force = refl
  -- this is also as before.

• Dependent irrelevance (minor)
  • Leader : Andreas
  • Day2: Finished, with Guilhem. Demo: In addition to irrelevant args and fields we had, we now have
    elimSq : ... (ih : .(a : A) -> P (squash a)) -> ... or

            ... (ih : \all .a -> P (squash a)) -> ...

   postulate P : .A -> Set
   f : ._ -> Set
   f = \ .x -> P x

   f' = \ .(x : _) -> P x
   f'' = \ .{x y z : _} -> P x

   -- IrrelevantFin is not allowed.
   data Fin : Nat -> Set where
     zero : .(n :Nat) -> Fin (suc n)
     ...

   -- But this type checks ok.  Not sure what this means though
   data Fin : .Nat -> Set where
     zero : .(n :Nat) -> Fin (suc n)
     ...

• Irrelevance and unification, connected with proof search
  • Leader : Dominique
  • Day2: gone
  • Day3-4 : all gone.
• Documentation
  • Internals (see the "HACKING" file); Externals ("abstract", "coinductive types")
  • Leader: Wolfram
  • Day2: Talking on Day1. No concrete docs yet.
  • Day4: Inserting docs in source code to understand things...
• Pattern synonyms
  • Leader: Stevan
  • Day2: Rumor that something is being done.
  • Day4: Talked with Daniel. Tricky. Looking into the source where to put the stuff. design re typed/untyped etc not fixed yet. New keyword "pattern".
    N: If you had a pattern syn for length 2 vector, ... do a non-linear pattern result?

    probably not a problem, will become .patvar..

    Partially applied pattern synonym?
    checking pattern would be per use.
    Intended use: when using Conor's universe etc.
• Template Agda
  • Leader: Nicolas
  • Day2: Nothing yet; work on BUILTIN must be done first
  • Day3: (lost - something about interleaving scope checking(importing) and type checking)
  • Day4: Demo. Term splicing.
    import Common.Reflect
    MySet : Set1 MySet = $(sort)
    test1 : MySet \equiv Set test1 = refl
    id : (A : Set) -> A -> A id = $(lam false (lam false (var 0 [])))
    polyId : ...
    data T : Set where

     tt : T     

   quoteOK : T
   quoteOk = $(con (quote tt) [])

   -- U: some worry about scoping.

   f : Set -> Set
   f x = $(def (quote x) [])
              --^ error

   f : Term -> Set
   f x = $(x)
         --^ can't unquote

   f : Term -> Set
   f x = $(var 0 [])
   -- works

   f : Term -> Set
   f x = $(var 1 [])
   -- panic ... checking closedness is not implemented yet.


   -- U: re scoping, this might leak private names.

   mutal
     f : Set -> Set
     f = $(def (quote f) [])
   -- f's in red, non-termination.

   -- N: prefers a keyword("splice", "unquote", ... ?) over $
   -- "unquote" won.

• Day5: still some bugs, but got good working examples.
  mutual

     data Term : Set where
       var  : Nat -> Ars -> Term
       con  : QName -> Agda -> Term
       def  : ...
       lam  : Hiding -> Term -> Term
       pi   : Arg Term -> Term -> Term
       sort : Term
       unknown : Term
     Args = List (Arg Term)
  # BUILTIN AGDATERM Term #
  # BUILTIN AGDATERMVAR var #
  ... (discussion on if hiding is needed at this level) ...


   MySet : Set1
   MySet = unquote sort

   idSet : Set -> Set
   idSet = unquote (lam false (var 0 []))

   -- n-ary function  
   test : (... \equiv ... ) x (... \equiv ...) x (... \equiv ... ) x (... \equiv ...) -> ...
   test = unquote (tuple (repliate 4 tmrefl))
          -- instead of refl , refl , refl , refl


   -- instead of
   --   pair t u = con (quote _,_ (arg false t :: arg false u :: []))
   pair t u = `con (quote _,_) (repliate 2 false)


   unquoteTwice : Set1
   unquoteTwice = unquote(unquote (con (quote sort) []))
   -- N: concern about constraing solving in meta-level checking interfering with object-level.


   Pi^n : Nat -> Term -> Term
   ...
   Lam^n : Hiding -> Nat -> Term -> Term
   ... 
   Proj : (i n : Nat) -> Term
   ... -- church numeral
   proj : \all i n -> Term
   ... ==> panic "unbound variable 0"
           due to lack of contexts for terms.

   -- on to definitions
   getDef : Name -> Def
   ...
   foo : Def
   ...
   unquote
     foo
     gen-induction (quote length)

   --
   length-ind : unquote(gen-induction-type(quote length))
   length-ind = unquote(gen-induction (guote length))

• Hiding declarations
  • Leader: Nicolas
  • Day2: Nice syntax NOT decided on Day1. A new block syntax, or reusing module syntax. Shadowing allowed or not? can result in ambiguity. Bengt: how about \renewcommand like thing? not quite. The situation is
    module ... f = ... open M -- with f inside -- here you want to hide the local f and want to use M.f
  • Day3: (lost)
  • Day4: Nothing
• Record pattern matchin in lambda / local case /extended lambda
  • Leader: Noam, Daniel
  • Day2: on extended lambda. Turning extended lambda into a helper function which is typechecked. Some issues in parsing. incosistency btw lambda and function defs, e.g., type annotation. Long term issue: Do we want to keep type annotation for lambda? Q on whether we could do "with"? U: We would.
  • Day4: Figured out parsing.
    \( ... = ... ;

      ... = ... ;
      ... = ...
    )

    (braces \{ ... } caused shift-reduce conflicts in grammar)

   Translation to temp func decl: at ConcreteToAbstract stage now.

   A few more days to finish all.

• epic backend
  • Leader: Olle
  • Day2: Nothing yet. Got input from Andreas.
  • Day4: Still on IO module in std lib. Made it strict. Fixing bugs.
  • Day5: Trying the new IO module for reading files etc. Demo:
    Strict.agda ... ... %effect ...
    {-# COMPILED_EPIC writef (s : Ptr, str : Data, u : Unit) -> Unit

        = foreign Int "fputs" (mkString(str) : String, s : Ptr); primUnit #-}
   ...

   withFile : \all {A} -> String -> String -> (Strieam -> IO A) -> IO A
   withFile file mode f =
     fopen file mode >>- \ handle ->
     f handle >>= \ res ->
     fclose handle >>= \ _ ->
     return res

   readFile : String -> IO String
   readFile file = withFile file "r" read
   -----
   AgdaPrelude.e
   ...
   primStringAppend(xs : Data, ys : Data) -> Data = case xs of
    {Con 0 () -> ys
    |Con  (x : String, rest : Data) -> Con 1 (x, primStringAppend (rest, ys))
    }
   ...
   -----
   Danger of introducing incosistency via ffi.
   ----
   Compilation works.
   ----
   Webbrowser written in Agda
   (Using Agda to write call back funcs for Webkit.)

   module webkit where
   ...
   open import gtk
   ...(binding)...

   module ..

   main : IO Unit
   main = gtk.Init >> ...

• Installation
  • Leader : Bengt
  • Windows(makoto), Mac(Everybody who had Mac problems)
  • Synching Haskell Platform and Agda (release version is done)
  • Ulf: changed the wiki.
  • Day2: (Mac) BN succeeded in installing w. experts helps, and updated Ulf's instruction. Still impossible with lingering old version of stuffs(GHC, cabal, ...). (Linux) : IMPORTANT. extending the sprint. (Win) Nothing concrete yet; Got good input from Wolfram; try not rely on cabal-install.; will aim for a make target "build-win-installer" or something.
  • Day4: Nothing new.
  • Day5: (Win) Only three-quarter finished: check existence of, download, and install Haskell Platform

         and emacs-23.  Still to go: font, Agda compilation, haskell-mode, agda2-mode.

• Builtin - better generic interface, cleaning up the code.
  • Leader : Simon
  • Day2: Bare representation of BUILTIN related info (Haskell level; cleaned up). Test suite problem identified.
  • Day4: working on co-induction...
• records in mutual blocks + more flexible induction-recursion
  • Leader : Thorsten
  • Day2: Nothing yet. Talking with Thierry.
  • Day4: Refactored Concrete.hs and Abstract.hs, proceeding with Ulf' guidance.
• Fix bug interactively: let more ppl know Agda internals.
  • Leader: Andreas

Thomas: Tutorial? Better error msg (refine)

• Day2: Risky. could take 2min to 2hr. Ask Thomas to ....
• Day3: (lost - 3 bugs fixed)
• Day4: modified wiki pages ....

• Non-canonical implicit args
  • Leader: Dominique

U: some concern about record module generation; still, should be merged.

• Day2: On day1:
• Day3: (lost)
• Day4: left
• Day5: (U decided against merging for now, due to inefficiency it introduces for ordinary checking)

• Argumentation
  • Leader: Makoto
  • Day2: nothing yet.
  • Day4: some discussion with Bengt. Agreed: "argumentation scheme" seems a hopelessly shallow, ad-hoc cocept; still, Agda-ised catalogue of shceme could be useful in some context.
• Avoid unnecessary type checking with finer granurality.
  • Leader : Wolfram
  • Day2: Interface Seriarization to support AST. Looked at upper layer, talking with U on design issues.
  • Day4: Ramification concerning hightlight-info. Working on comparison of possible ASTs.
  • Day5: Started to write AST as interface. Size increases by 50~100%. Writing interface takes a lot of time now; don't know why yet. Two new options: --trust-AST, --dont-trust-mtime (modification time)
• Cabal for Agda
  • Leader : Darin
  • Day2: Discussed a bit.
  • Day3: Nothing
• Program extraction
  • Leader: Anton
  • Day2: Succeeded in installing Agda (-> Installer).
  • Day4: Wrote code to relate cauchy real and signed digits and postulated reals and ... slides and code is on the wiki
• Profiling of open term reduction
  • Leader: Karim
  • Day2: Not yet.
  • Day3: Nothing
• "where" as an expression
  • Leader: Cezar
  • Day2: Not yet. Cezar wanted pattern matching definitions in "where"; more than current limited let-decls.
  • Day3: (lost)
  • Day4:
• Abstract internal term representation

starting one for variables?

• Leader: Ulf

NP: Nice interface could force bad complexity.

• Day3: <lost>
• Day4: cancelled.

• http interface to agda proof engine