2015-06-03!

2015-06-03!

• JC, AA, NAD :: Normalising simply typed lambda term using Delay Monad with sized inductive types
  • Had written CBV, now trying CBN
  • replacing Val to Delay Val - does not work with Size.
  • Delay monad def was wrong.
    • (i : size)(A:Set) wrong
    • should have taken (A : size -> Set)
    • but that doesn't work w.r.t. monotonicity.
  • Would add annotation for "antitone"
  • Problem: Proliferation of annotations with preservation of polarity
  etc.
  • Providing proofs of the preservation etc. manually may be better?
• AV, JC :: Caching of type checking result & Pragma NOETA

  • test case for single def with one open goal to be checked 1000 times. -> exhibits leak, investigating the cause.

  • Implemented NOETA pragma.
    • JC tested it for the cat thy lib(heavily nested records), 2x faster; no particular incovenience without eta.
      • THM: "Kleisli adjunction is initial in the cat of adjunctions for a monad"

2015-06-05!

 * AA, (MT): Serialisation speed up
 - 30% speed up since last AIM, by memoising QName serialization.
 - Looking for 50%, by trying to avoid worthless sharing for small data.
   (2x speed up from Agda 2.4.2.2)

 * NP: Packaging
 - trying to package Agda code in Java script.
   - On Agda side, js command in a monad.
 - somehow "ignore file" does not work.
 - demo: np.github.io/Pacman in html5

 * SA: agdARGS
 - CLI. Interpreting command line to invoke combination of subcommands
 #+BEGIN_EXAMPLE
 -- a subcommand
 sum-nat : Comand Level.zero
 sum-nat = record { descriptoin = "..."
                  ; subcommands = `[] , commands ⟨⟩
                  ; modifiers   = `[] , ⟨⟩
                  ; arguments   = ALot (List.rawMagma ℕ) , mapError [_] ∘ Parseℕ
                  }

 main : _
 main = run $

♯ getArgs >>= λ args →

  ♯ [ error , success ]' (parseCommand (exec sum-cli) args)
  where ...
 #+END_EXAMPLE

2015-06-09!

 * AA, MT : Optimising serialisation.
 - Serialising Interface data to data.
 - In Agda-2.4.0, it took up 50~60% of total execution time.
 - In AIM XX, that part became 1.5x faster, but still taking more
   time than the typecheking.
 - Overview : Hash Consing
   - icode : a -> S Int32 -- mapping a to an Int32 index into a hashtable
   - value : Int32 -> R a
   - The same thing gets the same Int32 -- introdusing sharing.
 - Done in AIM XXI
   - Utilizing qnameId of QName
     - (QNames are fat and numerous in an Interface.)
   - Thr: Introduced specialised hashtable for QName (which is wrtten out to .agdai)
     - Got 2x improvement in Ser. time.
     - Got 2x size for .agdai
   - Fri: Used the above just as memo table for memoised icode func.
     - Got the size of .agdai down
     - Got only 1.3x speed. - mysteriously dissapointing.
 - Discussion:
   - Alternative: Hash consing everything all the time
     - pros: All equality checking becomes fast
     - cons: makes everything state dependent, hard to debug
   - Keep QName info etc in a global symbol table.
   - Use StableName ?
   - What's the main issue in Agda efficiency now?
     - time consumed at: Typecheking(30s), Serialisation(25s),
       Parsing(10s).
     - Is standard library representative code? Some other types of code
       behaves differently.
       - Turning on interactive highlighting makes visible what's
         going on.
 * AS, AA : IO in Hancock-Setzer style, coinductively.
 #+BEGIN_EXAMPLE
 mutual 
   record IO (i : Size) (A : Set) : Set where
     coinductive
     field
       force : {j : Size< i} → IO' j A
       -- size = the depth of IO computation to force.
   data IO' (i : Size) (A : Set) : Set where
     do : (c : C) (f : R c → IO i A) → IO' i A
     return : (a : A) → IO' i A
   data IO+ (i : Size)(A : Set)  : Set where
     do : (c : C) (f : R c → IO i A) → IO+ i A
 #+END_EXAMPLE
 - Discussion
   - Having both IO and IO' versions of things could be avoided by
     "with force m" / "case (force m) of" ...
     - force (m >>= k) {j} = case (force m {j}) of λ { ... }
   - the musical notation could be used as a shorthand for such boilerplate code.
   - Can forcing be a view pattern?
   - new syntax? : "force ((force -> return a) >>= k) = force (k a)"
   - new syntax2?: "force ((delay (return a)) >>= k) = force (k a)"
     - delay is the constructor for the record IO i A
   - TXA: Isn't copattern matching an illusionary problem? Musical
     notation is fine. No need to have mutual record-data definition.
   - Guarded type theory?
   - AV: Generate those as translation of the use of ∞_ 
     #+BEGIN_EXAMPLE
     record ∞(A : Set) (i : Size) : Set where
       coinductive
       field force ...
     #+END_EXAMPLE
     - instead of using musical ♯ to stop evaluation, rely on the fact
       eval occurs only in the copattern force(...).
     - Currently, connecting this with cubical type theory.

 * AS : Experiment on coNat.
 - coEven and coOdd.
 - 
   #+BEGIN_EXAMPLE
   mutual
     record coEven (n : coNat) : Set where
       coinductive
       field
         Even↓ : coEvenaux(Nat↓ n)
     coEvenaux : coNataux → Set
     coEvenaux zero = ⊤
     coEvenaux (sucNat n) = coOdd n
   #+END_EXAMPLE
 - Why is coEvenaux recursive and inductive?
   - With succ defined by corecursion, this way gives better
     computation and better expressed case distinction.
 - (Later) : Defining coEvenaux as inductive data turned out to be also
   nice.
   - UN: proofs are actually nicer than the previous version.
   - AS: some nested copattern have to be decomposed to mutuals.

 * AS, SA : Object oriented programming
 #+BEGIN_EXAMPLE
 record cell : Set where
   coinductive
   field
     getresult : String
     getcell   : cell
     putcell    : String → cell
 #+END_EXAMPLE
 - A demo console program using AS's IO library.
 * GA : agda-mode new "SearchAbout" feature
 - M-x agda2-search-about-toplevel    (kbd "C-c C-z")
 - can request all the information about a name.
 - can work with a substring of a name.
 - not yet: foogle / coq like type-based search 

 * UN: Today's hacking
 - Trying AV's new pragma NOETA on stdlib so that only the necessary
   part is eta expaded.
 - Record pattern translation shouldn't expand when NOETA is in effect.
   => Fixed.
 - Still a problem with defs inside a record module.
   => introduced record pattern untranslation.
 - (The report from Wed: JC: NOETA on the record-heavy cat lib gave 50%
   speed up. - UN: With proper NOETA, order of magnitute speed up
   expected.)
 - A bit on M-Tac w. JCo.


 * Next AIM
 - JeCo: looking for the possible venue.
   - University rooms are cheaper, but in short supply. 
   - Either before end of Septermber or after middle of October
   - JeCo will report back when the venue situation clarifies.