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

--- Day changed Thu Jun 01 2017
gallais20:14 < comietek> or, any Agda implementation of a language with binders, using something else than de Bruijn indices?  ideally, names.01/06 00:25
gallaisdo you mean catarina coquand fresh names in nbe for stlc + explicit subst? 0:-)01/06 00:25
mietekgallais: I know you’ve pointed me to that before, and I have about three unfinished implementations to prove that01/06 00:32
mietekgallais: do you have a finished one?01/06 00:32
mietekI really like the context+freshness relation from that paper01/06 00:33
mietekit’s actually the #1 idea in my head at the moment01/06 00:33
mietekbecause I just can’t deal with "I am not a number"01/06 00:34
mietekhttps://gergo.erdi.hu/blog/2013-05-01-simply_typed_lambda_calculus_in_agda,_without_shortcuts/ looks promising01/06 00:53
liyangHas anyone made a concerted effort at “Project Euler for Grownups”, AKA http://www.cs.ru.nl/~freek/100/ ?01/06 02:02
mietekliyang: ooh.01/06 02:08
mietekand here I was planning to go to sleep tonight…01/06 02:08
liyangmietek: go to bed. You're not going to get them all done tonight.01/06 02:39
nohToHello everyone. I'm currently in the process of learning agda and I love it so far!01/06 13:20
nohToThere is one thing that bothers me, though. When I try to see my code (acting on natural numbers) in action, I would like to get my results sugared nicely as 3 instead of suc suc suc zero01/06 13:22
nohToDoes anyone know how to do that? I'm using the stdlib naturals01/06 13:22
nohToOh and also, I was expecting the stdlib to provide something like a _==_ : {A} -> A -> A -> Bool for all A that have decidable equality01/06 13:31
nohToBut the only == I could find right now is taylored to the naturals, which is a bit annoying01/06 13:32
mieteknohTo: are you looking for https://agda.github.io/agda-stdlib/Relation.Nullary.Decidable.html#822 ?01/06 13:53
mietek⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool01/06 13:53
nohToAh, so then I can define _==_ to be |\===| or something along those lines?01/06 13:54
eraserhdWhy would the goal remain unevaluated here? https://github.com/eraserhd/ehk/blob/master/algebra/PureScriptMonoid.agda#L3201/06 13:57
nohToTo me agda's support for implicit arguments seems perfectly suited for awesome polymorphism similar to how haskell treats numerals or +. Is that implemented somewhere? Or am I missing why that wouldn't be desirable?01/06 14:27
mieteknohTo: you’re right; http://agda.readthedocs.io/en/v2.5.2/language/instance-arguments.html#defining-type-classes01/06 14:36
gallais14:55 < eraserhd> Why would the goal remain unevaluated here?01/06 14:39
gallais^ what do you expect it to evaluate to?01/06 14:39
nohTomietek: Very nice. So that means I could make numerals change their type? I have to test that :-D01/06 14:41
eraserhdgallais: In the Idris version, at this point, it's unfolded the Q+ calls.01/06 15:32
mieteknohTo: I think now you’re looking for overloaded literals01/06 15:33
mieteknohTo: http://agda.readthedocs.io/en/v2.5.2/language/literal-overloading.html01/06 15:33
nohTomietek: I'm very glad that agda supports that01/06 15:34
mietekso am I, although I’m having some problems getting it to work reliably for more complex things01/06 15:34
mietekhttp://wiki.portal.chalmers.se/agda/;?n=Main.Arrays01/06 15:41
mietekit would been nice to have the contents01/06 15:41
nohToI don't quite understand what that list is supposed to mean? Are those implementation goals?01/06 15:45
Eduard_MunteanuIt isn't particularly difficult to bind to Haskell arrays.01/06 15:47
Eduard_MunteanuYou could also use AVL as a map.01/06 15:47
eraserhdOh, duh, it can't do that if I don't match out the numerators and denominators.01/06 15:48
mietekEduard_Munteanu: I’m interested in defining an array data structure01/06 15:51
mietekI suppose an array can be seen as a function from Fin n, for some n01/06 15:52
mietekbut that’s not ideal, because we can’t pattern-match on functions01/06 15:52
Eduard_Munteanumietek, there's Vec, if you don't care much about random access01/06 15:52
mietekEduard_Munteanu: I do01/06 15:52
mietekthat’s the entire point01/06 15:53
Eduard_MunteanuYou can bind to Haskell arrays and expose a Fin-indexed interface.01/06 15:53
mietekI’m more interested in simplicity and correctness, than efficiency01/06 15:54
mietekbinding to a Haskell array would be basically a bunch of postulates01/06 15:55
Eduard_MunteanuI'm not sure you can get true arrays without some language facility.01/06 15:56
mietekI probably don’t need the full flexibility of arrays01/06 15:57
mietekI’d like to be able to formalise de Bruijn levels, basically01/06 15:57
mietekit seems that this would require random-access for reading01/06 15:57
mietekand at the very least, append for writing01/06 15:58
mietekpossibly also insert01/06 15:58
mietekno mutation, no deletion01/06 15:58
Eduard_MunteanuAVL may be more suitable then, think of it as a Data.Map from Haskell.01/06 16:00
Eduard_Munteanu@where nameless01/06 16:01
lambdabotI know nothing about nameless.01/06 16:01
Eduard_Munteanu@where+ nameless Nameless, Painless: https://nicolaspouillard.fr/publis/nameless-painless.pdf01/06 16:02
lambdabotIt is stored.01/06 16:02
Eduard_Munteanumietek, you might also be interested in the paper above01/06 16:02
mietekhmm01/06 16:03
mietekthanks, although I’m not sure if this helps01/06 16:03
mietekthe paper is about de Bruijn _indices_, which count the other way from levels01/06 16:05
mietekright?01/06 16:05
mietekformalising de Bruijn indices together with lists is quite simple01/06 16:05
mietekor at least, can be; one not-so-simple method is https://agda.github.io/agda-stdlib/Data.List.Any.html01/06 16:06
mieteksimpler: https://mietek.github.io/imla2017/html/Stack.html01/06 16:07
eraserhdHow do I extract *-comm for Z to use it in a rewrite?01/06 16:24
bitonicI vaguely remember some work in encoding algorithm complexity of your program at the type level01/06 16:53
bitonicFor example putting an upper bound on how many times a certain operation is ran01/06 16:54
bitonicBut I can't find a reference now, does anybody remember that work or did I dream of it?01/06 16:54
mietekbitonic: at the language level, Pola01/06 17:05
mietekbitonic: http://www.csd.uwo.ca/~mburrel/presentation/LCC.pdf01/06 17:05
bitonicmietek: I don't think that's what I was remembering, but thanks, looks related!01/06 17:06
mietekyeah. if you find the thing you have in mind, please let me know.01/06 17:06
mietekmore on Pola: http://cs.ioc.ee/fics09/proceedings/invited1.pdf01/06 17:06
bitonicmietek: https://www.reddit.com/r/haskell/comments/4y8i85/complexity_monad/ I think this is what I was remembering01/06 17:07
bitonicOr anyway, something along those lines01/06 18:02

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