AIMXII /
\ AIMXII

Notes from AIM XII

Discussion on Future of Agda (6/9 Monday Morning)(Please correct)

Discussion on AIMXIII and AIMIXV

CodeSprint Planning Discussion (1/9 Tuesday Afternoon)

Irrelevant Discussion & impl.

  • Andreas, Ulf, Thorsten, Nisse, JP, Edwin
  • Day1: None
  • Day2: None
  • Day3: Started implementing Edwin's Forcing optim. Focusing on compile time benefits, not the runtime(but c. helps r.) Standard library run epsilon much faster now. Tagging constructor args and function args that are forced by the result type of the constructor/function. When comparing two cons, no comparison of length args. Constructed an example that run much faster after optim. Investigating why just epsilon for the lib. Needs to be more aggressive / maybe aggressive. Hard to profile whats going on(Haskell's uncertainty principle.)
    Andreas: There's a proper irrelevance analysis you could do. (map? example please add) Ulf: Worry about that is what happens with metavars.
  • Day4: Andreas DEMO. "IrrelevantApplication.agda" 
    postulate
      f : {A B : Set} -> A -> .B -> A  -- .B would be a proof argument

    data _==_ {A : Set}(a : A) : A -> Set where
      refl : a == a

    proofIrr : {A : Set}{x y z : A} -> f x y == f x z
    proofIrr = refl

    id : {A B : Set} -> (.A -> B) -> .A -> B
    id g x = g x

    -- This does not type check 
    -- id : {A B : Set} -> (A -> B) -> .A -> B
    -- id g x = g x

Does id preserve irrelevant-ness?

Yes. 

    pId : {A : Set} -> A -> A
    pId x = x
    -- t = pId (id{ ... }) -- example to be filled

Is it not undecidable?

User specifies and Agda keeps track of irrelevant-ness in the context. 

   Conservative approximation.

    data Bool : Set where
      true false : Bool

    not : .Bool -> Bool
    not true  = false -- needs to fail 
    not false = true
  • Day5: Andreas: Trying to get pattern matching right. Day4's example 'not' fails to typecheck as expected. You want to match record against irrelvant things. Typechecking patterns are quite complicated.
    Highlevel overview: Trying to finish, trying to see how much gain we get for large records with proof components.

Universe polymorphism

  • Andreas, Ulf, Nisse
  • Day1: 0.5 hr discussion; can do it; it'll be awsome.
  • Day2: Started implementing. Ran into problems. Realised that there's fundamental problem in MiniAgda metavariables for sizes. Now solving by staring at the white board. Not yet despairing.
  • Day3: Nisse found out the fundamental prob. of yesterday is not fundamental. The problem found by Ulf (subtyping constraint solving algo does not know anything about Miller higher-order pattern thingy but) might not apply to us about Level's.
  • Day4: Almost compiling now. Not quite as easy as we thought, have something that might work. Trying to go for the case where you only allow single level variable. Then subtype constraint solving gets easier. What you have to write is less than before. JP: "If you are lucky you got away with less, but if not, the same as before". Single variable and accumulativity working would mean less. Previously, only solving unif. that we know to have unique solution. The same can't be done for level thing. We could refuse the uncertain case and force user to annotate more.
    We are getting closer to a solution that works.
  • Day5: Nisse,Ulf,JP,.. Even closer to completion. Not committed yet. Now it compiles, runs, but some constraints are not solved correctly this morning, will be finished in a couple of days.

Constraints and Smart case

  • Thomas, Thorsten, JP, Andreas, Shin-Cheng

(Both formalising in Agda and implementing for Agda/Mini-Agda)

  • Day1: None
  • Day2: Almost None.
  • Day3: Looked at formalization of LambdaBool. Idea: Big step sem of LambdaBool. Trying to show Algorithimic equality and Declarative equality agrees. Shown soundness.
  • Day4: Looked at completeness proof of big step sem of LambdaBool without constraints. Trying to understand contraints by removing them completely. It's a nice thing on its own, related to James Chapman's relating complentenss of big step sem and declarative def of equality. Useful for partial setting.
  • Day5: Continue to work on formalization, fixed the semantics, complete proof on whiteboard, could be turned into Agda. Plan is to look at the case WITH constraints next.

Install Agda

  • Thomas
  • Day2: Done
  • Day3: Bought a faster computer to cope with Agda.
  • Day4: Succeeded in all attempts on empty set of attempts.
  • Day5:

D-Case discussion and implementation

  • Bengt, Makoto, Yoshiki
  • Day1: Detailed explanation of current scheme; conveying what are problems with it; no direction yet. Whether to mix definitions and explanations.
  • Day2: Makoto: Send a buggy patch to Ulf. Trying to get the BUILTIN for the special D-Case operators to work. Bengt: Reading up on the background of D-Case.
  • Day3: Makoto: Stuck with ENCODING related difficulty to pass the tests... Bengt/Yoshiki:None
  • Day4: Makoto: (Making test suit works on Windows), D-Case could be a separate packge, still Agda itself has to be extended for Builtins;
    Reflection code sprint
    Yoshiki, Bengt:None -> Codata with Anton
  • Day5: Makoto: (More efforts on test suit on Windows) No builtin for _\ni_ and <_/_> yet. -> Interface discussion. (D-Case/Agda will be a separate package including builtin extension.) Yoshiki/Bengt:

