# Record Of AIMXVII

- HTML version, org-mode source

____________________ RECORD OF AIM XVII ____________________ Table of Contents _________________ 1 Participants: 2 (7 May Tue) .. 2.1 Supper 18:30 ~ 3 8 May Wed. .. 3.1 Agenda discussion, orientation : 9.00 - 10.00 .. 3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30 4 9 May Thr. .. 4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power) .. 4.2 James Chapman: On copatterns: 11.00 - 12.00 .. 4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00 .. 4.4 Shuji Kinoshita: On Granström's World : 14.00 - 15.30 .. 4.5 X-Sprint : 15.45 - 18.00 5 10 May Fri. : Excursion 6 11 May Sat. .. 6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40 .. 6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40 .. 6.3 MT : Meta-verification and validation 16.00 - 17.00 .. 6.4 X-Sprint : 17.00 - 18.00 7 12 May Sun. .. 7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40 .. 7.2 X-Sprint : All : 14.00 - 17.30 .. 7.3 Wrap up .. 7.4 JC and MT: .. 7.5 YK and JC: .. 7.6 SK .. 7.7 JC and SK and MT 8 13 May Mon. .. 8.1 X-Sprint, Wrap-up .. 8.2 Next AIM Discussion: 1 Participants: =============== - James Chapman (Institute of Cybernetics) - Shuji Kinoshita (NAIST) - Yoshiki Kinoshita (Kanagawa U) - Bengt Nordström (Chalmers) - Makoto Takeyama (Kanagawa U) - Liyang Hu (Tsuru Capital LLC / U Nottingham) 2 (7 May Tue) ============= 2.1 Supper 18:30 ~ ~~~~~~~~~~~~~~~~~~ 3 8 May Wed. ============ 3.1 Agenda discussion, orientation : 9.00 - 10.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ § 3.1.1 Planned schedule: [http://wiki.portal.chalmers.se/agda/uploads/Main.AIMXVII/AIMXVIITImeTalbe.pdf] (Excursion moved to Friday due to the forcasted rain on Saturday.) § 3.1.2 Actual --------------------------------------------------------------------------------------------- Wed JC 10.30 - 11.45 On Copatterns JC, All 14.00 - 17.30 Continued to discussion sprint? on copatterns --------------------------------------------------------------------------------------------- Thr YK 09.00 - 10.40 Category Theoretic Structure of Setoids JC 11.00 - 12.00 On Copatterns (cont.) (JC,MT) 13.30 - 14.00 ((Not) speeding up Agda type checking) SK 14.00 - 15.30 On Granström's Worlds All 15.45 - 18.00 X-Sprint 15.45 - 17.50 - JC,MT,BN : Discussion on Copatterns (cont.) - BN: Explanation of batch type checking - SK: Agda formalisation of the category of Granström's worlds --------------------------------------------------------------------------------------------- Fri Excursion --------------------------------------------------------------------------------------------- Sat JC 09.00 - 11:00 Formalizing restriction categories BN 11.20 - 12:00 Incremental Type checking BN 14.00 - 15.40 Incremental Type checking (Cont.) MT 16.00 - 17.00 Meta-verifcation and validation All 17.00 - 18.00 X-Sprint --------------------------------------------------------------------------------------------- Sun LH 09.00 - 11.30 Software Transactional Memory All 14.00 - 17.00 X-Sprint Mon All 09.00 - 12.00 X-Sprint, wrap-up. --------------------------------------------------------------------------------------------- 3.2 James Chapman(+all): On copatterns : 10.30 - 11.45, 14.00 - 17.30 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ § 3.2.1 Summary JC led the discussion on coinduction and copatterns based on ,---- | Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. | Copatterns - Programming Infinite Structures by Observations -. POPL 2013 | http://www.tcs.ifi.lmu.de/~abel/popl13.pdf `---- up to Section 5.1 - BN: Analysing general scheme of coinductive definition with nested (co)patterns are too complex. We should study simple copatterns / corecursors like we do for inductive types. - Lots of discussions on the sense of "values" and "getting stuck" - Extension to dependent types where type equality involves computation seems non trivial. § 3.2.2 More details - BN: If we take "observers define a coinductive type" seriously, a suitable notation for declaring typing of observers is something like ,---- | Stream A = { X : Type ; head : X → A ; tail : X → X } `---- not like field label declarations ,---- | Stream A = { head : A ; tail : Stream A} `---- - BN: It is hard to try reasoning about the general definition schema with nested (co)patterns as in the paper. *We could study what corresponds to the recursor / elimination principle for coinductive types and explain general definitions in terms of that.* (Like the pattern matching definition of `_+_' is understood in terms of the recursor on ℕ.) - The sense of "values" (which affects the sense of "not getting stuck", "progress" and "coverage") - To say any expression of a negative type is a value seems rough. Is the expression "f ∘ g" a value? (function types are negative.) - What the values of a coinductive type are is not explained as clearly as those of an inductive type. - Is there a problem with the usual "a stream value is one that has cons-headed form with head and tail revealed"? Or is a stream value anything that we know for sure we can make into a cons? (Is the latter just turning the theorem "don't go wrong" to a definition?) - Is it inappropriate to ask what they are? - Values usually are considered for the purpose of conversion checking (besides for being answers). But the paper's type system does not require conversion checking, so the role of value-ness in that regard is unclear. - The sense of polarity of types? Positive = defined by introduction, Negative = defined by elimination? - Relationship between the polarity of types and the bidirectional checking? Here checking vs inferring more or less align with polarity of the type (positive → checked against (at first); negative → inferred). Is there some significance to this? How does this relate to the usual alignment with the form of the term (introductory → checked against a type; neutral → inferred)? - Why the main function must have positive type? Not all objects of negative type seem infinite or unprintable. - What is the status of the reduction relation generated from the observation rules of a program in Sec 4? Is this the operational semantics of the program? Non-deterministic without a strategy? (while evaluation contexts usually are considered in order to specify a strategy?) - It seems non-trivial extend all this to dependent types where type conversion checking involves computation, particularly Lemma 7. - Missing lemma to apply Lemma 8 for Theorem 4? - "If Γ ⊢ E[f] : B then Γ | Σ(f) ⊢ E : B" Ok by induction on E. - BN: Starting with general copatterns makes it hard to see what is happening. What it means to be an object of a coinductive type should be defined to be being able to prove that the (simple) observations on that objet is defined. Type system should guarantee that complex observations are defined. - The sense of values and getting stuck again. - Is the seemingly non-deterministic reduction relation in Sec 4 CR? - Is the sense of "getting stuck" dependent on reduction strategies? - Usually a programming langauge semantics comes with a deterministic strategy and no questions arise about CR or various senses of getting stuck. The paper is more in the lambda calculus tradition? - Finished for today at the end of Sec 5.1 4 9 May Thr. ============ 4.1 Yoshiki Kinoshita: Category Theoretic Structure of Setoids (with John Power) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Discussed the paper ,---- | Power, J. and Kinoshita, Y. | Category theoretic structure of setoids. | Theoretical Computer Science. ISSN 0304-3975 (In Press) | http://opus.bath.ac.uk/34231/1/main.pdf `---- - Mathematical formulation of a setoid where the equivalence relation is replaced by family of sets with refl, sym and trans witnessed by families of functions without coherence requirements. - Discussion on the sense of formalising naive set theory based mathematics in Agda. - Structures on the category Equiv of equivalence relations (complete, cocomplete, exponentials) and Setoid of setoids (products, coproducts, exponentials, no equalisers and coequalisers). - Equiv-enriched Seotid and its weak eqaulisers (inserters). - Discussion on the senses of the terms "proof irrelevance" 1. Identifying all proofs (1a. of certain propositions, or 1b. that appear as function arguments at positions that are declared irrelevant.) - justified by not analysing proofs / not using proofs relevantly in computation. 2. Never comparing two proofs (while not positively identifying the two). 3. Only caring about existence / non-existence of proofs - 1. is the usual technical meaning, but how to call 2? How does 3 relate with 1 and 2 exactly? 4.2 James Chapman: On copatterns: 11.00 - 12.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Continued the discussion from Wednesday. - Still trying to understand the sense of "not getting stuck" from the definition of copattern coverage. - Why don't we see "getting stuck on a variable"? What is preventing computation under context in this system? 4.3 (James Chapman and Makoto Takeyama only): (Not) speeding up Agda type checking : 13.30 - 14.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Experimented on how to speed up type checking / lessen memory usage on JC's category theory code. - Use of "abstract" helped slightly but there were not much opportunity for it for the code already heavily annotated for irrelevance. - Moving let definitions to where clause helped one file but made things worse for the overall build. - Splitting files up 4.4 Shuji Kinoshita: On Granström's Wold : 14.00 - 15.30 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Discussed the paper ,---- | Johan G. Granström. A new paradigm for component-based development. | JOURNAL OF SOFTWARE, VOL. 7, NO. 5, MAY 2012 | https://www.academypublisher.com/~academz3/ojs/index.php/jsw/article/view/jsw070511361148 `---- - Worlds, world maps, the category of world - Things that were figured out during discussion, which turned out to be written in the later part of the paper: - For w = (C, R), w ⇒ X is like the W-type W(C,R), but parameterised in the type X of leaves. W(C,R) ≅ w ⇒ 1. - w ⇒ X is the free monad on the functor ⟦ w ⟧ X = Σ c : C . R c → X - a world map w₁ ⊸ w₂ is a container map w₂ → w₁̂̂* - The equality on programs seems a usual inductive predicate - why is it called a new primitiv of type theory? - It was not clear what exactly is new compared with the original Hancock-Setzer or with container works. 4.5 X-Sprint : 15.45 - 18.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ § 4.5.1 JC and MT, BN Continued copatterns discussion. - In the statement of case 4 of Lemma 14, ⊬v e : B should be read ⊢ e : B and ⊬v e : B for the proof of Thm 15 (Progress)? - In the proof of Progress, why is E₁, and not E₂, shown to be a value context? - From the statement of Progress, "not getting stuck" is seen to apply only for closed terms. - To say any expresssion of a negative type is a value still felt unsatisfactory as an explanation of what a value of a coinductive types is. - Looked for an answer for the above in Granström's thesis, which turned into a wild goose chase. Found no Easter eggs. § 4.5.2 BN Worked on the explanation of batch type-checking. § 4.5.3 SK Worked on Agda formalisation of Granström's worlds. 5 10 May Fri. : Excursion ========================= - 09.11 - 10.24 : From Shonan OVA to Enoshima Station [http://goo.gl/maps/vUe0Y] - 10.24 - 15.40 : Walk along Sagami Bay beach [http://goo.gl/maps/aDwyo] - 12.40 - 14.40 : Lunch: Shabu Shabu 'Viking' buffet - 16.10 - 16.40 : To Inamuragasaki Onsen [http://goo.gl/maps/YXtlZ] - 16.40 - 19.00 : Bath [http://inamuragasaki-onsen.com/ofuro/index.html] - 19.00 - 20.40 : Dinner [http://www.main-inamuragasaki.jp/index.html] - 20.40 - 21.10 : To Shonan OVA 6 11 May Sat. ============= 6.1 James Chapman : Formalizing restriction categories : 09.00 - 10.40 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Discussed the paper ,---- | James Chapman, Tarmo Uustalu and Niccolò Veltri. | Formalizing restriction categories. PCC 2013 | slides url? `---- § 6.1.1 Formalising frameworks of Cockett and Lacks "Restriction Categories" - Partial map categories - Restriction categories § 6.1.2 Categoraical Approaches to Partiality - Partial map categories. Partial map synthed from toal maps - Partial product categories (di Paola, Heller; Robinson, Rosolini), Restriction categories (Cockett, Lack) - axiomatic approaches - Partila map classification - sometimes pmaps are the Kleisili maps of a monad on the toal map category - Recusion categories (di Paorla, Heller). Turing categories (Cockett, HExtra) - computational. § 6.1.3 Restriction Categories - For f : A → B, has f̅ : A → A, which - R1 : f ∘ f̅ = f - R2 : f̅ ∘ g̅ = g̅ ∘ f̅ - R3 : g̅ ∘ f̅ = rest(g ∘ f̅) - R4 : ... - <Looking at Agda code> type in types. Het equality. With many axioms for extensionality and quotienting. § 6.1.4 Restriction Categories: Examples § 6.1.5 Stable Systems of Monics § 6.1.6 Partial Map Categories § 6.1.7 Partial Map Categories : Examples § 6.1.8 From Partial Map Categories to Restriction category § 6.1.9 From Restriction category to Partial map cat - Needs idempotent splitting. - X ≅ Par(Total(X), M) § 6.1.10 Wrap-up - Check up the notion of stable factorization system - Check up those old papers from late 80's referred in Robin's paper, like those of Giuseppe Rossolini. - Also the relationship between Set and Rel as detailed in Peter Johnstone's book. 6.2 Bengt Nordström : Incremental Type Checking : 11.20 - 12.00, 14.00 - 15.40 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ § 6.2.1 Syntax ,---- | a ::= i | (a e) -- application, avoiding beta-redex | e ::= a | Set | Π e f | fun f | f ::= lam x e `---- § 6.2.2 Declarations ,---- | c₁ : t₁ ; ... ; cn / tn `---- § 6.2.3 Steps 1. No defined constant 2. With definition - c₁ = e₁ ; ... ; cn : tn § 6.2.4 With the usual type systems. § 6.2.5 Incremental type checking In situation ,---- | ? ∈ t `---- 1. Refinigning with constant c results in ,---- | c ?₁ ... ?n ∈ t | ?₁ ∈ A₁ ... ?n ∈ An `---- 1. Refinieng with Set is an error 2. with Π is error 3. with fun, the result is ,---- | fun (lam ?₁ ?₂) `---- § 6.2.6 Rep. of Terms under construction - is a tree with (nodes and) leaves being placeholders. - a sate is like ,---- | q₁ = c₁ q11 ... q1n1 | q₂ = c₂ q21 ... q2n2 | ... `---- plus constant declarations and definitions and constraints. § 6.2.7 Thin expressions ,---- | e ::= c q1 .. qn | | Set | | Π q q′ | | λ q' | | q | q' := lam q₁ q₂ `---- § 6.2.8 Commands from a state to state 1. q := thin-e -- refinement 2. c :: thin-e -- type declaration 3. c = thin-e -- definition 4. q₁ := q₀ -- deletion; delete what's bound to q₁ and replace with q₀ § 6.2.9 Batch type checking too complex to understand. The goal is to simplify and understand. § 6.2.10 Batch checking algorithm ,---- | -- induction over G | checkType e (G : Well typed context) : Result Ok | checkType a G = | Ok := checkObj a Set G | checkType Set G = Ok | checkType (Pi e f) G = | Ok := checkType e G | x := fresh G -- get a new constant in G | Ok := checkType (apply f x) (update G x e) | checkType (fun f) = error | ... `---- § 6.2.11 Question: In inferring type of an application (f : Pi a b)(e : a), apply b e must reduce beta-redexes. Is this avoidable? - Yes, if you take the closure value approach. - B wants values to be expressions. Can't expressions be extended? - Yes, but then you must consider their reductions too (those like explicit substitution calculus). § 6.2.12 Wrap-up - A lot of discussion on having separate worlds of expressions and values or having values to be certain expressions. - You can write in Haskell in the way BN wants to write with do-notation. - that last question above. 6.3 MT : Meta-verification and validation 16.00 - 17.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Discussed how parts of validation could be verification about properties of formal assurance cases as objects. § 6.3.1 Wrap-up Consider having composable primitives of validation / verification activities and proving something about properties of those combination. Cf. Simon Peyton Jones' paper "Composing contracts: an adventure in financial engineering." 6.4 X-Sprint : 17.00 - 18.00 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - BN: - JC: - LH: - MT: investigated the possiblities of binary distribution of Agda on Windows independent of Haskelll Platform. There seems to be no problems technically, as libraries seems to be all statically linked on Windows. Statically linked GNU GMP library etc cause problems in terms of licenses. - YK: 7 12 May Sun. ============= 7.1 Liyang Hu : Software Transactional Memory : 09.00 - 11.40 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ § 7.1.1 Background (1hr) - IO monad, IORef a ,---- | data IO a = ... | data IORef a = ... `---- - STM monad, TVar a ,---- | data STM a = ... | instance Monad STM where ... | data TVar a = ... | readTVar :: TVar a → STM a | writeTVar :: a → TVar a → STM() | atomically :: STM a → IO a | retry :: STM a | orElse :: STM a → STM a → STM a | forkIO :: IO () → IO () `---- § 7.1.2 The Language (Hutton's Razor) - STM level ,---- | data Expression′ : Set where | #_ : (m : ℕ) → Expression′ | _⊕_ : (a b : Expression′) → Expression′ | read : (v : Variable) → Expression′ | write : (v : Variable)(e : Expression′) → Expression′ `---- - IO level ,---- | data Expression | #_ : (m : ℕ) → Expression | _⊕_ : (a b : Expression) → Expression | atomic : (e : Expression′) → Expression `---- - No fork, but instead non-deterministic semantics. § 7.1.3 Heaps and Variables ,---- | postulate ∣Heap∣ : ℕ | Heap : Set | Heap = Vec ℕ ∣Heap∣ | Variables = Fin ∣Heap∣ `---- § 7.1.4 1 step reduction (↦ ~ "stop the world semantics") ,---- | data _↦′_ : Rel(Heap × Expression′) | ↦′-⊕ℕ : ∀ {h m n} → (h , # m) ⊕ # n ↦′ (h, #(m + n)) | ... | ↦′-read : h , reav v ↦′ h , # h[v] | ↦′-write : h , write v (# n) ↦′ h [ v ]:= m , # m | ... `---- § 7.1.5 Action τ silent action c2 c3 § 7.1.6 Labeled Transition System Action → Rel(Heap × Expression) ↦-atomic : ∀ {h e h' e'} → (e↦*m : h, e ↦* h' , # m) → (c3 ▷ h , atomic e) ↦ (h' , # m) ↦-mutate : ∀ h' {h e} → (τ ▷ h , atomic e) ↦ (h' , atomic e) § 7.1.7 Transaction Log and Consistency - Log-based implementation of transaction: read-log and wright-log ,---- | data Logs : Set where | constrocutre _&_ | field | ρ ω : Vec (Maybe ℕ) ∣HEap∣ | | Write : Logs → Variables → ℕ → Logs | Read : Heap → Logs Variable → Logs × ℕ | -- check if you yourself have written; then return that | .. ow, check if you have read before; then return that | .. ow, read heap and record that fact in read log. `---- § 7.1.8 Consistency ,---- | Consistent: Heap → Logs → Set | Consistent h (ρ & _) = ∀ v m → ρ [ v ] ≡ Just m → h [ v ] ≡ m `---- Consistency is decidable - sicne Heap is finite. ,---- | Update-lookup : Heap → Logs → Variable → ℕ | -- if you have written, what you wrote; else read from heap | Update h l = tabulate (Update-lookup h l) `---- § 7.1.9 Log-Based Semantics (↣ ~ log-based, non-stop-the-world semantics) Heap are not updated by this one-step (write goes to log) - STM level ,---- | data _⊢_↣′_ (h : Heap) : Rel(Logs × Expression′) where | ... `---- - IO level ,---- | TState = Maybe (Expression′ × Log) | data _▷_↣_ : Action → Rel(Heap × TState × Expression) | .... `---- ↣-mutate allows heap to be changed in anyway. § 7.1.10 Bisimilarity of Semantics (between ↦ version and ↣ version) 7.2 X-Sprint : All : 14.00 - 17.30 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 7.3 Wrap up ~~~~~~~~~~~ 7.4 JC and MT: ~~~~~~~~~~~~~~ Discussed copatterns and termination/productivity. 7.5 YK and JC: ~~~~~~~~~~~~~~ - Looked at Agda formalisation of each other on - Category theory, Yoneda lemma - Normalisation by Evaluation - Planning to put up a category theory library on a git hub. 7.6 SK ~~~~~~ Formalising Granstroem's worlds. 20% remaining. 7.7 JC and SK and MT ~~~~~~~~~~~~~~~~~~~~ Pullback. Discussed the situation of ,---- | DirectedContainer ---------> Comonad Set | | | | | | | v v | Container -----------------> Endo Set `---- in the context of JG's Worlds. There's a progression of ,---- | World --> Endo Set --> Mnd Set | w ⟦w⟧ w=>_ `---- 8 13 May Mon. ============= 8.1 X-Sprint, Wrap-up ~~~~~~~~~~~~~~~~~~~~~ § 8.1.1 SK: Agda code formalising Granström's World World, world map, composition, id, unit-laws, lifting-laws, § 8.1.2 LH: Discussion on formulation of bisimilarity § 8.1.3 JC, MT, BN: nothing to add to yesterday § 8.1.4 YK: Yoneda lemma and NbE for category - NbE for monoid expression via Yoneda applied to monoids as 1-object categories, using free monoid on "strict setoids" - NbE for path expression of a graph free categories on a graph. 8.2 Next AIM Discussion: ~~~~~~~~~~~~~~~~~~~~~~~~ It would be good to have the next AIM in Gothenburg. BN will talk with Ulf and Nisse about dates / place in Gothenburg to make sure they can attend.