--- Day changed Wed Mar 15 2017
akr[m]Is is possible to define the partiality monad [1] without musical notation, using copatterns instead?15/03 15:04
akr[m]I'm having a hard time imagining how that could be done15/03 15:05
jonsterlingakr[m]: I did this once... I'll see if i can find it for you later today.15/03 15:11
akr[m]maybe a hint about how to define the _⊥ type might be enough to get me going :)15/03 15:12
akr[m]I'm trying to cook up something with sized types but no success so far15/03 15:13
akr[m]I mean, I guess I could just disable positivity checks, but that's cheating15/03 15:18
jonsterlingWhen i get to my office, I'll dig it up :) There is a trick where you need to define two types mutually, one of which adds the coinductive part or something15/03 15:29
akr[m]alright, thanks15/03 15:41
gallaisakr[m]: you should have a look at Abel & Chapman's https://arxiv.org/abs/1406.205915/03 18:04
comietek++15/03 18:07
comietekakr[m]: also https://github.com/mietek/abel-chapman-extended15/03 18:08
comietekCaveat emptor; notation in this repo is not up to my current standards15/03 18:08
rntzhttps://agda.readthedocs.io/en/v2.5.2/language/coinduction.html claims that "The type constructor \inf can be used to prove absurdity!"15/03 18:10
rntzis this true?15/03 18:10
rntzif so, can someone show me such a proof?15/03 18:10
akr[m]gallais: mietek: that looks quite interesting, thank you15/03 18:40
akr[m]hmm that's a funny trick with the mutual - coinductive definition15/03 18:42
akr[m]can't say that I like it very much15/03 18:45
akr[m]what the paper calls the Delay monad is the same as what agda-stdlib calls the Partiality monad, right?15/03 18:46
akr[m]morally speaking15/03 18:46
akr[m]if you can permit the use of that word :)15/03 18:46
comietekakr[m]: same monad AFAIK15/03 18:50
comietekakr[m]: I don't think you are allowed to non-ironically use "morally" until your 3rd published paper15/03 18:51
akr[m]lol15/03 18:53
akr[m]what if I need to use it to publish anything15/03 18:53
wrengrrntz: iirc, yes it's true; which is a big part of why it's deprecated. I'd have to dig out the proof from the Agda archives though15/03 22:29
gallaisrntz: https://github.com/agda/agda/issues/194615/03 22:44
gallaisThere's a label for proofs of false on the issue tracker: https://github.com/agda/agda/issues?utf8=%E2%9C%93&q=is%3Aissue%20label%3Afalse%2015/03 22:45
rntzhm. so maybe it wasn't inconsistent until sized types were added?15/03 23:31

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