/home/laney/.irssi/irclogs/Freenode/#agda.log-20170207

--- Day changed Mon Feb 06 2017
akrAny ideas about how to type something like https://i.stack.imgur.com/DM5os.png with unicode?06/02 09:25
akr_-[_]→_ isn't all that nice06/02 09:25
akrIs printing operators coming from instances broken?06/02 10:14
akrShould be    s -[ v ]→ s'    but it's    (_ Model.-[ s ]→ .v) s'06/02 10:14
akr(note the reversed argument order)06/02 10:14
akr(well not reversed exactly, just messed up)06/02 10:15
rntzdoes agda have pattern synonyms oranything like them?06/02 14:36
{AS}rntz: it does06/02 14:38
rntzare they documented anywhere?06/02 14:38
{AS}akr: you should open Model06/02 14:38
rntzthere is no Model.agda file in agda-stdlib.06/02 14:38
{AS}rntz: https://agda.readthedocs.io/en/latest/language/pattern-synonyms.html?highlight=synonym06/02 14:38
rntz... maybe my agda-stdlib is out of date06/02 14:38
{AS}rntz: I was writing to akr :)06/02 14:39
{AS}about the Model06/02 14:39
rntzoh, herp06/02 14:39
rntzthanks for the link!06/02 14:39
{AS}np06/02 14:39
akr{AS}: I did 'open Model {{…}} public'06/02 14:40
rntzmaybe the readthedocs link should be in the topic? it seems handy06/02 14:40
{AS}akr: Hmm, is the pretty printing still broken?06/02 14:41
{AS}rntz: We need someone who can change the topic06/02 14:41
{AS}comietek: *highlight*06/02 14:43
{AS}err06/02 14:43
{AS}copumpkin: 06/02 14:43
{AS}comietek: sorry06/02 14:43
akr{AS}: no idea06/02 14:53
akrmaybe it's something in my code, idk06/02 14:54
akrIt happens in a 'module _ {{_: Model}} where'06/02 14:54
{AS}akr: Hmm06/02 14:54
{AS}I think the first argument _06/02 14:54
{AS}is the instance06/02 14:54
{AS}akr: try naming the Model06/02 14:55
{AS}what do you call it?06/02 14:55
{AS}err06/02 14:55
{AS}what happens06/02 14:55
akryes, you're right06/02 14:55
akrit's the name of the instance06/02 14:56
akrbut it's still broken06/02 14:56
{AS}I think you need to have something like06/02 14:56
{AS}module M = Model M06/02 14:56
{AS}or open Model M06/02 14:56
{AS}or something06/02 14:56
{AS}where M is the name of your model06/02 14:56
akrin the module _?06/02 14:57
{AS}Yeah06/02 14:57
akrnot sure what to write06/02 15:00
{AS}akr: try open Model M first06/02 15:00
{AS}inside the module06/02 15:00
akreverything is either a syntax error or the fields from the record become irresolvable06/02 15:00
{AS}where M is your model name06/02 15:00
akryeah, that gives "Cannot resolve overloaded projection State because it is not applied to a visible argument"06/02 15:00
{AS}akr: ah06/02 15:01
{AS}how about 06/02 15:01
{AS}module M = Model M06/02 15:01
{AS}inside _ ?06/02 15:01
akroh yeah, that's fixed it06/02 15:02
akralthough now I get 's M.-[ .w ]→ s₂'06/02 15:02
akris there any way to get rid of the M.?06/02 15:02
akrwhat does module M = Model m even do?06/02 15:03
{AS}akr: It gives an alias to the namespace Model specialised for record m06/02 15:05
{AS}You could try having open Model {{...}} outside _06/02 15:06
{AS}and then removing this module alias06/02 15:06
akrthat's what I was doing originally06/02 15:06
akrsorry I guess I should've said that06/02 15:07
{AS}akr: and that didn't work?06/02 15:07
akrnope06/02 15:07
{AS}Yeah, I guess the only way to fix this is then to have the alias06/02 15:08
{AS}or I don't know any other way06/02 15:08
akrthis is much better already anyway06/02 15:09
akrthank you :)06/02 15:09
{AS}np :)06/02 15:09
comietekakr: it's a big06/02 15:26
comietekDISPLAY macros should help06/02 15:26
comietekI haven't done that myself yet06/02 15:26
comietekpgiarrusso might have06/02 15:27
comietekA bug :)06/02 15:27
akra big bug06/02 15:27
rntzhow do I convince agda that this function terminates: http://sprunge.us/KXJA ?06/02 15:39
rntzthe bit it complains about is the last line, U (coll-map (coll-map f) c)06/02 15:39
akryeah you can't really apply induction hypothesis twice on itself06/02 15:40
rntzthat explanation doesn't help me convince Agda that my function terminates06/02 15:41
rntz(I will also accept a counterexample on which it fails to terminate)06/02 15:41
{AS}rntz: This will terminate06/02 15:45
{AS}the problem is that Agda's termination checker is too stupid to figure that out :)06/02 15:45
{AS}or too simple06/02 15:45
rntzindeed, I'm pretty sure it does terminate :P06/02 15:45
{AS}stupid was maybe a bit harsh06/02 15:46
{AS}in any case06/02 15:46
{AS}what you can do is to make a size function06/02 15:46
rntzbut induction in this fashion over non-regularly-inductive types seems to be difficult to do in agda06/02 15:46
rntzhrm, a size function.06/02 15:46
{AS}that returns you a size06/02 15:46
rntzas a natural number, you mean? and then induct on hat?06/02 15:46
rntzand I ugess I can return empty if I run out of fuel06/02 15:46
{AS}Yeah06/02 15:47
{AS}rntz: and then you can prove that it returns an answer for any term06/02 15:47
akrwhat would be the size function? amount of nested Colls?06/02 15:47
rntz{AS}: oh, you mean have it return Maybe or something06/02 15:48
rntzand then separately prove it always returns just?06/02 15:48
{AS}rntz: yeah06/02 15:48
{AS}Yeah06/02 15:48
rntzah, that was different than what I was thinking06/02 15:48
{AS}akr: Hmm, that could be a way06/02 15:48
{AS}rntz: alternatively you provide a covering predicate which you can induct over06/02 15:48
rntzcovering predicate?06/02 15:48
{AS}rntz: a predicate on the input collection which somehow decreases at type level06/02 15:49
rntzcan you show me an example?06/02 15:50
{AS}rntz: Hmm06/02 15:51
{AS}Maybe what I was thinking of was somekind of sized types06/02 15:51
{AS}rntz: Yeah, that works06/02 15:54
{AS}rntz: https://gist.github.com/ahmadsalim/137f0455000e7c74547343e1af83bf2e06/02 15:55
rntz{AS}: hm, interesting.06/02 16:03
akrI know this gets asked a lot, but I always forget what the answer is: how can I control the amount of desugaring that's going on in the 'Goal' window? E.g. to have it write 'Σ[ … ] …' instead of 'Σ-syntax … …'06/02 16:28
akrwas there something about DISPLAY macros to deal with this as well?06/02 16:31
pgiarrussoakr: tried writing the resugaring with DISPLAY? Maybe there’s better, but that should work06/02 16:47
akrpgiarrusso: sorry, I don't know how to use DISPLAY at all, do you have any examples?06/02 16:51
pgiarrussoakr: find “New pragma DISPLAY” at https://github.com/agda/agda/blob/master/CHANGELOG.md06/02 16:54
pgiarrussoI’ve also done https://github.com/inc-lc/ilc-agda/pull/19/files#diff-ea1f747df12af929a23661b31c9789d6R38, and after seeing the CHANGELOG I suspect my example might actually be better06/02 16:55
akrpgiarrusso: that should help, thank you06/02 16:59
pgiarrussowelcome! Never tried if using DISPLAY for syntax, but it might work06/02 16:59
pgiarrussoalso, CHANGELOG seems generally the most complete reference, if not best organized, for the features it covers—everything since they started maintaining it06/02 17:00
akrcool, didn't know about that06/02 17:01
akrugh06/02 17:03
akrpattern matching doesn't work in where clauses?06/02 17:03
akrah it does but you have to give type first I think06/02 17:05
akrI wanted to do something like '[…] where (a , b) = makePair a b' and then use a and b in other where clauses, though06/02 17:06
akrI don't think one can do that, can they?06/02 17:07
SuprDewdis there a simple way to make all fields in a file public?06/02 21:31
SuprDewdsomething I can easily toggle on and off for debugging purposes06/02 21:31
SuprDewdor s/file/module, if that makes a difference06/02 21:42
akryou mean like 'open import MyModule public'?06/02 21:45
SuprDewdakr: if I understand correctly, this imports MyModule and all of its _public_ members into the current scope, and then re-exports them06/02 21:53
SuprDewdI want access to all of MyModule's private members (temporarily to debug some stuff)06/02 21:54
akrah06/02 21:59
larrytheliquidi may be remembering wrong, but werent parameters accessible as hidden arguments of constructors as in https://gist.github.com/larrytheliquid/602d60e2776230c5e8d5d35fccd43555 ?06/02 22:21

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