--- Day changed Wed Jan 25 2017
mietekpgiarrusso: simple products? It’s trivial25/01 00:02
mietekpgiarrusso: https://mietek.github.io/hilbert-gentzen/html/BasicIPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution.html#125/01 00:02
pgiarrussomietek: just the obvious rules right? That’s what I seemed to recall, a colleague was asking 25/01 00:03
pgiarrussoyeah, I found that file :-)25/01 00:03
pgiarrussoaugur: ah sorry, the Q (now answered) was: “how hard is adding products to hereditary substitution for STLC? I seem to remember it is not hard but I’ve seen this discussed on IRC (here or in #dependent, not sure…)”25/01 00:03
mietekpgiarrusso: is there anything I can clear up about it?25/01 00:03
mietekBTW, I spoke with @reifyreflect about hereditary substitution and he was convinced it is a form of normalisation by evaluation; in fact, IINM, he thinks that everything is a form of NbE25/01 00:04
mietekIf you look at the `expand` function in my code, you can see it’s induction on the type25/01 00:04
auguroh, i dont know anything about hereditary substitution25/01 00:04
pgiarrussomietek: the question was sth. like ‘do you know a paper like “Hereditary Substitutions for Simple Types, Formalized” but with products?” — I guess I was only missing a comment confirming the status25/01 00:05
mietekPretty much exactly like `reifyᶜ` here: https://mietek.github.io/hilbert-gentzen/html/BasicIPC.Metatheory.GentzenNormalForm-KripkeMcKinseyTarski.html#126525/01 00:05
pgiarrussoaugur: ah sorry, I was confused25/01 00:05
mietekpgiarrusso: ah. I’m almost certain there isn’t a paper, or I would’ve found it, back when I was pestering gallais to help me with this.25/01 00:05
pgiarrussomietek: OK, you were talking with gallais about this, I see :-)25/01 00:06
mietekYes, I think I must credit gallais with the actual ideas behind my implementations25/01 00:06
mietekAlso with hsubst for S425/01 00:07
auguri really should read up on it some time25/01 00:07
auguri hear conor has a nice paper or two25/01 00:07
mietekOn hsubst?!25/01 00:07
pgiarrussomietek: re NbE and HSubst, you and reifyreflect are already aware of http://www.larrytheliquid.com/drafts/sbe.pdf right? Not that I really read it but it claims new ideas, in particular NbE restricted to canonical forms is more related to hsubst :-)25/01 00:07
mietekpgiarrusso: I read that some time ago and found it unsatisfactory, but I don’t remember why now25/01 00:08
mietek(reifyreflect isn’t on IRC, AFAIK)25/01 00:09
mietek(https://twitter.com/reifyreflect)25/01 00:09
pgiarrussoyeah found that, thanks25/01 00:10
mietekHe did his PhD on NbE25/01 00:10
augurmietek: yes, and i believe you've shown it to me before. maybe not. does SOT sort by author? i think you might have it there25/01 00:11
pgiarrussomietek: I also remember I was confused by your/gallais’s hsubst on sums… does it work by not dealing with commuting conversions?25/01 00:12
mietekaugur: I’m not aware of a Conor paper discussing hsubst25/01 00:12
auguroh i think it was rensub, but maybe that doesnt do hereditary stuff25/01 00:13
mietekaugur: ah, yes.25/01 00:13
pgiarrussomietek: didn’t Conor also have hsubst in his notes?25/01 00:13
pgiarrussore sums, I was hinting at https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Metatheory/GentzenSpinalNormalForm-HereditarySubstitution.agda (and some file in gallais poutpourri)25/01 00:14
mietekpgiarrusso: yes, but not a paper :)25/01 00:14
mietekpgiarrusso: and it’s almost the same as the things explained in Keller-Altenkirch 2010, but not quite25/01 00:14
mietekpgiarrusso: I know what you’re referring to… let me see if I can answer :)25/01 00:15
pgiarrussoOh, I guess the canonical answer should be https://pdfs.semanticscholar.org/9bcf/268a869dfb3a95e5055f22127e0aa0edb8c7.pdf (cited by https://github.com/gallais/potpourri/blob/master/agda/papers/hs99/STLCSum.agda) and variants25/01 00:17
pgiarrusso(just found it)25/01 00:17
mietekpgiarrusso: well, then I’m double-confused now25/01 00:18
mietekpgiarrusso: IINM, this is what my code does, and more25/01 00:18
mietekpgiarrusso: Cs is _⊢ᵗᵖ_⦙_ (spine tip) in my code25/01 00:19
mietekpgiarrusso: the idea with the _⊢ˢᵖ_⦙_ and _⊢ᵗᵖ_⦙_ notation is that the type on the left of the `⦙` is as if it was part of the context25/01 00:20
mietekpgiarrusso: the structure of the spines should be reminiscent of sequent calculus25/01 00:21
mietekpgiarrusso: if you only just found Joachimski-Matthes, what were you confused about previously?25/01 00:21
pgiarrussoOh, I remember I had asked that question ages ago, but never understood the answer25/01 00:22
mietekWell, I think it actually does handle commuting conversions25/01 00:24
mietekYou can see that happening in the `reduce` function in my code25/01 00:24
mietek`reduce (neⁿᶠ (spⁿᵉ i xs boomᵗᵖ))       nilˢᵖ        y            = neⁿᶠ (spⁿᵉ i xs boomᵗᵖ)`25/01 00:25
mietekLet’s take bottom elimination (`boom`) as an example25/01 00:25
pgiarrussoWait I see the syntax and got a guess25/01 00:25
mietekIn this case, we’re supposed to do something about a spine that has `boom` at the tip25/01 00:26
pgiarrussoI’m not sure what to expect of `boom`25/01 00:27
pgiarrussobut I see that `case` is only in spine tips25/01 00:27
mietekWell, it’s the explosion principle, right?25/01 00:27
mietekIt’s the intuitionistic eliminator for the empty type.25/01 00:27
pgiarrussoyeah, but what are the commuting conversions for it… ah OK, it pops up?25/01 00:28
mietekIntuitively, if you have a `boom` that is not at the root of a proof tree, you have something to optimise away25/01 00:28
mietekBecause if you can get anything, then you might as well get the thing that you really want25/01 00:28
mietekSo, in the case I pasted above, when we see a `boom` at the end of a spine, we just ignore whatever was supposed to be the tip25/01 00:30
mietekBecause `boom` is going to be the new tip25/01 00:30
mietekThis is the simplest of the rules in General Elimination form25/01 00:31
mietekAll of the rules in GE form are problematic25/01 00:31
mietekOver there in the NbE world, Danko Ilik uses Kripke-CPS models to deal with them25/01 00:32
mietekhttps://mietek.github.io/hilbert-gentzen/html/IPC.Semantics.KripkeExploding.html#125/01 00:32
mietekhttps://mietek.github.io/hilbert-gentzen/html/IPC.Metatheory.GentzenNormalForm-KripkeExploding.html#125/01 00:32
mietekThis also turns out to be the thing necessary to do NbE for S4, with the correct operational behaviour25/01 00:33
mietekI hope to write something about this soon25/01 00:33
pgiarrussoso wait, you use CPS so you can throw away some continuation when you encounter a boom, like here you throw away stuff?25/01 00:34
mietekI can’t confirm that, but it sounds likely25/01 00:34
mietekThe CPS code is still a bit too opaque to me25/01 00:34
mietekI do have a clearer version of it here25/01 00:34
mietekhttps://gist.github.com/mietek/075f0a3c10087c04e3b52ea68deb490325/01 00:35
pgiarrussoMeanwhile: a spine Γ ⊢ˢᵖ B ⦙ C has a hole of type B and produces a C, while a tip Γ ⊢ᵗᵖ B ⦙ C provides a B into such a spine?25/01 00:36
pgiarrussoBTW, the C param in  Γ ⊢ᵗᵖ B ⦙ C seems unused (which is why I didn’t mention it)25/01 00:37
mietekI’m not sure this reading is correct25/01 00:37
mietekWhy do you think C seems unused?25/01 00:37
mietekC is the thing that we really want to get out of the whole spine, tip included25/01 00:38
pgiarrussoC is clearly used in the spine, it’s not clear why it’s in the tip25/01 00:38
mietekThink of the tip as a spine attached to the end of the regular spine25/01 00:39
pgiarrussoLooking at tips in https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Syntax/GentzenSpinalNormalForm.agda, it seems I can convert any Γ ⊢ᵗᵖ B ⦙ C to Γ ⊢ᵗᵖ B ⦙ D for any C and D25/01 00:39
pgiarrussoI see you match Γ ⊢ˢᵖ B ⦙ C and Γ ⊢ᵗᵖ B ⦙ C25/01 00:40
mietekSorry, which lines or functions are you looking at?25/01 00:40
pgiarrussoI suggest that (unless I miss sth.) you only need match Γ ⊢ˢᵖ B ⦙ C and Γ ⊢ᵗᵖ B25/01 00:40
pgiarrussowell, 25/01 00:41
pgiarrussolooking at https://github.com/mietek/hilbert-gentzen/blob/master/IPC/Syntax/GentzenSpinalNormalForm.agda#L44-L4925/01 00:41
pgiarrussoand OK, my claim is wrong for `nil`25/01 00:41
mietekI didn’t understand your comment about matching25/01 00:42
mietekThink about `boom` again; it’s the simplest case25/01 00:42
pgiarrussoYeah, that comment was nonsense25/01 00:42
mietekIn a proof tree that is in normal form, any `boom` will come after all the non-problematic eliminators25/01 00:43
mietekHence, the spine, and the second spine (tip)25/01 00:43
mietek(normal/neutral form)25/01 00:43
pgiarrussoOK: a spine Γ ⊢ˢᵖ B ⦙ C has a hole of type B and produces a C25/01 00:44
mietek(i.e. non-canonical form)25/01 00:44
pgiarrussois that part correct?25/01 00:44
mietekYes, I think so, although I find the concept of a hole in the spine disturbing :)25/01 00:44
mietekBTW, this is probably more suitable for ##dependent25/01 00:45
pgiarrussoyeah right, sorry for the others!25/01 00:45
arjen-jonathanMorning all25/01 10:48
arjen-jonathanI'm looking for some example usages of indexed monads in Agda25/01 10:49
arjen-jonathanAnyone have a pointer to some code?25/01 10:49
apostolisDoes anyone know when to use the /inf Size type in Coinductive data?25/01 20:52
apostolisGiven that for i : Size =>   \inf < i 25/01 20:53
apostolis\inf is a subtype of i, thus in any case that we care about the size, we cannot have functions that take \inf, since i is not the subtype of \inf, but the opposite.25/01 20:54
apostolisI think I found the asnwer. The problem is that I am defining the datatypes before having learned how to use sized types to prove productivity.25/01 21:14
apostolisI need to find in which places will Sized types be important in proving productivity and not use \inf in these functions.25/01 21:15
apostolisBye25/01 21:16

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