--- Day changed Wed Jun 21 2017 | ||

Saizan | dolio: yeah, there's been work in the last 10 years allowing proof-relevant relations, and indeed the proof you get depends on the original function, but that proof itself is well-behaved and you can capture that by using cubical sets instead of just reflexive graphs | 21/06 09:12 |
---|---|---|

Saizan | (maybe 5 years, recent but not super so) | 21/06 09:12 |

Saizan | ziman: are you familiar with coherence spaces? | 21/06 14:34 |

ziman | Saizan: not at all, unfortunately | 21/06 15:49 |

pgiarrusso | dolio: just read your comments from yesterday on the logs, sounds cool! Sorry I had to go | 21/06 21:16 |

pgiarrusso | I can't visualize all details in my head but I get the idea... I knew a bit about fibrations and about natural numbers object (which seem just a special case of initial algebras, though nobody says so) | 21/06 21:18 |

pgiarrusso | but I never knew about this combination | 21/06 21:18 |

dolio | I have a file with it written up in more detail I could put somewhere if you want to read it. It's got a bunch of half-baked coinduction ideas that I haven't finished yet in it, though. | 21/06 21:20 |

pgiarrusso | which, IIUC, says that you can use the categorical analogue of fold (given an algebra F A -> A there exists an arrow mu F -> A) | 21/06 21:20 |

pgiarrusso | dolio: I'm in no hurry with this and should finish my thesis, but if you feel like publishing it I'd be curious :-) | 21/06 21:21 |

pgiarrusso | OTOH, I might just be too lazy for this, but I doubt I'll ever manage to *use* such fancy math. In comparison, right now I'm impressed by how easy it was to use step-indexed logical relations | 21/06 21:23 |

dolio | Well, the reason I did it was that I was hoping by working through the connection between type theory induction and category theory induction very carefully, it'd give me ideas about how to have fancier uses of coinduction in type theory (because I'm not really satisfied with what I've seen so far). But I haven't come up with anything yet. | 21/06 21:28 |

Nik05 | mietek thanks for all the link | 21/06 21:28 |

dolio | I at least fully understand why 'just do the same thing as induction' doesn't get you something, though. | 21/06 21:29 |

Nik05 | I get the idea of monads, but I think I see some mistakes in Pfennings lectures, although I am sure he is probably not making any mistakes | 21/06 21:29 |

Nik05 | Maybe his pdfs are more clear | 21/06 21:29 |

Nik05 | clearer* | 21/06 21:30 |

pgiarrusso | dolio: I used to hear "Set isn't self-dual, so you can't just dualize algebra and get coalgebra for free" | 21/06 21:41 |

dolio | That doesn't seem like a very illuminating explanation. :) | 21/06 21:42 |

pgiarrusso | dolio: that's what I remember from Prof. Peter Gumm, but I won't claim I understand it | 21/06 21:43 |

pgiarrusso | but honestly it does fit with many categorical insights they tend to need a bit of unpacking | 21/06 21:44 |

dolio | I mean, I can concoct ways that it's related to the specific thing I ended up with. | 21/06 21:45 |

carter | Does enabling agdas type in type flag let me have impredicative polymorphism? | 21/06 21:45 |

carter | Or is there a subtlety that I'm over looking? | 21/06 21:45 |

carter | Trying to figure out the lowest pain way to deal with variables in an ast model :) | 21/06 21:46 |

dolio | The problem is that what induction is letting you do is construct a map from `id : Nat -> Nat` to `t : T -> Nat`. id is the terminal object in the slice category, which means it's the family with exactly one value in each 'fiber'. | 21/06 21:47 |

dolio | Which is an interesting thing to do. | 21/06 21:47 |

dolio | Coinduction lets you get a map in the opposite direction, but you already had one, so it isn't interesting. | 21/06 21:47 |

dolio | Actually, it's even worse than you already had one. The one you already had is the unique one that exists. | 21/06 21:48 |

dolio | So, that's probably related to the fact that monoids in set are interesting, but every set is a comonoid in exactly one, boring way. | 21/06 21:51 |

dolio | Etc. | 21/06 21:51 |

pgiarrusso | carter: type in type should include impredicative polymorphism, yes, but that's not enough if you're aiming to handle variables with HOAS | 21/06 21:56 |

pgiarrusso | carter: have you considered (typed/scoped) de Bruijn indexes? | 21/06 21:57 |

pgiarrusso | also, do you need substitution or can you get by with environments of values | 21/06 21:57 |

pgiarrusso | ? | 21/06 21:57 |

carter | pgiarrusso: phoas dodges positivity issues afaik | 21/06 21:59 |

carter | pgiarrusso: what's the least painful basic description of system f or something bigger I can look at? | 21/06 21:59 |