Codata/Coalgebra

  • Anton, Bengt, Yoshiki,
  • Day4: 6 ways to write Colist. Winner: Colist having two indices. One tells whether its empty or not.
    < code to be filled >
    Bisimulation
  • Day5: Anton implemented the idea in Agda(coalgebra as record), but termination checker rejected it. (Agda version not the latest).
    • Coalgebra as record 
    data N : Set
      (as usual)

    record Stream (A : Set) :Set where
      field 
        head : A
        tail  : Stream A

    a : Stream N                         -- a red
    a = record { head = zero; tail = a } -- 2nd a red

    inc : N -> Stream N                          -- inc red
    inc n = record{head = n; tail = inc(suc n)}  -- inc2 red


    inc' n = record { head = n; tail = record {head = suc n; tail = in'(suc(suc n))}}

    record Bisim(l : Steram N)(l' : Stream N) : Set where
      field headeq : Steram.head l == Stream.head l'
            taileq : Bisim (Stream.tail l) (Stream.tail l')

    proof : Bisim inc inc'
    proof = ...

    -- Type checks, but termination checker give red warning.
Th: There's confusionn between recursive structure by record and coinductive types. 
  Anton: Yes, like what you want w.r.t. eta.

  Discussion on translation between coalg way and infinity way. (please fill out)

Infinite Games / Codata

  • Martin, Makoto, Andreas, Thorsten, Nisse
  • Day1: No significant result yet.
  • Day2: Martin & Thorsten: Infinite games. Implemented Bang !. Using Nisse's technique. Defined composition for partial strategies on infinite games using Partiality Monad.
  • Day3: Continued to formulate more about inf game. Found in practice there's a lot of places we must beat termination checker (expand, etc.) Got to the associativity of tensor, but blow up factor is big. Sized type might help, but still investigating.
  • Day4: Martin put up a copy of the code including the infinite game developments at http://people.bath.ac.uk/mdc25/agdagames.tar.gz .
  • Day5:

Process Algebra ACP in Agda

Interface to external theorem provers, Reflection

  • Simon, Makoto, Thorsten, Ulf, (Anton)
  • Day1: None
  • Day2: Simon/Makoto discussed some. Hoping quoteGoal with Contexts. Need a builtin interpretation function ("unquote"). Ulf has some examples to be published as a DTP agda source file. Need a way to use Haskell version of function decision : Problem -> Bool (with Agda version for soundness proof)
  • Day3: Decided to how to write "unquote". Clarifying the primitives to write your own unquote. QName -> arity, QName -> type, QName -> Handling of Term needs to be changed. Needs representation of context. quoteGoal should give you not only reified type but the context too. AGDATerm structure gets quite complicated to guarantee the consistensy of arity / type info and usage, etc. Partial application requires BoundedVector instead of Vector. Prototyping Agda side with postulated primitives. Term done. Going on with unquote from primitives.
    Thorsten: 1. Good (and small) use case would be nice. 2. The extension do requires getting inside Agda implementation. Try starting with small feasible parts.
    S: use case: Equational Reasoner, tactics, ... T: use case with unquote...
    U: with external procedure, checking the returned proof may be more expensive than running decision procedure in Agda.
    Safety of unquote: Let unquote to take reified Context, Term, and Environmnet while quoteGoal gives..(Later)
  • Safety material is often needed agaibns thefts ; best solution is a certified safe - coffre-fort A2P certifié par les assurances.
  • Day4: Simon: Looking at the way to do. In theory a simple thing to do. Infra to imcorporating new haskell module is there. Problem is how to link it up with the interface. Situation: You are in a goal the type of which Agda knows. Must supply goal type details to a function that prepares the input for the external tool. Putting together a syntax for a configuration file that describes what Agda needs to know. 1. Goal pattern (for type) telling what kind of goal can be accepted for a tool. Decomposes the goal to bits of information. 2. Function to decide and produce data for proof. 3. Function to reconstruct Agda proof. Started to get familiar with Agda code. Would document the finding. Difficulty is the kind of tediousness. When done, would be quite powerfull. Extension to reflection is required but not as essential as it was thought in the beginning. Application of tactical without users' making context explicit.
    The model: Agsy working with Agda that knows little about Agsy.
    For current application, reified proof etc were prepared. Ulf: Those can be grabbed from TC state from *ghci*. No need for reflection.
    Reflection would be a nice way to formalise tactics if it is not a necessity.
    Ulf: that is orthogonal to external prover thing.
  • Day5:
    • Idea to add new builtins within the extra Agda extension package.
      • Just modify the TCM state at *ghci* prompt (need to catch 'NoSuchBuiltin' exception)
      • Agda typechecker and reducer would not know about the new builtins, but the Agda extension package can use them.
      • Info necessary for builtins could be given in terms of Agda file (expected type and reduction) + alpha (optional: translation to/from Internal.Term and reduction behaviour in haskell)
      • Keeping the info necessary for builtins in the TCM state will enable dynamic(runtime) addition of new builtins (rather than at the compile time of extension package.)
      • Simon started working on implementing the new builtins. Reflection: Idea is sound but needs more thought to do it non-invasive way. User must have control about the granurality. Ulf: you can change the 'abstract' property of definitions temporarily.

Make Epigram work

  • Pierre, Peter
  • Day1: It works. but efforts conitnues.
  • Day2: It is still working. Trying to fix the machinery that turns recursive calls to eliminators. bugs in unification algorithms. Definitions of nicer elimination gadgets. Starting look like Epigram(you can almost run that look like functional Epigram program rather than raw type theory terms...) Start programming in Epigram next week.
  • Day3: Nothing.
  • Day4: Peter went home. (Th: Must have done smthg...)
  • Day5: Demo in the morning.

Formalization of Category theory and Families of Setoids, Optimizing Agda

  • Darin, Iain, Martin
  • Day1: Exponentials, Setoids implementation with "Extensional Equality in ITT"
  • Day2: Efforts continues. CCC. Comma Categories. PERFORMANCE PROBLEM.
  • Day3: Cones, limits, --> products, terminal objects, ..
    (Ulf: The optim today did not have effect on the cat examples...)
    Setoid model of type theory in Agda and Coq
  • Day4: Arrow categories. Slice&Coslice and related proofs/examples. Setoid model implementation continues.
  • Day5: Adjunctions, limits, products; better understanding of the cause of unusability. 'import ProductCategoy' hardly works, but defining top-level concepts works. 
    http://gitorious.org/cats/setoidcats
    git://gitorious.org/cats/setoidcats.git

Cabal support for Agda, Agdackage

  • Darin, Ulf, Nisse
  • Day1: None
  • Day2: Nothing
  • Day3: Nothing
  • Day4: Nichts
  • Day5:

Termination Checker(Parametric definitions and Mu-nu)

  • Thorsten, Ulf, Andreas, Nisse
  • Day1:
    • Parametric def: Interesting Discussions. Still more details to be discussed.
      Two options.
      • 1. Extend current termination checker
      • 2. Use sized type (needs improvement to make it practical)
      Option 1 gives you short term benefits, but 2 would be better for a longer term (with a lot more work.)
    • Mu-nu: None
  • Day2: Looked at Parametric defs in detail. Figured out it works for corecursion in the same way. Most details done (some ways to go to make it nicer).
  • Day3: Nothing
  • Day4: ?
  • Day5: Know more than before the meeting. Documented in ?. The Problem is for a mutual def block, sometime you can get passed termination checker by expanding the code by hand, and that is ugly. Instead of expanding, termination checker could be parameterised w.r.t. the higher order arguments (those things that were inlined by hand?)

Removing codata, making infinity primitive, disallowing broken mu-nu

  • Nisse
  • Day1: None
  • Day2: In progress. Fixed unrelated bugs.
  • Day3: Not Pushed but Done. Small issues remain
  • Day4: codata Removed. disallowing broken mu-nu still undecided wheter it's worth.
  • Day5: Nothing

Extending mixfix syntax to binders.

  • JP, Nisse, Ulf
  • Day1: Clarified issues.
    • Need to tell which part will the bound variable scope over
    • Two different behaviours: lambda style or Pi style.

Possible syntaxes:
Thorsten: \x<-_;_[x]

Ulf:
syntax bind e1 (\x -> e2) = x <- e1 ; e2

JP: What to use for Pi style?
syntax exists (\(x : A) -> B) = (x : A) × B
syntax exists (forall x -> B) = (x : _) × B
syntax exists (A -> B) = A × B
syntax exists (\(_: A) -> B) = A × B

  • Day2: Discussed impl. details. Shouldn't be very difficult. (Nisse: still some doubt about if it's essential.)(Ulf: It can be the way to fool users to feel they are programming in something other than Agda. Cf. Basic in Haskell)
  • Day3: JP: Started writing up "Spec" MixFixBinders
  • Day4: JP: Spec has been approved. Implementation started.
  • Day5: Done the stupid part. Ready for the interesting part.

Axioms of Parametricity

  • JP, Thorsten
  • Day1: None
  • Day2: None
  • Day3: None
  • Day4: Th too busy.
  • Day5: Discussed. Haven't given up on someday to have the axioms. The axioms will be like: 
      -- relational interpretation [A]
      axiom : \all (x : A) -> [A] x x
Hoped to implement the generation of [A] and the proof via 
  reflection, but not yet.

  Th: having the axiom with computation would be difficult since
  parametricity is a very much of extentional thing.

Conclusion

Nisse: We've done a lot .... Continue working ...

External Link Page :

Edit | History | Recent Changes (all) | Search
Page last modified on December 06, 2015, at 10:48 am
Powered by PmWiki