--- Day changed Wed Jun 21 2017
Saizandolio: 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 graphs21/06 09:12
Saizan(maybe 5 years, recent but not super so)21/06 09:12
Saizanziman: are you familiar with coherence spaces?21/06 14:34
zimanSaizan: not at all, unfortunately21/06 15:49
pgiarrussodolio: just read your comments from yesterday on the logs, sounds cool! Sorry I had to go21/06 21:16
pgiarrussoI 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
pgiarrussobut I never knew about this combination21/06 21:18
dolioI 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
pgiarrussowhich, 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
pgiarrussodolio: 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
pgiarrussoOTOH, 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 relations21/06 21:23
dolioWell, 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
Nik05mietek thanks for all the link21/06 21:28
dolioI at least fully understand why 'just do the same thing as induction' doesn't get you something, though.21/06 21:29
Nik05I 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 mistakes21/06 21:29
Nik05Maybe his pdfs are more clear21/06 21:29
Nik05clearer*21/06 21:30
pgiarrussodolio: 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
dolioThat doesn't seem like a very illuminating explanation. :)21/06 21:42
pgiarrussodolio: that's what I remember from Prof. Peter Gumm, but I won't claim I understand it21/06 21:43
pgiarrussobut honestly it does fit with many categorical insights — they tend to need a bit of unpacking21/06 21:44
dolioI mean, I can concoct ways that it's related to the specific thing I ended up with.21/06 21:45
carterDoes enabling agdas type in type flag let me have impredicative polymorphism?21/06 21:45
carterOr is there a subtlety that I'm over looking?21/06 21:45
carterTrying to figure out the lowest pain way to deal with variables in an ast model :)21/06 21:46
dolioThe 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
dolioWhich is an interesting thing to do.21/06 21:47
dolioCoinduction lets you get a map in the opposite direction, but you already had one, so it isn't interesting.21/06 21:47
dolioActually, it's even worse than you already had one. The one you already had is the unique one that exists.21/06 21:48
dolioSo, 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
dolioEtc.21/06 21:51
pgiarrussocarter: 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
pgiarrussocarter: have you considered (typed/scoped) de Bruijn indexes?21/06 21:57
pgiarrussoalso, do you need substitution or can you get by with environments of values21/06 21:57
pgiarrusso?21/06 21:57
carterpgiarrusso: phoas dodges positivity issues afaik21/06 21:59
carterpgiarrusso: what's the least painful basic description of system f or something bigger I can look at?21/06 21:59
pgiarrussocarter: 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
carterpgiarrusso: it does for system f21/06 22:00
carter Unless when I was trying to do it two years ago I was fucking up )21/06 22:00
pgiarrussocarter: https://github.com/sstucki/system-f-agda21/06 22:00
pgiarrussoI think that one is not the least painful around, but it works21/06 22:01
pgiarrussocarter: see https://github.com/sstucki/system-f-agda/blob/master/src/README.agda for a description21/06 22:02
pgiarrussothat one's only using well-scoped indexes21/06 22:02
carterpgiarrusso:  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 term21/06 22:02
carterpgiarrusso:  the original phoas stuff that did system f did require impredicative set to type check21/06 22:03
carterlast i tried to poke at it / adapt it to lean or agda21/06 22:04
pgiarrussocarter: uh I see21/06 22:04
pgiarrussocarter: I'm not the most expert here and I've never done System F myself21/06 22:04
carterpgiarrusso:  try it out21/06 22:04
carter:)21/06 22:04
pgiarrussoI'm not surprised21/06 22:04
carteri think theres some ways of indexing types by number/depth of quantfiers or something  might side step the issue21/06 22:05
carteror using sized types?21/06 22:05
carteridk21/06 22:05
pgiarrussobut I wanted to say: while I'm not the most expert, that feels well-suited for de Bruijn21/06 22:05
carteryes21/06 22:06
carterotoh, i'm also keen on trying to be as lazy as possible :0 21/06 22:06
pgiarrussooh well... do you have a clue if you need any permutation/swapping lemmas?21/06 22:06
carterbut yeah, its probably gonna wind up being debruijn 21/06 22:06
carterwhy would i?21/06 22:06
carter:)21/06 22:06
cartercontext?21/06 22:06
pgiarrussoI think that codebase has pretty much *all* of those lemmas, just in case, the guy is not lazy :-)21/06 22:07
carterultimately want the interesting bit to be  a function "erasingLinearityGivesWellTypedSystemFThing : Linear System F derivation tree -> SystemF derivation tree"21/06 22:07
pgiarrussocarter: I'm not saying *I* would have the discipline to figure that out in advance, but if you can it does save time21/06 22:07
carterand then say "by totality, this is sound"21/06 22:08
carter:)21/06 22:08
carterthis was still helpful21/06 22:08
carterthx21/06 22:08
carterme and a colleague are doing some formal proofs for a large project we're kicking off21/06 22:08
cartertrying to do the sanest / easiest appraoch possible21/06 22:08
carterso we can get it down21/06 22:08
carterdone21/06 22:08
carterttyl :) 21/06 22:08
pgiarrussocarter: oh, have you looked at Tiark's stuff?21/06 22:09
pgiarrussosorry, will let you go21/06 22:09
carterHe has proof stuff?21/06 22:09
carterI tried looking at the truffle stuff once and gave up 5 seconds into the code base21/06 22:09
carterLink please ?21/06 22:10
carter:)21/06 22:10
carterpgiarrusso: I assume you mean proof stuff?21/06 22:10
pgiarrussocarter: yes, with Nada http://doi.acm.org/10.1145/3009837.300986621/06 22:11
pgiarrussohis F<: definition uses definitional interpreters and environments, some links here: https://github.com/TiarkRompf/minidot/blob/529ef538929f204ec0d8a26534fd533e1890cfdf/README.md21/06 22:14
pgiarrussocarter: (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 everything21/06 22:15
carteri dont care about anything but getting that one function and associated type derivation model working :) 21/06 22:16
carterg2g, thx for the links21/06 22:16
pgiarrussohis 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 annoying21/06 22:16
pgiarrussoHTH21/06 22:16

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