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

--- Log closed Tue Jan 10 09:37:17 2017
--- Log opened Tue Jan 10 09:37:27 2017
-!- Irssi: #agda: Total of 111 nicks [0 ops, 0 halfops, 0 voices, 111 normal]10/01 09:37
--- Log closed Tue Jan 10 09:38:47 2017
--- Log opened Tue Jan 10 09:47:38 2017
-!- Irssi: #agda: Total of 116 nicks [0 ops, 0 halfops, 0 voices, 116 normal]10/01 09:47
-!- Irssi: Join to #agda was synced in 124 secs10/01 09:49
drdoWhat are the capitalisation restrictions in Agda?10/01 18:12
drdoOh, apparently none, it just doesn't like me using the module name10/01 18:14
drdoWrong again, it really doesn't like "TL"10/01 18:14
mietekdrdo: none?10/01 19:15
drdoIs there a gentler introduction to the stdlib for someone new to agda? Other than digging through the README and slowly figuring it out.10/01 20:11
drdoIn particular with for practical programming rather than theorem proving10/01 20:12
akrAaron Stump's book makes for a nice introduction to Agda and is available for free online10/01 20:13
akrI don't think there is a specific guide to the stdlib10/01 20:13
akrThough maybe you want to use the Agda Prelude for more practical programming: https://github.com/UlfNorell/agda-prelude10/01 20:15
drdoI'm likely to be proving things later. About the program I'm trying to write10/01 20:16
drdoI may have missed some messages, computer crashed :S10/01 20:19
akrI only typed 3 lines10/01 20:20
akrbut saw only 1 in response from you10/01 20:20
mietekExcept that Aaron Stump’s book doesn’t use the official stdlib10/01 20:58
mietekdrdo: there are no capitalisation restrictions in Agda that I’m aware of10/01 20:58
mietekdrdo: my suggestion is, do not use the stdlib as is; instead, try to write things from the ground up on your own, and use the stdlib to guide you10/01 20:59
akrmietek: no, but it develops something rather similar10/01 21:00
drdomietek: Interesting. Why that last suggestion?10/01 21:03
drdoI thought the purpose of the stdlib was to be, well, standard :)10/01 21:03
mietekdrdo: if you look at the README…10/01 21:03
mietekhttps://agda.github.io/agda-stdlib/README.html10/01 21:04
mietek-- Note that no guarantees are currently made about forwards or backwards compatibility, the library is still at an experimental stage.10/01 21:04
drdoRight, that's fine for what I'm doing10/01 21:04
mietekAlso https://agda.github.io/agda-stdlib/Everything.html is a good entry point10/01 21:04
drdoApropos, is there something useable right now with decent performance similar to Haskell's Data.Set?10/01 21:04
mietekIf you’re asking about performance, you may find that the language does not meet your expectations10/01 21:05
mietekWhat are you hoping to do?10/01 21:05
drdoWrite some logic-related program for my dissertation, and hopefully prove some interesting things about it as well10/01 21:06
mietekAh. Well, that should work :)10/01 21:06
drdoIt would be nice if it could run decently on some small examples :P10/01 21:06
mietekThere is https://agda.github.io/agda-stdlib/Data.AVL.IndexedMap.html#1 but I haven’t used it10/01 21:07
drdoI was using Haskell before, but got rather frustrated with the type system limitations10/01 21:08
mietekHaskell is much more mature.10/01 21:10
mietekThat being said, after 10 years of Haskell and 3 years of Agda, I now do all my free time programming in Agda.10/01 21:11
drdoIt's pretty hard to do something as simple as having a family of inductively defined data types such that they are all restrictions on the same base rules10/01 21:12
drdoYou can do some hacking with all the type extensions, but then you can't really use the types anyway because as soon as you start writing some function doing basic manipulation, you won't be able to prove that it type checks10/01 21:14

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