--- 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 done | 15/03 15:05 |

jonsterling | akr[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 far | 15/03 15:13 |

akr[m] | I mean, I guess I could just disable positivity checks, but that's cheating | 15/03 15:18 |

jonsterling | When 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 something | 15/03 15:29 |

akr[m] | alright, thanks | 15/03 15:41 |

gallais | akr[m]: you should have a look at Abel & Chapman's https://arxiv.org/abs/1406.2059 | 15/03 18:04 |

comietek | ++ | 15/03 18:07 |

comietek | akr[m]: also https://github.com/mietek/abel-chapman-extended | 15/03 18:08 |

comietek | Caveat emptor; notation in this repo is not up to my current standards | 15/03 18:08 |

rntz | https://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 |

rntz | is this true? | 15/03 18:10 |

rntz | if so, can someone show me such a proof? | 15/03 18:10 |

akr[m] | gallais: mietek: that looks quite interesting, thank you | 15/03 18:40 |

akr[m] | hmm that's a funny trick with the mutual - coinductive definition | 15/03 18:42 |

akr[m] | can't say that I like it very much | 15/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 speaking | 15/03 18:46 |

akr[m] | if you can permit the use of that word :) | 15/03 18:46 |

comietek | akr[m]: same monad AFAIK | 15/03 18:50 |

comietek | akr[m]: I don't think you are allowed to non-ironically use "morally" until your 3rd published paper | 15/03 18:51 |

akr[m] | lol | 15/03 18:53 |

akr[m] | what if I need to use it to publish anything | 15/03 18:53 |

wrengr | rntz: 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 though | 15/03 22:29 |

gallais | rntz: https://github.com/agda/agda/issues/1946 | 15/03 22:44 |

gallais | There'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%20 | 15/03 22:45 |

rntz | hm. 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!