--- Day changed Fri Apr 28 2017
akr[m]Hello, I'm trying to define the syntax for a somewhat freaky language in Agda and here is what I came up with: https://gist.github.com/osense/700ac43666a40ae24d8723b32c55e79428/04 12:32
akr[m]also including an example of what I'm trying to achieve28/04 12:32
akr[m]and I'm wondering if there is a better way / more concise way28/04 12:33
akr[m]for example I'm not very happy that the datatype Form is indexed by another data type28/04 12:33
comietekStruct? Is isomorphic with Bool28/04 12:35
akr[m]sure28/04 12:35
comietekwhich suggests to me that you could have two separate Form datatypes, instead of one with an extra bit28/04 12:35
akr[m]hmm, but why would it be better / how would it be better than having one indexed data type?28/04 12:36
comietekI don't know28/04 12:36
comietekhow do you define better?28/04 12:36
akr[m]easier to work with28/04 12:37
comietekI would look for a close correspondence with source material28/04 12:37
akr[m]what do you mean? source material?28/04 12:38
comietekI suppose if you are developing new ideas then there is none28/04 12:40
akr[m]ah28/04 12:40
akr[m]well, it's supposed to model chemical compounds made up of different parts where each part can be in a different state28/04 12:41
comietekwhat is the meaning of Struct? and Form?28/04 12:41
comietekright, I see now28/04 12:44
comietekdoes Struct? need to be an index?28/04 12:45
akr[m]well, I don't know how else to define _⟨⊳⟩28/04 12:45
comietekcan you not just define it as a function on Form?28/04 12:45
comietekthen you would take an equality proof28/04 12:45
akr[m]hmm, I guess that could work28/04 12:46
akr[m]of course I'm not sure if that's easier or harder to work with :P28/04 12:46
comietekit really depends what you mean by work28/04 12:46
akr[m]e.g. next step is to define a proof system based on linear logic which allows you to derive valid chemical reactions28/04 12:47
comietekfunctions in return types give rise to green slime28/04 12:48
comietekbut as a prerequisite, should be fine28/04 12:48
comietekjust try it and ask if you run into trouble28/04 12:48
akr[m]alright, I will28/04 12:48
akr[m]thank you28/04 12:48
comietekaugur would tell you to think about the judgmental structure of the system first28/04 12:49
comietekwhat are you judgments and what do they say?28/04 12:49
comietekyour*28/04 12:50
jacobianDEFENCE. : was labour party not destroyed in elections because of your treachery by voters.  Joan Burton: No it was populist groups setting out to destroy social democracy its a world wide phenomenon.28/04 12:51
akr[m]hmm28/04 12:51
jacobian^ From the court trial of Paul Murphy TD28/04 12:51
akr[m]the most tricky judgment is one of "specialization", for example:28/04 12:51
jacobianWoops28/04 12:51
jacobianwrong chan :)28/04 12:51
jacobian<comietek> functions in return types give rise to green slime28/04 12:52
jacobianIs this a technical term? 28/04 12:52
akr[m](St S)   ⊢   (St S)        gets turned into          (St S) ⟨ A ⊳ u ⟩   ⊢  (St S) ⟨ A ⊳ p ⟩28/04 12:52
akr[m]i.e. A inside S has changed state from u to p28/04 12:52
comietekjacobian: inasmuch as the work of Conor McBride is canon, yes28/04 12:53
comietekand it is28/04 12:53
jacobianExcellent28/04 12:54
comietekakr[m]: I can't brain that today28/04 12:54
jacobianGreen slime is a pain28/04 12:54
akr[m]comietek: so if you have indexed Form. then already this is a problem, e.g.28/04 12:56
akr[m]data ⊢ : Form _ → Form _ → Set₁ where28/04 12:56
akr[m]doesn't really work28/04 12:57
akr[m]because you have to specify just what kind of Form are you taking in each judgment28/04 12:57
akr[m]and it gets really bad when you have something like28/04 12:58
akr[m]⊗Introₗ : ∀ {A B C} → A ⊕ B ⊢ C → A ⊗ B ⊢ C28/04 12:58
akr[m]because Agda can't infer what are `A` and  `B` backwards from `A ⊕ B`28/04 12:58
akr[m](even though it doesn't matter)28/04 13:01
akr[m]also I don't see how to make this work with equivalence28/04 13:03
akr[m]I think it might be best to have two forms of _⟨⊳⟩28/04 13:03
akr[m]one for when you're applying it to (St S) and one when you're already applying it to some  α ⟨ A ⊳ a⟩28/04 13:04
akr[m]no wait that doesn't make sense either28/04 13:05
akr[m]:|28/04 13:05
akr[m]hmm, I wonder how's this: https://gist.github.com/osense/700ac43666a40ae24d8723b32c55e79428/04 13:17
akr[m]I guess it'll lead to something freaky somewhere down the line28/04 13:18
quchenIt’s possible to express existential quantification via two universals. Is the reverse direction also true?28/04 16:33
quchenAs a theorem,28/04 16:33
quchen∀-to-∃ : ∀ {α β γ} {A : Set α} {P : A → Set β} → (f : ∀ (y : Set γ) → (∀ (x : A) → P x → y) → y) → ∃ P28/04 16:33
quchenI should paste this somewhere I guess ;-)28/04 16:33
quchenhttp://lpaste.net/35503728/04 16:33
quchenI can’t seem to find a proof for the latter.28/04 16:33
gallaisquchen: Is there a reason why the quantifier for `γ` is outside of `f`?28/04 16:48
gallaisbecause if it's inside then it's trivial to prove28/04 16:48
gallais(just pick `y = ∃ P`)28/04 16:48
dolioquchen: Those two types are only interchangeable with impredicativity.28/04 17:03
dolioWith predicative universes, your forall construction is not actually encoding all the capabilities of the existential quantifier.28/04 17:05
dolioOr, alternately, the existential quantifier has too many capabilities that your forall construction does not.28/04 17:07
quchendolio: Ah, I see. Thanks.28/04 17:14
dolioBasically, `Exists P` is initial, and the forall thing is only initial with respect to things that fit in Set gamma.28/04 17:18

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!