--- Day changed Thu Jun 22 2017
pgiarrussocarter: *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
pgiarrussobut 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
carterThe goal is simplest thing possible22/06 02:25
carter:)22/06 02:32
pgiarrussocarter: 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
pgiarrussoso I'll shut up and let you work :-)22/06 02:39
carterpgiarrusso: it's for work. So there's a limit to how much I wanna debug stuff22/06 02:51
pgiarrussocool, looking forward to an industry job where I get the chance to use Agda ^_^ :-)22/06 03:01
carter:)22/06 03:16
carterpgiarrusso:  lol ... this is to prove the metatheory sound for a subset of what might be a linear logical agda22/06 03:39
pgiarrussocarter: that seems almost a sound metatheory, up to "sound erasure won't prove this linear stuff is actually linear", but I guess you know that22/06 03:41
pgiarrussoor maybe are doing something much more clever and encoding linear logic in System F22/06 03:42
carterNo. Just lower bounds22/06 03:43
carterAlso linearity is trivial to do correctly in this context.22/06 03:44
pgiarrussocarter O_O "Lightweight Linear Types in System F◦": http://www.cis.upenn.edu/~stevez/papers/MZZ10.pdf22/06 03:44
pgiarrussothey also erase to System F22/06 03:45
carterpgiarrusso: ... nope22/06 03:45
carterthis is cooler22/06 03:45
carterfull linear logic 22/06 03:45
pgiarrussoI see22/06 03:45
pgiarrussoANYWAY don't let me distract you (and myself :-))22/06 03:45
carterwait a month or three and i'll have a preprint22/06 03:46
carterso deal22/06 03:46
carterand wait 22/06 03:46
pgiarrusso+122/06 03:48
rntzdoes the agda stdlib have a way to turn a preorder into its poset of equivalence classes?22/06 15:59
rntzit should be easy enough to code up, I'm just wondering whether I've missed it22/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
rntznah, I don't need the quotient or anything22/06 16:05
rntzagda's stdlib has a Poset type22/06 16:05
rntzfor which you give a type, an equivalence relation, and a partial order relation that respects the equivalence relation22/06 16:06
rntzso basically you give a poset on a setoid, so you do quotients manually22/06 16:06
rntzbut 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
rntzand I was wondering if there was a function somewhere to do this22/06 16:07
rntzbut I think I'll just go write it22/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
rntzyes.22/06 17:22
rntzbut then you have to prove it's an equivalence, etc. etc.22/06 17:22
rntznone of which is difficult22/06 17:22
rntzit's just tedious boilerplate22/06 17:23
{AS}Ah, I see :)22/06 18:27
{AS}I guess they accept pull requests if you make one22/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!