--- Day changed Tue May 30 2017
pgiarrussoTIL pattern matching on the RHS works better than I thought30/05 02:43
pgiarrusso  match-on-rhs : ∀ {τ} Γ1 Γ2 → Term Γ1 τ → Term Γ2 τ → Set30/05 02:43
pgiarrusso  match-on-rhs Γ1 Γ2 t1 t2 = Σ (Γ1 ≡ Γ2) λ { refl → t1 ≡ t2 }30/05 02:43
pgiarrussoThis is a silly example, but it's cool that t1 ≡ t2 is type correct because I match on refl30/05 02:43
pgiarrussosorry, no question, just wanted to share. I know, should use Twitter.30/05 02:44
Saizanpgiarrusso: yep, that's very nice, it's only been like that since a year ago or so30/05 09:24
arjen-jonathanHi all30/05 11:51
arjen-jonathanI don't understand Agda's irrelevance; does anyone have a good resource?30/05 11:56
arjen-jonathanIt seems that Idris has more powerful "erasure"; is anyone working on bringing that to Agda?30/05 11:57
nohToHello 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
nohToOr can anyone recommend a good way to learn agda? :-)30/05 15:40
nohToOr can anyone recommend a good way to learn agda? :-)30/05 15:41
zimanarjen-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 would30/05 15:49
subttlethis is probably a really silly question but I'm not sure I fully get why `remainder` here is using Fin30/05 19:50
subttlehttps://github.com/agda/agda-stdlib/blob/e25c3220f1d6cb822d1cf3c004907ac4576f3759/src/Data/Nat/DivMod.agda#L3430/05 19:50
mieteksubttle: why not?30/05 20:28
mieteksubttle: we know the remainder is supposed to be less than the divisor30/05 20:28
mieteksubttle: we might as well promise that this is in fact the case30/05 20:28
arjen-jonathanDoes 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
mieteknohTo: consider reading Aaron Stump’s boo30/05 20:29
mieteknohTo: book*30/05 20:29
subttlemietek: Ah, it just clicked, thank you for clearing that up!!!30/05 20:29
mieteksubttle: read types as propositions describing properties we wish to hold30/05 20:30
mieteknohTo: consider also following Martin Escardo’s tutorial: http://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html30/05 20:32
mieteknohTo: theorem-proving in Agda is like programming in a rigorous Haskell30/05 20:33
subttlemietek: Yes, I certainly see it now! Thanks again!30/05 20:33
mieteknohTo: the proofs are, quite literally, the programs that you write explicitly30/05 20:34
mieteknohTo: theorem-proving in Coq is like, uh… repairing a car engine through its tailpipe30/05 20:34
subttlelmfaoo30/05 20:34
mieteknohTo: the proofs are implicit and manipulated via imperative tactics scripts written in separate languages30/05 20:34
nohTomietek: :-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
mietekyou should just give it a go30/05 20:41
mietekalso30/05 20:41
mietekread Wadler30/05 20:41
mietekhttp://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf30/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 not30/05 20:42
mietekproofs are programs30/05 20:42
nohToyeah, 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
mietekyou know Haskell, yes?30/05 20:44
mietekcan you ask yourself the same question?30/05 20:44
mietekif proofs are programs/functions, then combining simpler programs/functions is…30/05 20:45
mietekfunctional programming30/05 20:45
mietekyes, Agda has higher-order functions; it could hardly not have them30/05 20:46
nohTo:-D Yeah, written out it sounded more stupid than in my head30/05 20:46
mietekI wouldn’t say stupid; it’s fine to ask30/05 20:46
mietekI’d say the question smelled a bit of Coq30/05 20:47
mietekwhere you need to explicitly invoke an inductive tactic, and so on30/05 20:47
mietekhttp://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html is a really good tutorial30/05 20:48
nohToYeah, coq is what I spent the last couple of hours with having a go at it.30/05 20:48
mietekprotip: use emacs and agda-mode30/05 20:48
mietekeven if you hate emacs like I do30/05 20:48
mietekI curse and scream and use it some more30/05 20:48
mietekand I will write my own editor in my copious free time, one day30/05 20:49
mietekbut for now, I haven’t found anything better30/05 20:49
nohToI just tried it again a few hours ago and I lasted 5 minutes30/05 20:49
nohToI'm just much more used to vim.30/05 20:49
subttlemietek: I've managed to get by so far with Atom :D but Emacs is probably a good investment for most30/05 20:49
mietekI suppose I haven’t really tried Atom’s Agda mode30/05 20:50
mietekI’m just generically opposed to running a web browser masquerading as an editor30/05 20:50
subttlemietek: ahaha, I hear that30/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 hole30/05 23:16
mietekhas not been reached during type checking (do you see yellow?)"30/05 23:16
* mietek sees red30/05 23:16

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