pgiarrusso | carter: yes, but IIRC that doesn't need impredicative polymorphism (though I'm not 100% sure, PHOAS is for Coq which has some of it) | 21/06 21:59 |

carter | pgiarrusso: it does for system f | 21/06 22:00 |

carter | Unless when I was trying to do it two years ago I was fucking up ) | 21/06 22:00 |

pgiarrusso | carter: https://github.com/sstucki/system-f-agda | 21/06 22:00 |

pgiarrusso | I think that one is not the least painful around, but it works | 21/06 22:01 |

pgiarrusso | carter: see https://github.com/sstucki/system-f-agda/blob/master/src/README.agda for a description | 21/06 22:02 |

pgiarrusso | that one's only using well-scoped indexes | 21/06 22:02 |

carter | pgiarrusso: i have a slightly richer than system f calculus that does linear logic things, and i want to do the simplest / easiest possible proof that i can erase info from the fancier typing derivation tree and get a system f well typed term | 21/06 22:02 |

carter | pgiarrusso: the original phoas stuff that did system f did require impredicative set to type check | 21/06 22:03 |

carter | last i tried to poke at it / adapt it to lean or agda | 21/06 22:04 |

pgiarrusso | carter: uh I see | 21/06 22:04 |

pgiarrusso | carter: I'm not the most expert here and I've never done System F myself | 21/06 22:04 |

carter | pgiarrusso: try it out | 21/06 22:04 |

carter | :) | 21/06 22:04 |

pgiarrusso | I'm not surprised | 21/06 22:04 |

carter | i think theres some ways of indexing types by number/depth of quantfiers or something might side step the issue | 21/06 22:05 |

carter | or using sized types? | 21/06 22:05 |

carter | idk | 21/06 22:05 |

pgiarrusso | but I wanted to say: while I'm not the most expert, that feels well-suited for de Bruijn | 21/06 22:05 |

carter | yes | 21/06 22:06 |

carter | otoh, i'm also keen on trying to be as lazy as possible :0 | 21/06 22:06 |

pgiarrusso | oh well... do you have a clue if you need any permutation/swapping lemmas? | 21/06 22:06 |

carter | but yeah, its probably gonna wind up being debruijn | 21/06 22:06 |

carter | why would i? | 21/06 22:06 |

carter | :) | 21/06 22:06 |

carter | context? | 21/06 22:06 |

pgiarrusso | I think that codebase has pretty much *all* of those lemmas, just in case, the guy is not lazy :-) | 21/06 22:07 |

carter | ultimately want the interesting bit to be a function "erasingLinearityGivesWellTypedSystemFThing : Linear System F derivation tree -> SystemF derivation tree" | 21/06 22:07 |

pgiarrusso | carter: I'm not saying *I* would have the discipline to figure that out in advance, but if you can it does save time | 21/06 22:07 |

carter | and then say "by totality, this is sound" | 21/06 22:08 |

carter | :) | 21/06 22:08 |

carter | this was still helpful | 21/06 22:08 |

carter | thx | 21/06 22:08 |

carter | me and a colleague are doing some formal proofs for a large project we're kicking off | 21/06 22:08 |

carter | trying to do the sanest / easiest appraoch possible | 21/06 22:08 |

carter | so we can get it down | 21/06 22:08 |

carter | done | 21/06 22:08 |

carter | ttyl :) | 21/06 22:08 |

pgiarrusso | carter: oh, have you looked at Tiark's stuff? | 21/06 22:09 |

pgiarrusso | sorry, will let you go | 21/06 22:09 |

carter | He has proof stuff? | 21/06 22:09 |

carter | I tried looking at the truffle stuff once and gave up 5 seconds into the code base | 21/06 22:09 |

carter | Link please ? | 21/06 22:10 |

carter | :) | 21/06 22:10 |

carter | pgiarrusso: I assume you mean proof stuff? | 21/06 22:10 |

pgiarrusso | carter: yes, with Nada http://doi.acm.org/10.1145/3009837.3009866 | 21/06 22:11 |

pgiarrusso | his F<: definition uses definitional interpreters and environments, some links here: https://github.com/TiarkRompf/minidot/blob/529ef538929f204ec0d8a26534fd533e1890cfdf/README.md | 21/06 22:14 |

pgiarrusso | carter: (1) copy-pasting and extending that deBruijn code might give you a proof quicker (2) using environments instead of substitution, if you can pull it off, can give much simpler proofs, but it doesn't do everything | 21/06 22:15 |

carter | i dont care about anything but getting that one function and associated type derivation model working :) | 21/06 22:16 |

carter | g2g, thx for the links | 21/06 22:16 |

pgiarrusso | his actual Coq code OTOH uses locally nameless approach, and (1) I've seen nobody use it in Agda (2) using it in Coq with more than one variable sort can get annoying | 21/06 22:16 |

pgiarrusso | HTH | 21/06 22:16 |

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