00:00:03 -!- erdic has quit (Changing host).
00:00:03 -!- erdic has joined.
00:01:44 -!- boily1 has joined.
00:02:08 -!- tromp__ has joined.
00:02:25 -!- atehwa has joined.
00:03:03 -!- Slereah__ has joined.
00:03:28 <Melvar> It timed out, and now it’s in a different net fragment.
00:04:20 <metasepia> General Melvar was the right hand man of Warlord Zsinj.
00:04:43 <Taneb> ~duck University of York
00:04:43 <metasepia> The University of York (informally York University, or simply York, abbreviated as Ebor.
00:05:25 <Taneb> Short for Eboracum, I presume
00:05:42 <Taneb> Roman name for York
00:05:57 -!- sgeoweb has joined.
00:06:02 <metasepia> Eboracum was a fort and city in Roman Britain.
00:06:56 -!- variable has joined.
00:07:00 <boily1> as the proverb goes, "Anas non satis accurate in hac nocte..."
00:07:36 -!- idris-ircslave has joined.
00:07:36 -!- trn has joined.
00:07:36 -!- Frooxius has joined.
00:08:16 -!- trn has quit (Max SendQ exceeded).
00:08:19 -!- nortti_ has joined.
00:10:50 -!- sebbu has quit (Ping timeout: 246 seconds).
00:10:52 -!- idris-ircslave has changed nick to 23LAATE3Q.
00:10:52 -!- idris-ircslave has joined.
00:10:52 -!- atehwa_ has quit (Ping timeout: 246 seconds).
00:10:52 -!- elliott_ has quit (Ping timeout: 246 seconds).
00:10:52 -!- boily has quit (Ping timeout: 246 seconds).
00:10:52 -!- glogbackup has quit (Ping timeout: 246 seconds).
00:10:56 -!- idris-ircslave has quit (Client Quit).
00:10:56 -!- nortti has quit (Ping timeout: 246 seconds).
00:10:56 -!- itsy has quit (Ping timeout: 246 seconds).
00:10:56 -!- Slereah_ has quit (Ping timeout: 246 seconds).
00:10:56 -!- tromp has quit (Ping timeout: 246 seconds).
00:10:56 -!- trn has joined.
00:11:08 -!- sgeoweb has quit (Quit: Page closed).
00:11:15 -!- boily1 has changed nick to boily.
00:11:21 -!- Froox has joined.
00:12:00 <oerjan> quousque tandem abutere, boily, latina nostra?
00:12:22 -!- tromp_ has quit (Remote host closed the connection).
00:12:41 -!- FireFly has joined.
00:12:49 -!- 23LAATE3Q has quit (Ping timeout: 240 seconds).
00:13:09 <oerjan> are we being ddosed again
00:13:39 -!- Frooxius has quit (Ping timeout: 240 seconds).
00:14:50 -!- Sgeo_ has quit (Ping timeout: 265 seconds).
00:14:55 <boily> Taneb: “How long, pray will you abuse boily, the Latin do with us?” ← uhm... wut?
00:15:10 <boily> oerjan: thausibly.
00:15:15 -!- Sgeo has joined.
00:15:33 <oerjan> i just changed a couple words in an _actual_ famous quote fwiw
00:15:58 <boily> Taneb: I can't read. I meant to answer oerjan.
00:16:07 <boily> (stupid term colours.)
00:16:23 <Taneb> Wouldn't be "our Latin"?
00:17:06 <boily> I don't do the Latin. you can get addicted to it!
00:17:11 <oerjan> https://en.wikipedia.org/wiki/Catiline_Orations#Oratio_in_Catilinam_Prima_in_Senatu_Habita
00:17:45 <oerjan> Taneb: i assume he tried google translate
00:18:22 <Taneb> Anyway, I have a nine o'clock train. Goodnight
00:21:29 -!- erdic has quit (Remote host closed the connection).
00:27:02 -!- erdic has joined.
00:31:57 -!- yorick has quit (Read error: Connection reset by peer).
00:44:53 -!- FireFly has quit (Excess Flood).
00:46:11 -!- FireFly has joined.
00:55:17 -!- elliott has joined.
00:55:26 -!- elliott has quit (Client Quit).
00:55:41 -!- elliott has joined.
00:59:15 -!- tromp has joined.
01:02:41 -!- metasepia has quit (Remote host closed the connection).
01:02:47 -!- boily has quit (Quit: GALAPAGOS CHICKEN).
01:16:17 -!- erdic has quit (Remote host closed the connection).
01:16:51 -!- erdic has joined.
01:21:32 -!- ^v has joined.
01:27:05 -!- conehead has quit (Quit: Computer has gone to sleep.).
01:34:33 <Jafet> The risk is merely topical.
01:34:59 <oerjan> well but it's particularly high today (tomorrow for you americans)
01:48:05 -!- Slereah_ has joined.
01:49:43 -!- Slereah__ has quit (Ping timeout: 264 seconds).
02:05:49 -!- conehead has joined.
02:06:00 -!- tromp has quit (Remote host closed the connection).
02:06:35 -!- tromp has joined.
02:10:56 -!- tromp has quit (Ping timeout: 264 seconds).
02:20:07 -!- oerjan has quit (Quit: Nite).
02:27:50 -!- tromp has joined.
02:40:16 -!- Slereah__ has joined.
02:42:08 -!- Slereah_ has quit (Ping timeout: 264 seconds).
02:45:40 -!- nooodl has joined.
02:47:24 -!- nooodl__ has quit (Ping timeout: 255 seconds).
02:51:18 -!- Sellyme has quit (Excess Flood).
02:53:55 -!- Sellyme has joined.
03:21:03 -!- conehead has quit (Quit: Computer has gone to sleep.).
03:32:31 <Sgeo> 17:14:05 --- nick: idris-ircslave -> 23LAATE3Q
03:32:34 <Sgeo> What was that about?
03:37:25 -!- Slereah_ has joined.
03:39:08 -!- Slereah__ has quit (Ping timeout: 264 seconds).
03:40:56 -!- nooodl has quit (Ping timeout: 264 seconds).
03:46:07 -!- tromp has quit (Remote host closed the connection).
03:46:40 -!- tromp has joined.
03:50:51 -!- tromp has quit (Remote host closed the connection).
03:51:05 -!- tromp has joined.
03:51:31 -!- Guest95255 has quit (Quit: Connection closed for inactivity).
03:54:55 -!- Slereah__ has joined.
03:57:08 -!- Slereah_ has quit (Ping timeout: 264 seconds).
04:01:10 -!- shikhout has joined.
04:04:15 -!- shikhin has quit (Ping timeout: 255 seconds).
04:04:16 -!- shikhout has changed nick to shikhin.
04:10:07 -!- Sorella has quit (Quit: It is tiem!).
04:45:49 -!- tromp has quit (Remote host closed the connection).
04:45:56 <Melvar> Sgeo: Bogosity due to netsplits and -joins.
04:46:25 -!- tromp has joined.
04:48:50 -!- nisstyre_ has joined.
04:51:08 -!- tromp has quit (Ping timeout: 264 seconds).
04:55:05 -!- idris-ircslave has joined.
04:56:00 <Sgeo> ( the (a ** b) (5 ** "hi")
04:56:20 <Sgeo> ( the (a ** String) (5 ** "hi")
04:59:04 -!- variable has changed nick to trout.
05:06:36 <Sgeo> A dependent pair where the proof's type isn't actually dependent on the witness
05:07:48 <Sgeo> Almost wish you could do useful things with Types, make (t ** t) effectively be the typed of runtime-tagged values, practically dynamic typing
05:08:11 <Sgeo> ( the (t ** t) (Int ** 5)
05:11:10 <Sgeo> Totally useless but heterogeneous vector
05:12:25 <Sgeo> > the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), ((a -> a) ** id)]
05:12:27 <lambdabot> Not in scope: `the'Not in scope: data constructor `Vect'Not in scope: data c...
05:12:27 <lambdabot> `In' (imported from Lambdabot.Plugin.Haskell.Eval.Trusted),
05:12:27 <lambdabot> `InR' (imported from Lambdabot.Plugin.Haskell.Eval.Trusted)Not in scope: d...
05:12:51 <Sgeo> ( the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (({a : Type} -> a -> a) ** id)]
05:12:53 <idris-ircslave> the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (({a : Type} -> a ->>
05:13:15 <Sgeo> ( the (Vect 3 (t ** t)) $ [(Int ** 5), (String ** "Hello"), (((a : Type) -> a -> a) ** the)]
05:13:22 <idris-ircslave> [(Int ** 5), (String ** "Hello"), ((a124 : Type) -> a124 -> a124 ** the)] : Vect 3 (t ** t)
05:13:44 <copumpkin> Sgeo: I was mostly puzzled by the unconstrained a variable
05:14:10 <Sgeo> Implies implicit argument
05:14:19 <Sgeo> Although ** is syntax sugar
05:16:51 <copumpkin> [00:56:20] <idris-ircslave> (5 ** "hi") : (a ** String)
05:17:20 <lambdabot> parse error (possibly incorrect indentation or mismatched brackets)
05:24:05 -!- Slereah_ has joined.
05:25:56 -!- Slereah__ has quit (Ping timeout: 264 seconds).
05:35:45 -!- Bike has joined.
05:38:19 -!- Sellyme has quit (Excess Flood).
05:40:25 -!- Sellyme_ has joined.
05:41:20 -!- Sellyme_ has changed nick to Sellyme.
05:48:52 -!- conehead has joined.
05:49:02 -!- chaiomanot has quit (Quit: Leaving).
06:16:12 -!- trout has quit (Ping timeout: 255 seconds).
07:02:45 -!- ^v has quit (Quit: Leaving).
07:26:59 <Bike> was it, sgeo? or have you now violated your most cherished moral principles
07:29:32 <Sgeo> Hey, if Int can be a Type 1 and a Type 2 and a Type 3 and ... why shouldn't something lower down be able to participate?
07:30:35 <Bike> Int can be a Type 2?
07:31:43 <Sgeo> ( the (Vect 2 Type) [Int, Type]
07:32:09 <Sgeo> That Type in the type signature of that has to be Type 1
07:32:36 <Bike> this seems kind of dumb.
07:36:35 <shikhin> Um, silly question, but if you're on cell 0 in brainfuck, and you do '<', what's the expected behavior?
07:41:54 <Bike> i think it depends on implementation
07:42:25 <Bike> sometimes the tape goes infinitely left, sometimes you get an error, sometimes monkeys fly out your nose, that kinda thing?
07:48:27 -!- Bike has quit (Quit: Page closed).
07:50:41 -!- Slereah__ has joined.
07:52:20 -!- Slereah_ has quit (Ping timeout: 264 seconds).
07:53:41 -!- nisstyre_ has quit (Quit: WeeChat 0.4.3).
08:00:24 -!- Slereah_ has joined.
08:02:32 -!- Slereah__ has quit (Ping timeout: 264 seconds).
08:08:50 -!- Slereahphone has joined.
08:11:33 -!- nisstyre has quit (Quit: WeeChat 0.4.3).
08:13:35 -!- Slereahphone has quit (Ping timeout: 252 seconds).
08:27:50 -!- Slereahphone has joined.
08:30:57 -!- Tritonio has joined.
08:47:31 -!- conehead has quit (Quit: Computer has gone to sleep.).
08:48:14 -!- Tritonio has quit (Ping timeout: 252 seconds).
08:51:02 -!- Slereahphone_ has joined.
08:52:05 -!- Slereahphone has quit (Ping timeout: 252 seconds).
08:52:07 -!- Slereahphone_ has changed nick to Slereahphone.
08:52:07 -!- Slereahphone has quit (Client Quit).
09:00:54 -!- mysanthrop has changed nick to myname.
09:04:28 -!- nisstyre has joined.
09:10:04 <Sgeo> Melvar: Should I assume effects will always be a no-go for idris-ircslave?
09:12:43 <Sgeo> Yay, I'm "Talkative" on StackOverflow
09:18:23 <fizzie> (I hope that at least requires a space after the paren.)
09:19:19 <Sgeo> ( the ((a : Type) -> a -> a) the
09:19:33 <idris-ircslave> Control.Category.. : Category cat => (cat b c) -> (cat a b) -> cat a c
09:20:04 <Sgeo> What's a simple dependently typed function that might fail with .
09:21:45 <Taneb> 9:15 is the worst time to wake up for an 8:55 train
09:22:20 <Sgeo> ( (the . id) Nat 5
09:22:47 <Sgeo> ( (id . the) Nat 5
09:22:56 -!- Slereahphone has joined.
09:23:05 <idris-ircslave> Can't disambiguate name: Prelude.Basics.., Control.Category..
09:23:13 <Sgeo> ( :t (id Prelude.Basics.)
09:23:14 -!- Slereah__ has joined.
09:23:19 <Sgeo> ( :t (id Prelude.Basics..)
09:23:26 <Sgeo> ( :t (id (Prelude.Basics..))
09:24:58 <fizzie> ))))))))))))))))))))))))))))))))))))))))))))))))))) calculated to balance things for this month, so far.
09:25:19 <Sgeo> ) 1 2 3 + 4 5 6
09:25:38 -!- Slereah_ has quit (Ping timeout: 252 seconds).
09:28:58 <fizzie> Actually, based on my current set of logs starting from 2009-03, we actually need 19291 extra opening parens, and my "balancing" just made the total situation worse.
09:29:12 <fizzie> Wonder where all those closing parens come from; there hasn't been *that* much jconn use.
09:29:24 <olsner> how many come from fungot?
09:29:24 <fungot> olsner: " i want as much as i loathe how you've manipulated my friends and i are a bit, and if the good. or any room with. simple math dictates the futility of your effort, i have made, it will now go and i will give you my motives and they were not to your liking, would i be carrying our monthly" says that's what my dad, and my time that you are under the empire that has been so deeply disappoi--
09:31:51 <fizzie> olsner: ...actually it's almost all from ":)" and the like...
09:32:44 <olsner> time to start writing (:
09:34:34 <fizzie> Or just be :( all the time.
09:35:32 <Sgeo> 19291 palindromic parentheses
09:48:36 <oklopol> i guess that was answered.
10:01:22 -!- shikhout has joined.
10:02:46 -!- mr45 has joined.
10:03:48 -!- shikhin has quit (Ping timeout: 255 seconds).
10:03:50 -!- shikhout has changed nick to shikhin.
10:07:19 -!- mr45 has left.
10:22:26 -!- nisstyre has quit (Quit: WeeChat 0.4.3).
10:47:03 -!- nooodl has joined.
10:58:35 -!- Slereah__ has quit (Ping timeout: 252 seconds).
11:00:46 -!- Slereah_ has joined.
11:01:41 -!- ggherdov_ has quit (Changing host).
11:01:42 -!- ggherdov_ has joined.
11:01:42 -!- ggherdov_ has quit (Changing host).
11:01:42 -!- ggherdov_ has joined.
11:02:20 -!- ggherdov_ has changed nick to ggherdov.
11:03:05 -!- nooodl has quit (Ping timeout: 252 seconds).
11:12:42 -!- sebbu2 has changed nick to sebbu.
11:35:53 -!- nortti_ has changed nick to nortti.
11:43:12 -!- password2 has joined.
12:03:57 <Melvar> Sgeo, Taneb: It’s “Namespace.(*~)”, the pretty-printer is just still buggy on that bit.
12:06:47 -!- boily has joined.
12:37:34 <FreeFull> idris-ircslave should be configured to not accept > outside of #idris
12:39:59 -!- Sorella has joined.
12:45:54 <Melvar> It doesn’t have any configuration. At all.
12:47:01 -!- yorick has joined.
13:22:25 -!- password2 has quit (Ping timeout: 240 seconds).
13:27:50 -!- oerjan has joined.
13:32:08 <ion> TIL Nethack, Dungeon Crawl and others are based on octagonal tiles in a hyperbolic space. https://github.com/mhwombat/grid/wiki/Octagonal-tiles
13:33:57 <elliott> fizzie: I sort of think the wiki should have full specs when possible
13:37:14 <oerjan> ion: um i am quite suspicious that the connection graphs are the same.
13:37:49 <Jafet> ion: still can't beat the projective 3D goban
13:37:52 <oerjan> like because hyperbolic tilings usually grow exponentially by level, iirc
13:40:54 <Jafet> Well, they become the same if you merge a few to save space (Haskell is after all very bad with memory and we should help it out whenever possible)
13:43:19 <oerjan> yep, not the same as https://en.wikipedia.org/wiki/File:Uniform_tiling_83-t0.png
13:43:54 <ion> If you place a shape, such as a circle or a square, around (0,0) in https://raw.github.com/mhwombat/grid/master/userguide/images/UnboundedOctGrid.png and start growing the shape, the number of tiles its boundaries touch grows more or less like hyperbolic space, no?
13:44:14 <oerjan> while a cell has 8 neigbors by both countings, those 9 cells have 16 other neighbors in total with the diagonal stuff, but 32 in the hyperbolic one.
13:45:28 <oerjan> which i think is a "no" to your question.
13:46:33 <oerjan> basically, the moore neighborhood "disks" grow linearly sized boundaries, not exponential
13:48:51 <Jafet> http://programmers.stackexchange.com/questions/81624/how-do-computers-work
13:49:21 <oerjan> in fact that hyperbolic picture gets a little hard to read at the next step, but i _think_ it quadruples every new distance.
13:50:00 <oerjan> well logically it should, since it's uniform.
13:50:40 <Jafet> "Another distinctive property is the amount of space covered by the n-ball in hyperbolic n-space: it increases exponentially with respect to the radius of the ball, rather than polynomially."
13:51:16 <boily> Jafet: don't post that kind of link after a reading binge of creepy and horror stories. I am now scared post-shitless.
13:51:21 <oerjan> oh hm wait that's not true, some of them have only 3.
13:52:10 <Jafet> boily: http://stackoverflow.com/a/1732454
13:52:18 -!- variable has joined.
13:52:54 <boily> Jafet: ah, a classic! I always keep a copy of that one on every machine I own :D
13:53:08 <boily> (reminds me to copy it to my newest acquisition)
13:53:24 <Jafet> The text near the end is actually an amazing test for font rendering
13:53:58 -!- Sgeo_ has joined.
13:55:18 <Jafet> oerjan: the border of the image is so tattered that it puts the accuracy of the diagram into question
13:57:05 <oerjan> but i think it's actually meant to be varying for two types of octagons at distance 2, according to whether they themselves bound 1 or 2 at distance 1.
13:57:58 -!- Sgeo has quit (Ping timeout: 265 seconds).
13:58:04 <boily> TIL: it's en:octagon, but fr:octogon.
13:58:08 <oerjan> the former have 3 exclusive neigbors and 2 more shared on each side, the latter have 2 and 2.
14:04:51 -!- Slereah_ has quit (Remote host closed the connection).
14:05:05 <oerjan> hm apparently it's oktogon in norwegian.
14:05:12 -!- Slereah_ has joined.
14:07:52 <oerjan> Du latin octogonos, lui-même issu du grec ancien ὀκτώ, oktô (« huit ») et γωνία, gônia (« angle »).
14:08:12 <oerjan> i suspect the latins latinized the vowel a bit.
14:08:42 <oerjan> First attested in 1656, from Latin octagonos, from Ancient Greek οκτάγωνος (oktágōnos, “eight-angled”), from ὀκτώ (octō, “eight”) + γωνία (gōnía, “angle”).
14:09:49 <oerjan> otoh it's latin "octave"
14:09:58 <oerjan> which is pure latin afaik.
14:10:45 <oerjan> (given that it's the common ordinal)
14:12:03 -!- Slereah_ has quit (Remote host closed the connection).
14:12:14 -!- shikhin has quit (Read error: No route to host).
14:12:51 -!- shikhin has joined.
14:12:52 -!- Slereah_ has joined.
14:14:09 <boily> but then latin has "octō".
14:14:12 <boily> Latin+ ūnus duo trēs quattuor quinque sex septem octō novem decem
14:14:14 <boily> Greek éna đío tría téssera pénde éksi eftá oxtó ennéa đéka
14:14:49 <oerjan> that's modern greek, the ancient pronunciation was different see table in https://en.wiktionary.org/wiki/%E1%BD%80%CE%BA%CF%84%CF%8E
14:15:13 -!- variable has quit (Ping timeout: 240 seconds).
14:16:18 <oerjan> also http://www.youtube.com/watch?v=YCFXGanTx4A
14:19:50 -!- password2 has joined.
14:20:21 <boily> `relcome password2
14:20:35 <fungot> password2: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esote ...
14:20:35 <boily> Gregor: IEUAAAAAAAAAAAAAAAAAAARGH! I SHALL MAPOLE YOU!
14:20:47 <oerjan> fungot: stop being so brief
14:20:47 <fungot> oerjan: of, for-- what does that do? the guild" only worked because belkar and i are a bit, and if my whole life was just leading to one big anticlimax?
14:21:12 <boily> oerjan: but that clip only has one two three four. what about the Pronunciation of Eight?
14:21:29 <boily> (btw, nice fungotrick.)
14:21:29 <fungot> boily: good, good. my partner and i were to be connected to anything especialy scandalous. tell him that i said this is where that king guy is as you say that, i thought that the surname came first in feudal deal there and get started, just put my " thank my lord only gave you the really bad, belkar
14:21:40 <oerjan> boily: i am pretty sure at one point in the movie she shouts "oktogonta!"
14:21:58 <oerjan> (when haggling over their rent)
14:22:35 <oerjan> or possibly oxtogonta.
14:23:33 <boily> I need to spend more time watching old movies.
14:24:43 <oerjan> well it's been a while since i saw it.
14:24:51 -!- tromp has joined.
14:26:38 -!- HackEgo has joined.
14:28:34 <Melvar> oerjan: ‘x’ indicating what there?
14:28:39 <olsner> oh, so tesseract means four-something, finally makes sense
14:29:15 <oerjan> Melvar: the ipa sound, i guess?
14:30:09 <boily> I think a little mapoling is in order at this point.
14:30:11 <oerjan> `you're not really HackEgo are you. since when do you join from an unnamed ip.
14:30:39 * boily artfully, tesseratically swings his mapole over at Gracenotes
14:30:44 <Melvar> Okay. Just checking, ‘χ’ versus ‘ξ’ and stuff.
14:30:47 <boily> s/Gracenotes/Gregor/
14:31:13 <oerjan> Melvar: see the historical pronunciations at https://en.wiktionary.org/wiki/%E1%BD%80%CE%BA%CF%84%CF%8E
14:32:04 <Gregor> Yeah, I'm not really sure what's goin' on right now...
14:32:54 <Melvar> Ohhuh. /x/ from ‹κ›, hadn’t heard of that change.
14:33:10 <oerjan> Gregor: is that actually your bot or is it just someone else faking
14:33:14 <boily> password2: so, what brings you over to #esoteric by this fine Saturday morning?
14:33:57 <boily> fungot: with your sentience, can you achieve a HackEgo Impersonation?
14:33:57 <fungot> boily: i know, i was, uh, any reason... there's no one here but us? we just dueled, he had a name, in accordance with your orders when he instructed the orcs and told me
14:34:06 <oerjan> the repository looks ok
14:34:55 -!- HackEgo has quit (Remote host closed the connection).
14:35:10 <olsner> the problem seems to be that everything gives "No output." instead of e.g. an error
14:49:41 <lambdabot> Maybe you meant: rc reconnect remember repoint roll run v @ ? .
14:51:46 <password2> well boily , i have joined this channel a while ago
14:52:12 <boily> password2: ah? >_>'...
14:57:47 <olsner> what is that? it looks vaguely haskelly but not quite
15:02:33 -!- Slereahphone has quit (Quit: Colloquy for iPhone - http://colloquy.mobi).
15:03:00 -!- Slereahphone has joined.
15:09:13 -!- password2 has quit (Ping timeout: 240 seconds).
15:10:00 <idris-ircslave> Numbers strictly less than some bound. The name comes from "finite sets"
15:14:16 -!- Vorpal has joined.
15:14:22 <Melvar> (Thus, Fin n is inhabited by exactly n values.)
15:15:24 <boily> ah, so that's why (Fin 0) 1 doesn't work.
15:17:58 <Melvar> I hope the bit of error reflection that turns that into a more digestible message is merged soon.
15:41:03 -!- HackEgo has joined.
15:44:18 -!- impomatic has quit (Ping timeout: 240 seconds).
16:01:32 -!- shikhout has joined.
16:04:43 -!- shikhin has quit (Ping timeout: 264 seconds).
16:04:44 -!- shikhout has changed nick to shikhin.
16:08:29 <jconn> oerjan: |syntax error
16:08:29 <jconn> oerjan: | :t zipWith
16:08:35 <idris-ircslave> Prelude.List.zipWith : (a -> b -> c) -> (l : List a) -> (r : List b) -> (length l = length r) -> List c
16:08:35 <idris-ircslave> Prelude.Stream.zipWith : (a -> b -> c) -> (Stream a) -> (Stream b) -> Stream c
16:08:35 <idris-ircslave> Prelude.Vect.zipWith : (a -> b -> c) -> (Vect n a) -> (Vect n b) -> Vect n c
16:10:07 <oerjan> ( let fib = 1 :: 1 :: zipWith (+) fib (tail fib) in fib
16:10:09 <idris-ircslave> Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.::
16:10:36 <oerjan> ( let fib = the (Stream Integer) (1 :: 1 :: zipWith (+) fib (tail fib)) in fib
16:10:51 <idris-ircslave> Data.Vect.Quantifiers.:: : (P x) -> (All P xs) -> All P (x :: xs)
16:10:51 <idris-ircslave> Prelude.Stream.:: : a -> (Lazy (Stream a)) -> Stream a
16:11:11 -!- ^v has joined.
16:11:48 <oerjan> ( let fib = the (Lazy (Stream Integer)) (1 :: 1 :: zipWith (+) fib (tail fib)) in fib
16:12:07 <oerjan> this type inference isn't very reliable.
16:12:37 <oerjan> ( let fib : Lazy (Stream Integer); fib = 1 :: 1 :: zipWith (+) fib (tail fib) in fib
16:12:38 <idris-ircslave> let fib : Lazy (Stream Integer); fib = 1 :: 1 :: zipWith (+) fib (tail fib) in>
16:13:04 <oerjan> ...you cannot use : in let?
16:14:33 <oerjan> ( let fib = Delay (1 :: 1 :: zipWith (+) fib (tail fib)) in fib
16:14:33 <idris-ircslave> Can't disambiguate name: Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Prelude.Vect.::
16:15:17 <oerjan> ( let fib = Delay (the (Stream Integer) (1 :: 1 :: zipWith (+) fib (tail fib))) in fib
16:16:15 <oerjan> ( let fib = Delay (1 :: 1 :: Prelude.Stream.zipWith (+) fib (tail fib))) in fib
16:16:31 <oerjan> ( let fib = Delay (1 :: 1 :: Prelude.Stream.zipWith (+) fib (tail fib)) in fib
16:18:22 <oerjan> ( let fib = Delay (1 Prelude.Stream.:: 1 Prelude.Stream.:: Prelude.Stream.zipWith (+) fib (tail fib)) in fib
16:18:47 <oerjan> ( let fib = Delay (1 Prelude.Stream.(::) 1 Prelude.Stream.(::) Prelude.Stream.zipWith (+) fib (tail fib)) in fib
16:18:47 <idris-ircslave> (input):1:20:Can't infer type for (|(|fromInteger 1 , fromInteger 1 , |) , 1 , 1 , 1 , 1 , 1 , 1 , |) (::)
16:19:10 <oerjan> ( let fib = Delay ((the Integer 1) Prelude.Stream.(::) 1 Prelude.Stream.(::) Prelude.Stream.zipWith (+) fib (tail fib)) in fib
16:19:10 <idris-ircslave> (input):1:34:the Integer (fromInteger 1) does not have a function type (Integer)
16:19:39 <idris-ircslave> Prelude.List.tail : (l : List a) -> (isCons l = True) -> List a
16:20:40 <oerjan> ( let s = (the Integer 1) Prelude.Stream.(::) s in s
16:20:40 <idris-ircslave> (input):1:25:the Integer (fromInteger 1) does not have a function type (Integer)
16:20:54 <oerjan> ( let s = (the Integer 1) `Prelude.Stream.(::)` s in s
16:21:45 <oerjan> ( let s = (the Integer 1) `Prelude.Stream.(::)` (Delay s) in s
16:30:14 <Melvar> oerjan: What are you trying to do?
16:30:31 <oerjan> make a fibonacci stream
16:30:59 <oerjan> ( let rec s = (the Integer 1) `Prelude.Stream.(::)` (Delay s) in s
16:31:23 <Melvar> > let fibs = with Stream 0 :: 1 :: [| fibs + tail fibs |] in take 10 fibs
16:31:24 <lambdabot> <hint>:1:29: Illegal literal in type (use -XDataKinds to enable): 1
16:31:33 <Melvar> ( let fibs = with Stream 0 :: 1 :: [| fibs + tail fibs |] in take 10 fibs
16:32:07 <oerjan> so only functions can recurse?
16:32:36 <oerjan> or, recursion only at top level?
16:32:53 <Melvar> Only top-level and where-clause defns, I think.
16:33:58 <Melvar> “fibs : Stream Nat ; fibs = 0 :: 1 :: [| fibs + tail fibs |]” in a file should work.
16:34:16 <oerjan> ( let fibs = fibs' where fibs' = with Stream 0 :: 1 :: [| fibs' + tail fibs' |] in take 10 fibs
16:34:18 <Melvar> That’s also not recursion, but corecursion; in idris the difference is significant.
16:35:13 <oerjan> no where clauses in let definitions?
16:36:04 <oerjan> if you borrow haskell syntax, you should do it _properly_ :(
16:39:31 <Melvar> It started out whitespace-insensitive, it has grown more like Haskell syntax since …
16:40:33 <oerjan> cargo cult haskell syntax >:)
16:46:51 <Melvar> Mainly because whitespace-insensitive was easier to implement; it’s largely a research language.
16:55:01 <Jafet> U+237B NOT CHECK MARK appears before U+2713 CHECK MARK. ✓
16:55:22 <oerjan> i guess they forgot to check that
16:56:49 -!- yorick has quit (Read error: Connection reset by peer).
16:59:42 -!- oerjan has quit (Quit: leaving).
17:05:56 <kmc> I hope they implemented whitespace as sugar for punctuation, like Haskell
17:14:53 <Melvar> kmc: Well, it’s not sugar as such; the parser checks indents rather than lexing and preprocessing indents into blocks before continuing (which IIRC is what is done for Haskell). But you can use whitespace and {;} alternatively, yes.
17:19:02 <kmc> is that difference observable in the language specification
17:19:29 -!- nisstyre has joined.
17:20:51 <Melvar> There is no specification. Just research papers that describe some of the foundations and features.
17:22:48 <kmc> sure, I mean hypothetically
17:24:53 -!- tromp has quit (Remote host closed the connection).
17:25:26 -!- tromp has joined.
17:29:16 <Melvar> Well, the implementation approaches can be made to behave exactly the same, but I’m guessing that the actual Idris implementation parses some edge cases differently even in the language constructs that Idris and Haskell share, and this is not necessarily always considered a bug.
17:29:26 <Melvar> There are almost certainly still outright bugs though.
17:29:29 -!- tromp has quit (Ping timeout: 240 seconds).
17:52:02 -!- password2 has joined.
18:12:34 -!- AnotherTest has joined.
18:36:26 <boily> `relcome password2 (because I can :D)
18:38:47 <password2> I like the randomness of this channel
19:08:57 <boily> I lunched at a Vietnamese restaurant, then went grocery shopping, coffee shopping, and now I'm back home playing DCSS.
19:21:53 -!- conehead has joined.
19:31:20 -!- lexande has quit (Ping timeout: 264 seconds).
19:31:49 -!- lexande has joined.
19:32:15 -!- password2 has quit (Remote host closed the connection).
19:34:45 -!- password2 has joined.
19:40:07 -!- password2 has quit (Ping timeout: 264 seconds).
19:45:20 -!- chaiomanot has joined.
19:48:57 -!- password2 has joined.
19:57:33 <kmc> http://i.imgur.com/hTcbghi.jpg
19:59:14 -!- ^v has quit (Ping timeout: 252 seconds).
20:08:08 <Taneb> Today I bought an apple and ate it, entirely of my own volition. I... don't know who I am any more
20:10:09 -!- itsy has joined.
20:11:41 <boily> Taneb: if you are having identity troubles, you should become Canadian. it's a very sane choice.
20:11:54 <boily> kmc: shiny racoons!
20:12:20 <Taneb> boily, I am still reasonably confident about my nationality
20:12:24 <Taneb> Merely not my diet
20:16:12 <password2> oh yeah , i now have an irc bot running
20:16:37 <Taneb> Is it written in Piet
20:23:09 <password2> for now it just sit in a room and responds to hello
20:23:43 <fungot> fizzie: and my soul and nev'r... actually, y'know, the rune over behind xkyon's throne labeled " castle blowing her cover.
20:23:57 <fizzie> This new style is not very good. :/
20:24:14 <boily> Taneb: Canadianness isn't just a nationality. it's a State of Mind. it's a Temperature. it's Kraft Dinner, too!
20:24:37 <boily> fizzie: it already had some interesting moments, but I concur. I think my favourite is the lovecraft one.
20:24:39 -!- ^v has joined.
20:24:45 <Taneb> But I was going to make chilli and cheese sandwich things
20:25:07 <olsner> but you had an apple instead?
20:25:25 <Taneb> olsner, the apple was for the walk home from the shop
20:25:26 <fizzie> boily: I'm partial to europarl, for some reason. (And the "irc" style, which was in fact the first.)
20:25:32 -!- nortti has changed nick to lawspeaker.
20:25:35 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack oots* pa qwantz sms speeches ss wp youtube
20:25:43 <fungot> Selected style: enron (subset of the Enron email dataset)
20:25:52 <Taneb> fungot, how do I deseed a chilli
20:25:52 -!- lawspeaker has changed nick to nortti.
20:25:52 <fungot> Taneb: for an email. check on the appropriate. april brazil mark t. d. anderson will get to know that the issue of how the attached schedule of the plane that landed a job.
20:25:59 <fungot> Selected style: jargon (UNIX-HATERS mailing list archive)
20:26:03 <fungot> olsner: ack, i've gotten more help than criticism from its alumni.
20:26:43 <Taneb> Hmm, I prefer hotter food, should I leave the seeds in, fungot?
20:26:43 <fungot> Taneb: to the root directory and then return to the superficial dogma of the
20:27:49 <olsner> deseeding is overkill in my experience, doesn't seem to matter if there are seeds or not
20:28:21 <Taneb> Thanks, olsner. Tholsner.
20:28:29 <olsner> perhaps it's hotter? but just use less next time if it gets too hot
20:28:59 <Taneb> Oh man, the recipe says use four chillies, but I only bought three :)
20:30:52 <boily> do you have any hot sauce? tomato paste?
20:31:47 -!- conehead has quit (Quit: Computer has gone to sleep.).
20:32:39 <Taneb> I could just spread it thinner
20:32:45 <Taneb> It's only baked sandwiches
20:35:36 -!- yorick has joined.
20:38:06 -!- FireFly has quit (Excess Flood).
20:39:58 -!- FireFly has joined.
21:06:00 <fungot> Thanks, olsner. Tholsner.
21:06:23 <fizzie> Replacing HackEgo, one command at a time.
21:06:43 <fizzie> Disclaimer: may have bugs.
21:07:15 <fizzie> If it doesn't have any, then it should have the same semantics as `thanks.
21:08:04 <olsner> the semantics of `thanks luckily doesn't depend too much on the output
21:08:29 <fungot> >2,[>,]+15[>+6>+7>+3>+2<4-]>-6.>-.-7.+13.-3.+8.>-.>+2.<5[<]>[.>]>3+2.>.<3.<2[<]>[[-<2+>+>]+<-97[-4[-4[-6[-6[-4[>-<[-]]]]]]]>[[>]>2-11.<3[<]<.>3[.>]>3.>5][-]>]<3[[<]>2[.>]>5.>2]
21:09:12 <olsner> great way to show thanks, fungot
21:09:12 <fungot> olsner: didn't you think i'm using it as it were the greatest new idea since the counter was big enough, zwgc has an opening for a routing entry first in the header ( as set forth in the file
21:13:09 -!- Slereahphone has quit (Remote host closed the connection).
21:13:30 -!- Slereahphone has joined.
21:16:05 -!- Slereahphone_ has joined.
21:17:38 -!- Slereahphone has quit (Ping timeout: 240 seconds).
21:17:40 -!- Slereahphone_ has changed nick to Slereahphone.
21:18:39 <nortti> how would one cleanly search for 3 sequential lines conforming to same regex using standard unix commandset?
21:21:54 <nortti> never mind, awk and counter var
21:29:32 <mroman> standard unix commandset
21:39:38 -!- AnotherTest has quit (Ping timeout: 240 seconds).
21:39:58 -!- password2 has quit (Ping timeout: 240 seconds).
21:40:41 -!- Slereah__ has joined.
21:43:43 -!- Slereah_ has quit (Ping timeout: 264 seconds).
21:51:35 -!- Slereah_ has joined.
21:53:59 -!- Slereah__ has quit (Ping timeout: 240 seconds).
22:01:40 -!- shikhout has joined.
22:04:43 -!- shikhin has quit (Ping timeout: 264 seconds).
22:04:44 -!- shikhout has changed nick to shikhin.
22:05:30 <Sgeo_> https://github.com/idris-lang/Idris-dev/issues/287#issuecomment-37738942
22:07:44 * Sgeo_ doesn't actually know what's going on in that code
22:13:04 -!- oerjan has joined.
22:27:34 <Sgeo_> Except possibly totality checker merely not active
22:28:49 <oerjan> ok it's definitely not getting into the repository.
22:37:47 -!- ^v has quit (Read error: Connection reset by peer).
22:38:14 -!- ^v has joined.
22:38:28 <boily> `learn TEST TEST TEST! TEST TEST TEST!
22:41:01 -!- nooodl has joined.
22:45:36 * boily sings the Zelda grab-item jingle ♪
22:46:02 <boily> (still crawling. just got the Sword of Zonguldrok!)
22:47:13 -!- aloril has quit (Remote host closed the connection).
22:57:04 -!- aloril has joined.
23:09:10 <ion> http://fratti.ch/spaghetti/airlessarchives69%20-%20%5bArchive%5d%20Unboxing%202012%20McDonalds%20My%20Little%20Pony%20Toys.webm
23:14:31 -!- Slereah__ has joined.
23:15:13 -!- Slereah_ has quit (Ping timeout: 240 seconds).