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

--- Day changed Wed Apr 12 2017
parolangHello12/04 01:03
quchenIs there a way to tell Agda that a function reduces its argument, in the sense of the termination checker? Consider12/04 08:37
quchenwiden : … -> Fin n -> Fin (succ n)12/04 08:38
quchenwhich says that 5 is Fin 6, so it is also Fin 712/04 08:38
quchenAnd now I have another function that recurses on a Fin, foo (fsucc n) x = foo (widen n) (succ x), or something12/04 08:39
quchenThe termination checker now complains that this is not terminating, since (widen n) is not structurally smaller than (fsucc n).12/04 08:39
quchenI hope this is at least somewhat understandable; if not, I can try to put together a minimal example.12/04 08:40
quchenThe problem I’m trying to solve is looping over a Fin (succ n), i.e. evaluate a function (succ n) times, while keeping »n« fixed.12/04 08:41
quchenPattern matching on a Fin, (fsucc n), gives me an (n) of a smaller Fin though.12/04 08:41
quchenAh, my »widen« is called »raise« in the standard lib.12/04 08:44
gallaisquchen: not without having to rewrite a lot of code (i.e. by defining Fin in a sized-type manner)12/04 10:31
quchengallais: sized-type, another one of those words I’ve seen, but not used yet. :-)12/04 11:15
quchenPity some small attribute or implicit argument or something doesn’t help12/04 11:15
gallaisquchen: do you really have to adjust the Fin at that point? Can't you accumulate information in another (possibly extra) argument?12/04 11:42
gallais(e.g. have a "Fin k" and carry a proof that "k <= n")12/04 11:43
quchengallais: I thought I could just create a loop that starts at the maximum of a Fin, and recurses down to 012/04 11:45
quchenI guess I can first create the list [n..0] and then use that12/04 11:46
gallaisDo you mean you want `reverse (allFin n)`? https://agda.github.io/agda-stdlib/Data.Vec.html#687112/04 11:47
quchenHmm, maybe I can use that.12/04 11:54
quchenWorked! Thanks :-)12/04 12:11
subttleSo I read this http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/ and thought it would be fun (and also potentially useful for something else I'm working on) to make a nubsort for nonempty lists12/04 21:56
subttleAny feedback is welcome :D https://gist.github.com/subttle/7c2d3e745eb6a3af9ba430e54f07e01712/04 21:56
subttleoh and I should say it needs agda-stdlib >0.13 (currently that means the development version)12/04 22:06
subttleUnrelated.. I have some basic questions about trying to work with Fin if anyone is around later today, any help would be appreciated12/04 22:55
subttleor even if there are exercises or literature to which anyone will point me, I would be very grateful!12/04 23:19
comieteksubttle: just Asi12/04 23:22
comietekask*12/04 23:22
subttlecomietek: sure, I have a bunch though so I didn't want to clog up the chat :D12/04 23:29
subttleFor starters I'm not sure what exactly strengthen is meant to do12/04 23:30
subttlethe comment says -- A strengthening injection into the minimal Fin fibre.12/04 23:30
subttlebut I'm not quite sure I get that12/04 23:31
subttleAnd one other question for now, if I have a function which takes (X : Fin n) is there an idiomatic way to return the least element, and what would that type look like?12/04 23:34
subttleI feel like that should be easy to do but I'm having brain flatulence I guess12/04 23:34
subttleand perhaps I'm asking that too awkwardly... basically if I have a set X and I want to take that as an argument and return X₀ then I'm not sure how to write that12/04 23:38
subttles/set X/finite set X/12/04 23:47
subttleand maybe it's better to call that X₁12/04 23:52

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