--- 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/700ac43666a40ae24d8723b32c55e794 | 28/04 12:32 |
---|---|---|

akr[m] | also including an example of what I'm trying to achieve | 28/04 12:32 |

akr[m] | and I'm wondering if there is a better way / more concise way | 28/04 12:33 |

akr[m] | for example I'm not very happy that the datatype Form is indexed by another data type | 28/04 12:33 |

comietek | Struct? Is isomorphic with Bool | 28/04 12:35 |

akr[m] | sure | 28/04 12:35 |

comietek | which suggests to me that you could have two separate Form datatypes, instead of one with an extra bit | 28/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 |

comietek | I don't know | 28/04 12:36 |

comietek | how do you define better? | 28/04 12:36 |

akr[m] | easier to work with | 28/04 12:37 |

comietek | I would look for a close correspondence with source material | 28/04 12:37 |

akr[m] | what do you mean? source material? | 28/04 12:38 |

comietek | I suppose if you are developing new ideas then there is none | 28/04 12:40 |

akr[m] | ah | 28/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 state | 28/04 12:41 |

comietek | what is the meaning of Struct? and Form? | 28/04 12:41 |

comietek | right, I see now | 28/04 12:44 |

comietek | does 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 |

comietek | can you not just define it as a function on Form? | 28/04 12:45 |

comietek | then you would take an equality proof | 28/04 12:45 |

akr[m] | hmm, I guess that could work | 28/04 12:46 |

akr[m] | of course I'm not sure if that's easier or harder to work with :P | 28/04 12:46 |

comietek | it really depends what you mean by work | 28/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 reactions | 28/04 12:47 |

comietek | functions in return types give rise to green slime | 28/04 12:48 |

comietek | but as a prerequisite, should be fine | 28/04 12:48 |

comietek | just try it and ask if you run into trouble | 28/04 12:48 |

akr[m] | alright, I will | 28/04 12:48 |

akr[m] | thank you | 28/04 12:48 |

comietek | augur would tell you to think about the judgmental structure of the system first | 28/04 12:49 |

comietek | what are you judgments and what do they say? | 28/04 12:49 |

comietek | your* | 28/04 12:50 |

jacobian | DEFENCE. : 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] | hmm | 28/04 12:51 |

jacobian | ^ From the court trial of Paul Murphy TD | 28/04 12:51 |

akr[m] | the most tricky judgment is one of "specialization", for example: | 28/04 12:51 |

jacobian | Woops | 28/04 12:51 |

jacobian | wrong chan :) | 28/04 12:51 |

jacobian | <comietek> functions in return types give rise to green slime | 28/04 12:52 |

jacobian | Is 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 p | 28/04 12:52 |

comietek | jacobian: inasmuch as the work of Conor McBride is canon, yes | 28/04 12:53 |

comietek | and it is | 28/04 12:53 |

jacobian | Excellent | 28/04 12:54 |

comietek | akr[m]: I can't brain that today | 28/04 12:54 |

jacobian | Green slime is a pain | 28/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₁ where | 28/04 12:56 |

akr[m] | doesn't really work | 28/04 12:57 |

akr[m] | because you have to specify just what kind of Form are you taking in each judgment | 28/04 12:57 |

akr[m] | and it gets really bad when you have something like | 28/04 12:58 |

akr[m] | ⊗Introₗ : ∀ {A B C} → A ⊕ B ⊢ C → A ⊗ B ⊢ C | 28/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 equivalence | 28/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 either | 28/04 13:05 |

akr[m] | :| | 28/04 13:05 |

akr[m] | hmm, I wonder how's this: https://gist.github.com/osense/700ac43666a40ae24d8723b32c55e794 | 28/04 13:17 |

akr[m] | I guess it'll lead to something freaky somewhere down the line | 28/04 13:18 |

quchen | It’s possible to express existential quantification via two universals. Is the reverse direction also true? | 28/04 16:33 |

quchen | As a theorem, | 28/04 16:33 |

quchen | ∀-to-∃ : ∀ {α β γ} {A : Set α} {P : A → Set β} → (f : ∀ (y : Set γ) → (∀ (x : A) → P x → y) → y) → ∃ P | 28/04 16:33 |

quchen | I should paste this somewhere I guess ;-) | 28/04 16:33 |

quchen | http://lpaste.net/355037 | 28/04 16:33 |

quchen | I can’t seem to find a proof for the latter. | 28/04 16:33 |

gallais | quchen: Is there a reason why the quantifier for `γ` is outside of `f`? | 28/04 16:48 |

gallais | because if it's inside then it's trivial to prove | 28/04 16:48 |

gallais | (just pick `y = ∃ P`) | 28/04 16:48 |

dolio | quchen: Those two types are only interchangeable with impredicativity. | 28/04 17:03 |

dolio | With predicative universes, your forall construction is not actually encoding all the capabilities of the existential quantifier. | 28/04 17:05 |

dolio | Or, alternately, the existential quantifier has too many capabilities that your forall construction does not. | 28/04 17:07 |

quchen | dolio: Ah, I see. Thanks. | 28/04 17:14 |

dolio | Basically, `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!