--- Day changed Thu Jun 22 2017 | ||

pgiarrusso | carter: *actually*, that might be a different timesink, but if you define well-typedness as a separate judgement (not intrinsically well-typed terms), I suspect Twelf could work and give you full HOAS; and Beluga would do the same but let you still do functional programming instead of logic programming. | 22/06 02:20 |
---|---|---|

pgiarrusso | but I've never seen people use Beluga outside of where they work on it (Twelf, on the other hand, has been used for ML, if you can face its limited expressivity) | 22/06 02:21 |

carter | The goal is simplest thing possible | 22/06 02:25 |

carter | :) | 22/06 02:32 |

pgiarrusso | carter: well, how much can you fiddle to get that? Learning Beluga sounds like https://xkcd.com/1319/ or https://xkcd.com/1205/ :-) | 22/06 02:38 |

pgiarrusso | so I'll shut up and let you work :-) | 22/06 02:39 |

carter | pgiarrusso: it's for work. So there's a limit to how much I wanna debug stuff | 22/06 02:51 |

pgiarrusso | cool, looking forward to an industry job where I get the chance to use Agda ^_^ :-) | 22/06 03:01 |

carter | :) | 22/06 03:16 |

carter | pgiarrusso: lol ... this is to prove the metatheory sound for a subset of what might be a linear logical agda | 22/06 03:39 |

pgiarrusso | carter: that seems almost a sound metatheory, up to "sound erasure won't prove this linear stuff is actually linear", but I guess you know that | 22/06 03:41 |

pgiarrusso | or maybe are doing something much more clever and encoding linear logic in System F | 22/06 03:42 |

carter | No. Just lower bounds | 22/06 03:43 |

carter | Also linearity is trivial to do correctly in this context. | 22/06 03:44 |

pgiarrusso | carter O_O "Lightweight Linear Types in System F◦": http://www.cis.upenn.edu/~stevez/papers/MZZ10.pdf | 22/06 03:44 |

pgiarrusso | they also erase to System F | 22/06 03:45 |

carter | pgiarrusso: ... nope | 22/06 03:45 |

carter | this is cooler | 22/06 03:45 |

carter | full linear logic | 22/06 03:45 |

pgiarrusso | I see | 22/06 03:45 |

pgiarrusso | ANYWAY don't let me distract you (and myself :-)) | 22/06 03:45 |

carter | wait a month or three and i'll have a preprint | 22/06 03:46 |

carter | so deal | 22/06 03:46 |

carter | and wait | 22/06 03:46 |

pgiarrusso | +1 | 22/06 03:48 |

rntz | does the agda stdlib have a way to turn a preorder into its poset of equivalence classes? | 22/06 15:59 |

rntz | it should be easy enough to code up, I'm just wondering whether I've missed it | 22/06 15:59 |

{AS} | rntz: You mean does Agda have quotient types? :) | 22/06 16:01 |

{AS} | Ah wait, I think I understand. You just want quotienting | 22/06 16:02 |

rntz | nah, I don't need the quotient or anything | 22/06 16:05 |

rntz | agda's stdlib has a Poset type | 22/06 16:05 |

rntz | for which you give a type, an equivalence relation, and a partial order relation that respects the equivalence relation | 22/06 16:06 |

rntz | so basically you give a poset on a setoid, so you do quotients manually | 22/06 16:06 |

rntz | but given a preorder, it's easy to derive the equivalence relation it induces (x == y iff x <= y and y <= x) | 22/06 16:07 |

rntz | and I was wondering if there was a function somewhere to do this | 22/06 16:07 |

rntz | but I think I'll just go write it | 22/06 16:07 |

rntz | (mind you, I *would* kind of like an agda with quotients) | 22/06 16:07 |

{AS} | rntz: That equivalence relation is just a pair | 22/06 16:12 |

{AS} | _~_ = x ≤ y \times y ≤ x , no? | 22/06 16:15 |

rntz | yes. | 22/06 17:22 |

rntz | but then you have to prove it's an equivalence, etc. etc. | 22/06 17:22 |

rntz | none of which is difficult | 22/06 17:22 |

rntz | it's just tedious boilerplate | 22/06 17:23 |

{AS} | Ah, I see :) | 22/06 18:27 |

{AS} | I guess they accept pull requests if you make one | 22/06 18:27 |

{AS} | (so that people do not have to redo it in the future) | 22/06 18:28 |

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