--- Day changed Tue May 30 2017 | ||

pgiarrusso | TIL pattern matching on the RHS works better than I thought | 30/05 02:43 |
---|---|---|

pgiarrusso | match-on-rhs : ∀ {τ} Γ1 Γ2 → Term Γ1 τ → Term Γ2 τ → Set | 30/05 02:43 |

pgiarrusso | match-on-rhs Γ1 Γ2 t1 t2 = Σ (Γ1 ≡ Γ2) λ { refl → t1 ≡ t2 } | 30/05 02:43 |

pgiarrusso | This is a silly example, but it's cool that t1 ≡ t2 is type correct because I match on refl | 30/05 02:43 |

pgiarrusso | sorry, no question, just wanted to share. I know, should use Twitter. | 30/05 02:44 |

Saizan | pgiarrusso: yep, that's very nice, it's only been like that since a year ago or so | 30/05 09:24 |

arjen-jonathan | Hi all | 30/05 11:51 |

arjen-jonathan | I don't understand Agda's irrelevance; does anyone have a good resource? | 30/05 11:56 |

arjen-jonathan | It seems that Idris has more powerful "erasure"; is anyone working on bringing that to Agda? | 30/05 11:57 |

nohTo | Hello everyone. Recently I became interested in homotopy type theory and would like to play around with it. Maybe this is the wrong place to ask, because you might be biased, but how can I decide between learning Agda vs learning Coq? | 30/05 15:35 |

nohTo | Or can anyone recommend a good way to learn agda? :-) | 30/05 15:40 |

nohTo | Or can anyone recommend a good way to learn agda? :-) | 30/05 15:41 |

ziman | arjen-jonathan: they also seem to have a different focus; Agda's irrelevance is not only for erasure but also affects equality (irrelevant values are always considered equal) so if you have a record with proofs, the proofs won't affect equality; in Idris, they would | 30/05 15:49 |

subttle | this is probably a really silly question but I'm not sure I fully get why `remainder` here is using Fin | 30/05 19:50 |

subttle | https://github.com/agda/agda-stdlib/blob/e25c3220f1d6cb822d1cf3c004907ac4576f3759/src/Data/Nat/DivMod.agda#L34 | 30/05 19:50 |

mietek | subttle: why not? | 30/05 20:28 |

mietek | subttle: we know the remainder is supposed to be less than the divisor | 30/05 20:28 |

mietek | subttle: we might as well promise that this is in fact the case | 30/05 20:28 |

arjen-jonathan | Does anyone happen to know wether a recording exists of any of last AIM's talks? Particularly looking for Ulf's talk. | 30/05 20:29 |

mietek | nohTo: consider reading Aaron Stump’s boo | 30/05 20:29 |

mietek | nohTo: book* | 30/05 20:29 |

subttle | mietek: Ah, it just clicked, thank you for clearing that up!!! | 30/05 20:29 |

mietek | subttle: read types as propositions describing properties we wish to hold | 30/05 20:30 |

mietek | nohTo: consider also following Martin Escardo’s tutorial: http://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html | 30/05 20:32 |

mietek | nohTo: theorem-proving in Agda is like programming in a rigorous Haskell | 30/05 20:33 |

subttle | mietek: Yes, I certainly see it now! Thanks again! | 30/05 20:33 |

mietek | nohTo: the proofs are, quite literally, the programs that you write explicitly | 30/05 20:34 |

mietek | nohTo: theorem-proving in Coq is like, uh… repairing a car engine through its tailpipe | 30/05 20:34 |

subttle | lmfaoo | 30/05 20:34 |

mietek | nohTo: the proofs are implicit and manipulated via imperative tactics scripts written in separate languages | 30/05 20:34 |

nohTo | mietek: :-D I really enjoy your comparison. But if you construct the proof explicitly as a function isn't it quite tough to keep your head around what is happening? But since I'm a really big fan of Haskell, Agda has a big bonus in my mind. | 30/05 20:40 |

mietek | you should just give it a go | 30/05 20:41 |

mietek | also | 30/05 20:41 |

mietek | read Wadler | 30/05 20:41 |

mietek | http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf | 30/05 20:41 |

mietek | "if you construct the proof explicitly as a function" makes it sound like something weird and unusual is happening — but it’s not | 30/05 20:42 |

mietek | proofs are programs | 30/05 20:42 |

nohTo | yeah, you're right. And then Agda has some "higher order" proofs like induction that can combine simpler proofs into more sophisticated ones? | 30/05 20:44 |

mietek | you know Haskell, yes? | 30/05 20:44 |

mietek | can you ask yourself the same question? | 30/05 20:44 |

mietek | if proofs are programs/functions, then combining simpler programs/functions is… | 30/05 20:45 |

mietek | functional programming | 30/05 20:45 |

mietek | yes, Agda has higher-order functions; it could hardly not have them | 30/05 20:46 |

nohTo | :-D Yeah, written out it sounded more stupid than in my head | 30/05 20:46 |

mietek | I wouldn’t say stupid; it’s fine to ask | 30/05 20:46 |

mietek | I’d say the question smelled a bit of Coq | 30/05 20:47 |

mietek | where you need to explicitly invoke an inductive tactic, and so on | 30/05 20:47 |

mietek | http://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html is a really good tutorial | 30/05 20:48 |

nohTo | Yeah, coq is what I spent the last couple of hours with having a go at it. | 30/05 20:48 |

mietek | protip: use emacs and agda-mode | 30/05 20:48 |

mietek | even if you hate emacs like I do | 30/05 20:48 |

mietek | I curse and scream and use it some more | 30/05 20:48 |

mietek | and I will write my own editor in my copious free time, one day | 30/05 20:49 |

mietek | but for now, I haven’t found anything better | 30/05 20:49 |

nohTo | I just tried it again a few hours ago and I lasted 5 minutes | 30/05 20:49 |

nohTo | I'm just much more used to vim. | 30/05 20:49 |

subttle | mietek: I've managed to get by so far with Atom :D but Emacs is probably a good investment for most | 30/05 20:49 |

mietek | I suppose I haven’t really tried Atom’s Agda mode | 30/05 20:50 |

mietek | I’m just generically opposed to running a web browser masquerading as an editor | 30/05 20:50 |

subttle | mietek: ahaha, I hear that | 30/05 20:50 |

mietek | (of course, emacs is an operating system masquerading as an editor… but I digress) | 30/05 21:11 |

mietek | "No type nor action available for hole ?0. Possible cause: the hole | 30/05 23:16 |

mietek | has not been reached during type checking (do you see yellow?)" | 30/05 23:16 |

* mietek sees red | 30/05 23:16 |

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