--- Day changed Thu Jan 12 2017
subttleHi, I am still pretty new to Agda (but I do have experience with Haskell though) and I have a question. I am working on some educational code making my own implementation of regular expressions. I have a RegExp GADT and then smart constructors which form a Kleene algebra (a monoid for each binary operator, etc.) and I'm trying to prove that my smart constructor for concatenating (multiplying) any two 12/01 00:11
subttleregular expressions forms a monoid. Here is the relevant snippets of code for my question:12/01 00:11
subttlehttp://pastebin.com/y7diuxML12/01 00:11
subttleSo far all I have is very basic code (which works) but I noticed that making the changes to which I allude in the comments of that snippet causes a type error. Would anyone be so kind as to explain to me (or point me in the right direction) why changing the order of the first two lines of the _⨁_ function would cause a type error? I would like to feel that I fully understand this before I move on. Thank 12/01 00:11
subttleyou!12/01 00:11
tomjackpatterns are considered in order. so with your current version, ε ⨂ β matches the first clause and reduces to β. with the other version, ε ⨂ β _might_ match the first clause, if β is ε. so agda does not proceed to the further clauses, and ε ⨂ β will not reduce at all, until more is known about β12/01 00:40
subttletomjack: Ah, I see. Thank you. So then would you recommend just leaving the "long version" as is then, or is there a different way I should approach it?12/01 00:43
tomjacka simpler example to consider https://www.irccloud.com/pastebin/REtniINM/12/01 00:43
tomjackit might also be instructive to try things with `{-# OPTIONS --exact-split #-}` at the top of your file, if your agda is new enough to have that option12/01 00:45
tomjack(leave out the `'s)12/01 00:45
subttletomjack: ah, yes I'm on the latest :)12/01 00:45
tomjackthis will force you to write the patterns more explicitly, kind of showing how e.g. max1 and max2 actually have to work12/01 00:45
subttletomjack: excellent, thank you I will give this a go right now12/01 00:46
tomjackas for your example... it is nice to take advantage of behavior like the short version when possible12/01 00:46
tomjackbut there is always a kind of tradeoff. if you make some things reduce nicely, some other things probably won't reduce as nicely12/01 00:47
tomjacke.g. the extremely common example of 0 + n vs n + 0 with Nat12/01 00:48
tomjackpick whichever one makes you happier :)12/01 00:48
subttletomjack: I think I'm tracking, thank you for the help!12/01 00:52
francoisbabeufhttps://www.facebook.com/photo.php?fbid=10207975882611710&set=p.10207975882611710&type=3&theater12/01 01:06
rgrinbergSomething broke agda on archlinux for me, I keep getting /usr/share/agda/lib/prim/Level.agdai: removeLink: permission denied (Permission denied) when I load anything.12/01 04:02
rgrinbergAny idea what that could be?12/01 04:02
effectfu1rgrinberg: I had "permission denied" errors, try to close & open emacs (or whatever you use), if it won't help then try to delete all *.agdai files12/01 04:31
rgrinbergi tried restarting emacs but no dice. I deleted all agdai files except for the ones installed by the package manager12/01 04:33
rgrinbergIs this an issue with the emacs mode or agda itself?12/01 04:56
effectfu1rgrinberg: no idea12/01 04:58
effectfu1maybe try to form a bug report at https://github.com/agda/agda/issues12/01 04:59
rgrinbergWill do12/01 05:00
tomjackseems people have had a similar problem nix packages: https://github.com/NixOS/nixpkgs/issues/1530612/01 05:25
tomjackit seems like a bug with the package, not with agda :)12/01 05:25
rgrinbergtomjack: thanks. Anything i can do to narrow it down? The package in question is from the archlinux repository12/01 05:29
rgrinbergso it's nothing exotic12/01 05:29
tomjackyou didn't upgrade agda I presume?12/01 05:30
tomjackmaybe it could be considered a bug in agda if agda is needlessly trying to rewrite the .agdai12/01 05:30
tomjackI don't know why it would be doing it here...12/01 05:31
tomjackin the nix issue someone linked to /agda/agda/blob/master/CHANGELOG#L239 (lol)12/01 05:31
tomjackin their case though, it seems the package had no .agdai included12/01 05:32
rgrinbergtomjack: perhaps it was an upgrade, but I've uninstalled and installed agda from scratch since and it didn't fix anything12/01 05:32
tomjackif the agda version used to check the stdlib package differs from yours, it would not be very surprising if agda needs to rewrite the .agdai12/01 05:33
tomjackthe changelog says "Note that a module M may be re-typechecked if its time stamp is strictly newer than that of the corresponding interface file (M.agdai).", but dunno why that would affect you12/01 05:34
rgrinbergLet me see if agda from master is working12/01 05:35
tomjacknewer versions of agda seem less likely to work :)12/01 05:38
tomjackmaybe agda needs a feature to enable putting the .agdai elsewhere12/01 05:39
tomjackotherwise packaged .agda+.agdai files must only be used with a compatible (preferably packaged?) version of agda which must then guarantee that it won't ever rewrite the .agdai files...12/01 05:40
tomjackwhat I do is to just not use a package manager for agda libraries, which works fine :(12/01 05:42
rgrinbergHmm, $ stack build is failing for me12/01 05:44
rgrinbergnever mind, just to disable some test packages12/01 05:47
pgiarrussoeffectfully: uh OK, those are typed deBrujin indexes indeed; the scoped deBrujin indexes ones I saw before where just the contexts for type variables12/01 10:18
rgrinbergis there a way to case split on a view?12/01 23:52

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