Code Sprint Discussion

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