00:00:36 -!- ais523 has joined.
00:01:39 -!- skj3gg has quit (Quit: ZZZzzz…).
00:07:52 -!- adu has joined.
00:10:03 <ais523> hmm, is this the right channel to post Wikipedia pages which are so specific I'm surprised they exist?
00:10:05 <ais523> https://en.wikipedia.org/wiki/Artificial_castling
00:11:00 <zzo38> Probably not, but you can post it anyways.
00:14:17 -!- shikhin has joined.
00:15:05 <boily> it is chess, therefore it is the right channel.
00:17:54 -!- shikhin_ has quit (Ping timeout: 272 seconds).
00:21:13 <J_Arcane> are there any esolangs that encode instructions in chess moves?
00:21:32 <J_Arcane> because chess notation looks to me at least as unintelligible as burlesque.
00:23:09 <ais523> hmm, clearly we need an esolang which has a relatively simple mapping between chess moves and instructions (preferably one that ties into chess somehow, not a boring BF equivalent)
00:23:21 <ais523> but the twist is: the program needs to be a valid chess game
00:23:44 <ais523> the hardest part would presumably be ensuring that each piece is only moved from the square it's currently on
00:25:08 <J_Arcane> Looks like the wiki turns up only a couple unfinished and unimplemented idea pages.
00:26:05 <J_Arcane> It does occur to me that a chessboard is essentially 8 one-byte registers, after a fashion ...
00:26:29 <ais523> this also makes the language fail at full TCness because it only supports finitely many programs
00:26:38 <ais523> however, IMO it should at least be curly-L complete
00:28:54 <J_Arcane> That's true. Chess is 'solvable' after all. Now Go ...
00:28:56 -!- ProofTechnique has quit (Quit: ZNC - http://znc.in).
00:30:20 <int-e> ais523: hmm, the 50-moves rule isn't enforced.
00:33:50 <int-e> (same for the three-fold repetition)
00:34:14 <HackEgo> [wiki] [[Talk:CBR (Cleverer Brainfuck)]] N http://esolangs.org/w/index.php?oldid=41728 * BCompton * (+133) Created page with "Should this page be ''CBF'' instead of ''CBR''? ~~~~"
00:58:30 -!- bb010g has joined.
01:18:44 -!- Lymia has quit (Ping timeout: 246 seconds).
01:32:32 -!- Lymia has joined.
01:41:33 -!- ^v has joined.
01:42:00 <ais523> J_Arcane: but Go is already a programming language
01:42:00 -!- ^v has quit (Client Quit).
01:43:43 <Jafet> Call it Ban Go
01:55:23 -!- Lymia has quit (Ping timeout: 252 seconds).
02:02:27 * boily sings «Ban go, ban go, ban go, ban go, ban go dai kazoku ♪»
02:02:34 -!- boily has quit (Quit: UNNERVING CHICKEN).
02:06:19 -!- chaosagent has joined.
02:10:14 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
02:30:33 -!- Lymia has joined.
02:42:44 -!- MDude has quit (Ping timeout: 246 seconds).
02:48:20 -!- shikhin has quit (Ping timeout: 246 seconds).
02:52:12 -!- Tritonio has joined.
02:56:10 -!- Tritonio has quit (Remote host closed the connection).
02:56:26 -!- Tritonio has joined.
03:25:08 -!- mitchs_ has joined.
03:28:32 -!- mitchs has quit (Ping timeout: 272 seconds).
03:30:54 -!- GeekDude has changed nick to GeekAfk.
03:40:10 -!- shikhin has joined.
03:51:06 -!- MDude has joined.
03:58:43 -!- fractal has quit (Ping timeout: 245 seconds).
04:11:44 -!- fractal has joined.
04:24:15 -!- skj3gg has joined.
04:37:28 -!- arjanb has quit (Quit: zzz).
04:37:58 <Sgeo> There exists a web browser written in Node.js
04:40:32 -!- skj3gg has quit (Quit: ZZZzzz…).
04:40:45 <copumpkin> can't get much more isomorphic than that
04:46:33 -!- skj3gg has joined.
04:54:40 -!- fractal has quit (Ping timeout: 272 seconds).
05:05:54 -!- skj3gg has quit (Quit: ZZZzzz…).
05:16:50 -!- skj3gg has joined.
05:16:50 -!- skj3gg has quit (Client Quit).
05:20:21 -!- shikhin has quit (Ping timeout: 252 seconds).
05:36:28 -!- v^ has joined.
05:40:16 -!- ^v^v has quit (Ping timeout: 272 seconds).
05:43:53 -!- nys has quit (Quit: quit).
05:48:25 -!- Eolus has joined.
05:57:25 <Eolus> Hello
05:58:24 -!- Sprocklem has quit (Ping timeout: 246 seconds).
06:01:33 <MDude> Hi
06:14:51 -!- Patashu has quit (Ping timeout: 256 seconds).
06:15:34 -!- Patashu has joined.
06:42:36 -!- oerjan has joined.
07:46:13 -!- hjulle has joined.
07:46:20 -!- v^ has quit (Read error: Connection reset by peer).
07:54:55 <zzo38> Did you study my Magic: the Gathering puzzle.3 by now? Or you don't?
07:57:59 -!- Patashu has quit (Quit: Soundcloud (Famitracker Chiptunes): http://www.soundcloud.com/patashu MSN: Patashu@hotmail.com , AIM: Patashu0 , YIM: patashu2 , Skype: patashu0 .).
08:04:02 -!- Patashu has joined.
08:04:40 -!- MDude has changed nick to MDream.
08:11:52 <oerjan> has reddit changed its comment font?  i suddenly find it harder to read :(
08:16:36 <oerjan> it's sans serif now, i don't remember if it used to be
08:17:43 -!- Eolus has quit (Quit: Connection closed for inactivity).
08:20:58 <oerjan> actually, i think it's just increased the size of the font one step too much
08:21:33 <oerjan> changing text size to small made it look normal
08:53:07 -!- adu has quit (Quit: adu).
08:58:42 <zzo38> A chess rating system with inflation could involve that a game is (e^(tr)) points where e is the base of natural logarithms, t is the timestamp in seconds since the epoch (you can change the epoch in order to rescale; all ratings are then recomputed), and r is the inflation rate in hertz. The system is of course more complicated than just that, but that can be one of the components of a system.
09:00:50 <zzo38> Do you think it can be worked?
09:12:08 <Jafet> Why do you want inflation?
09:14:26 <oerjan> everyone knows deflation is harmful
09:18:14 <zzo38> So that more recent points winning/losing is worth more.
09:28:25 <Jafet> You could use a model that assigns each player not only an estimated rating, but also an estimated rating rate of change
09:32:20 <Jafet> An exponential inflation rate won't work because if, say, an IM plays against a GM who hasn't played (in rated tournament games) for several years, the IM would start with a higher rating even though he is expected to lose
09:47:55 -!- GeekAfk has quit (Ping timeout: 256 seconds).
09:48:43 -!- zzo38 has quit (Ping timeout: 255 seconds).
09:54:49 -!- zzo38 has joined.
09:54:55 <zzo38> Sorry, it was connection error
09:56:08 <zzo38> The purpose of this rating system I try to make up isn't exactly the same as things such as Elo anyways.
09:57:15 -!- AnotherTest has joined.
09:59:50 <zzo38> Also, event bonuses would be part of the system too.
10:02:53 -!- GeekDude has joined.
10:03:09 -!- GeekDude has changed nick to Guest42916.
10:05:00 -!- zzo38 has quit (Ping timeout: 272 seconds).
10:09:09 -!- zzo38 has joined.
10:10:03 <zzo38> Event bonuses would be based on different expectations calculated for each event. No wins/losses are calculated at all outside of a tournament. If you play outside of a tournament, your score is safe.
10:13:27 -!- nyuszika7h has quit (Remote host closed the connection).
10:17:52 -!- nyuszika7h has joined.
10:24:17 -!- oerjan has quit (Quit: leaving).
10:26:46 -!- chaosagent has quit (Ping timeout: 265 seconds).
10:54:06 -!- dianne has quit (Quit: byeannes).
10:58:08 <mroman> Wouldn't systems using average rank be way better?
10:59:01 <zzo38> I don't know?
10:59:53 <mroman> If you win as the lower player you switch ranks with your opponent
11:00:04 <mroman> for example if you play as rank 5 against a rank 3 
11:00:09 <mroman> then the average ranks are 5 and 3
11:00:12 <mroman> if you win
11:00:21 <mroman> you'll be promoted to rank 3 and he'll go down to rank 5
11:00:30 <mroman> which means both have an average rank of 4 now
11:00:33 <mroman> you'll play again
11:00:37 <mroman> and you'll win again
11:00:45 <mroman> both stay at their ranks
11:00:48 <mroman> > (3+3+5)/3
11:00:51 <lambdabot>  3.6666666666666665
11:01:01 <mroman> is then the new average rank of the winning player
11:01:02 <mroman> and
11:01:07 <mroman> > (3+5+5)/3
11:01:09 <lambdabot>  4.333333333333333
11:01:15 <mroman> will be the rank of the loosing player
11:03:05 <mroman> (Obviously there are two rankings then. The current ranking and the ranking based on average ranking)
11:11:06 -!- Taneb has changed nick to Tabneb.
11:14:27 -!- Tabneb has changed nick to Taneb.
11:19:26 -!- J_Arcane has quit (Quit: ChatZilla 0.9.91-rdmsoft [XULRunner 32.0.3/20140923175406]).
11:20:26 -!- boily has joined.
11:47:01 -!- J_Arcane has joined.
11:48:13 -!- J_Arcane has quit (Remote host closed the connection).
11:53:43 -!- Patashu has quit (Ping timeout: 256 seconds).
11:56:00 -!- J_Arcane has joined.
12:03:16 -!- Guest42916 has quit (Quit: ZNC - http://znc.in).
12:07:35 -!- GeekDude has joined.
12:07:35 -!- GeekDude has changed nick to Guest73330.
12:12:44 -!- AnotherTest has quit (Ping timeout: 245 seconds).
12:12:56 -!- ais523 has quit (Ping timeout: 272 seconds).
12:16:07 -!- Guest73330 has quit (Quit: ZNC - http://znc.in).
12:18:53 -!- boily has quit (Quit: ACOUSTIC CHICKEN).
12:20:55 -!- AnotherTest has joined.
12:44:40 -!- ais523 has joined.
13:05:21 -!- TieSleep has left.
13:06:39 -!- TieSoul has joined.
13:10:37 -!- ais523 has quit (Ping timeout: 265 seconds).
13:24:13 -!- callforjudgement has joined.
13:28:44 -!- scarf has joined.
13:28:53 -!- scarf has quit (Changing host).
13:28:54 -!- scarf has joined.
13:30:03 -!- callforjudgement has quit (Ping timeout: 256 seconds).
13:45:22 -!- scarf has quit (Read error: No route to host).
13:45:36 -!- scarf has joined.
13:46:47 -!- scarf has changed nick to ais523.
14:05:35 -!- Eolus has joined.
14:06:32 <Eolus> oerjan its always been sans serrif
14:13:31 -!- variable has quit (Quit: I found 1 in /dev/zero).
14:45:57 <HackEgo> [wiki] [[User:InputUsername]] M http://esolangs.org/w/index.php?diff=41729&oldid=41598 * InputUsername * (+82) Added qq implementation
14:46:41 -!- SopaXorzTaker has joined.
14:52:57 -!- ais523 has quit (Read error: Connection reset by peer).
14:53:34 -!- ais523 has joined.
14:59:06 -!- trn has quit (Ping timeout: 276 seconds).
15:01:10 -!- variable has joined.
15:01:10 -!- variable has quit (Changing host).
15:01:10 -!- variable has joined.
15:02:55 -!- trn has joined.
15:04:13 -!- skj3gg has joined.
15:06:47 -!- skj3gg has quit (Client Quit).
15:09:45 <HackEgo> [wiki] [[Brainfuck implementations]]  http://esolangs.org/w/index.php?diff=41730&oldid=41345 * 68.227.98.57 * (+107) /* Normal implementations */
15:12:53 -!- ais523 has quit (Ping timeout: 252 seconds).
15:20:58 -!- nycs has joined.
15:20:58 -!- nycs has changed nick to `^_^v.
15:22:38 -!- skj3gg has joined.
15:24:16 -!- GeekDude has joined.
15:25:59 -!- nys has joined.
15:28:19 -!- skj3gg has quit (Quit: ZZZzzz…).
15:33:55 -!- skj3gg has joined.
15:35:28 -!- ais523 has joined.
15:48:23 <FireFly> they did increase the font size (and other small changes): https://www.reddit.com/r/changelog/comments/2tw6pm/reddit_change_changes_to_default_text_styling/
15:49:09 -!- Phantom_Hoover has joined.
15:51:37 <GeekDude> Huh
15:51:43 <GeekDude> I was thinking the font was slightly different
15:53:32 <mroman> Ok
15:53:35 <mroman> I guess reddit sucks then
15:54:33 <mroman> Websites shouldn't set a font-size.
15:54:54 <mroman> maybe for headings
15:55:03 <mroman> but only in terms of relative to default font-size
15:55:20 <GeekDude> oley moley
15:55:25 -!- ais523 has quit (Ping timeout: 252 seconds).
15:55:28 <GeekDude> Someone did something to the headers
15:55:36 <GeekDude> http://i.imgur.com/T6Vym68.png
16:00:24 -!- shikhin has joined.
16:18:01 -!- skj3gg has quit (Quit: welp, see you later.).
16:19:05 <int-e> and this is why forums are fundamentally broken. you're forced to use the front-end as provided by some website.
16:19:35 <int-e> rather than, say, your favourite news reader. (oh Usenet, I have not seen you for ages)
16:21:27 -!- arjanb has joined.
16:27:40 <int-e> "Well, this is h1. It should be really big."
16:27:56 <int-e> yeah, well, true. but you just know people are going to abuse it for emphasis.
16:28:16 <mroman> See
16:28:24 <mroman> That would be totally different with CoolHTML
16:28:40 <int-e> (I saw GeekDude's screenshot. I don't need more demonstration.)
16:28:52 <int-e> mroman: we had a better world. it was called plain text.
16:29:25 <mroman> we had a better world. it was called messenger pigeons.
16:30:37 <mroman> but no seriously
16:30:42 <mroman> we need CoolHTML .
16:31:13 -!- mihow has joined.
16:31:28 <int-e> You may, I don't think I do. I'm averse to "cool", it makes me shiver.
16:34:02 <int-e> you know what upsets me more than sites arbitrarily changing their layouts though ...
16:34:09 -!- skj3gg has joined.
16:34:32 <int-e> ... is that different sites have font sizes that vary by orders of magnitude (at least that's what it feels like).
16:35:24 -!- trnv2 has joined.
16:35:54 <int-e> oh and that 'px' still hasn't died out in CSS.
16:37:29 -!- trn has quit (Ping timeout: 265 seconds).
16:37:43 -!- Eolus has quit (Quit: Connection closed for inactivity).
16:39:22 <int-e> (e.g. the esoteric codes site has a huge font. must be a blog thing.)
16:41:38 -!- SopaXorzTaker has quit (Read error: Connection reset by peer).
16:42:40 -!- SopaXorzTaker has joined.
16:42:50 -!- trnv2 has changed nick to trn.
16:43:01 <mroman> I'm still experimenting with http://mroman.ch/designs/d2/
16:43:02 -!- skj3gg has quit (Quit: ZZZzzz…).
16:44:20 -!- skj3gg has joined.
16:44:29 <mroman> Next thing I gotta do some boxes and buttons that scale well across different displays
16:44:48 <mroman> the first thing for smartphones is websites that have ads on the left
16:44:56 <mroman> because those ads just take away so much space 
16:47:43 <mroman> I hate websites that require zoom to function well
16:47:51 -!- zzo38 has quit (Remote host closed the connection).
16:47:58 <mroman> some websites use incredibly small font-sizes for links
16:48:14 <mroman> so to click them you have to zoom in a lot 
16:51:46 -!- oerjan has joined.
16:55:30 -!- skj3gg has quit (Quit: ZZZzzz…).
16:59:28 -!- dianne has joined.
17:08:09 -!- bb010g has quit (Quit: Connection closed for inactivity).
17:15:03 -!- ^v has joined.
17:19:28 -!- Tritonio_ has joined.
17:21:27 -!- Tritonio has quit (Ping timeout: 276 seconds).
17:26:16 -!- Tritonio_ has changed nick to Tritonio.
17:33:23 -!- vanila has joined.
17:33:23 <vanila> hi
17:34:14 <vanila> https://gist.github.com/ahmadsalim/11077308
17:34:16 <vanila> Proof that Agda is Turing complete
17:34:39 <vanila> what do you think :/
17:34:43 <vanila> I don't agree
17:34:55 -!- skj3gg has joined.
17:43:17 <elliott> https://github.com/wouter-swierstra/Brainfuck mcbride makes this point a lot too
17:43:28 <elliott> (uh, not to imply that's mcbride)
17:48:52 <int-e> vanila: Looks acceptable to me.
17:49:06 <int-e> vanila: what's your objection?
17:49:25 <int-e> elliott: the README is missing a negation, isn't it?
17:49:59 <vanila> I don't understand what point wouter is trying to make
17:50:21 <int-e> "I get tired of explaining that totality is not the same as Turing completeness." <-- I think he means "incompleteness" there.
17:50:49 <elliott> vanila: that there's no reason the RTS can't follow codata like it follows IO actions
17:50:59 <elliott> Agda's IO monad is codata so it's TC I guess
17:51:08 <vanila> wow
17:51:11 <elliott> (as in, agda is TC in the same way that haskell can do IO)
17:52:19 <elliott> (conor also likes making the point that even for programs which don't terminate in practice, we generally don't want full partiality: for instance, a server should run forever, but it should always respond to requests in finite time -- i.e. unless the task is "implement a TC language", you can probably do better modelling things with a notion of productivity than just a full-blown partiality monad)
17:54:26 <int-e> (Tangentially related, stream fusion has streams (which are codata) with a Skip constructor because that avoids recursion, leading to better inlining...)
17:54:42 <int-e> (And I don't know why I thought of this now.)
17:54:57 <vanila> for some reason my view of 'turing complete' is about the functions N -> N you can implement
17:55:02 <vanila> and it's not TC in that respect
17:55:14 <vanila> but it IS TC in a looser sense I guess
17:55:34 <elliott> it's meant more as a rebuttal to people being, like, well, agda is total, so it's not TC, so you couldn't use it for writing real programs
17:55:50 <elliott> especially interpreters, etc.
17:56:03 -!- skj3gg has quit (Quit: ZZZzzz…).
17:57:38 <int-e> vanila: Right, here the view taken is that of a decision problem (i.e. the machine accepts some language L, with acceptence indicated by program termination.)
17:58:24 <int-e> right, codata is essential because now totality does not imply termination anymore.
17:59:40 <int-e> And that's how the argument goes: because the programs are total function, they have to terminate on all inputs, and therefore the language can't be TC.
17:59:53 <elliott> we would accept this as proof of agda being TC on the esowiki, say
18:00:08 <elliott> because we don't look at the internals of programs to see exactly how they're implemented when making that call
18:00:16 <elliott> (well, other than to verify it really has infinite memory etc.)
18:00:28 <vanila> I feel like it is misleading to tell people agda is turing complete
18:00:45 <int-e> Also in any paper in theoretical computer science, provided we say something about how to produce the `main` function in general.
18:01:25 <elliott> I feel like it's misleading to tell people it's sub-TC
18:01:34 <elliott> total : pure
18:01:38 <elliott> turing-complete : can do IO
18:02:03 <elliott> "haskell is useless, it's pure so it can't do any IO so you can't write real programs!" "haskell is pure, but we can do IO (even though a function (a -> b) is pure), by using the top-level 'main'"
18:02:07 <int-e> vanila: Clearly we need more than a single statement (Agda is [not] TC.) to do Agda justice.
18:02:14 <vanila> I thought an coinductive execution trace of a small step interpreter 
18:02:22 <vanila> was the same as 'run n steps' of a small step interpreter
18:02:29 <elliott> "agda is useless, it's total so it's not turing complete so you can't write real programs!" "agda is total, but we can do partiality (even though a function (a -> b) is total) by using the top-level 'main'"
18:02:34 <int-e> "Haskell is useless, everything it can express is constant."
18:02:35 <vanila> and you can do that in many non turing complete languages, it's run infinity steps that makes somethin TC
18:02:45 <elliott> vanila: but you can do that
18:02:51 <vanila> im not telling people agda is useless:/
18:02:54 <elliott> you could write an agda "main" that just follows that execution trace
18:03:00 <elliott> printing the output as it goes
18:03:02 <elliott> and then run that
18:03:08 <elliott> and it would halt iff the BF program does
18:03:29 <elliott> that module should probably have a main but I don't know how experimental/usable agda's IO stuff is
18:03:48 <elliott> but it's at least possible in theory because agda's IO is analoguous to that Trace
18:03:55 <elliott> *analogous
18:04:46 <int-e> Does Agda have something like   codata Compute a = Result a | Later (Compute a)  with machinery to live functions from base types to that stream type?
18:04:51 -!- SopaXorzTaker has quit (Ping timeout: 264 seconds).
18:05:25 <elliott> I think it has the partiality monad somewhere, yes, maybe not in the stdlib
18:05:29 <elliott> people have definitely written it up though
18:05:36 -!- skj3gg has joined.
18:05:54 <int-e> because then the answer to vanila's complaint becomes, well, if f : N -> N  doesn't always terminate, then you can still write  f : N -> Compute N.
18:06:20 -!- Froox has quit (Ping timeout: 244 seconds).
18:06:20 -!- Frooxius has joined.
18:06:26 -!- SopaXorzTaker has joined.
18:09:28 <int-e> wow. s/live/lift/ up there
18:09:53 <int-e> (worryingly, a spell checker wouldn't have helped me.)
18:11:37 -!- SopaXorzTaker has quit (Quit: Got to go).
18:12:24 -!- mihow has quit (Quit: mihow).
18:13:23 -!- skj3gg has quit (Quit: ZZZzzz…).
18:15:34 -!- skj3gg has joined.
18:17:30 -!- mihow has joined.
18:25:14 -!- mihow has quit (Quit: mihow).
18:26:16 -!- skj3gg has quit (Quit: ZZZzzz…).
18:26:34 -!- skj3gg has joined.
18:31:48 -!- mihow has joined.
18:57:12 -!- skj3gg has quit (Quit: ZZZzzz…).
19:14:20 -!- nycs has joined.
19:14:53 -!- `^_^v has quit (Ping timeout: 252 seconds).
19:15:58 -!- skj3gg has joined.
19:17:02 -!- skj3gg has quit (Client Quit).
19:19:38 -!- ski has quit (Read error: Connection reset by peer).
19:19:48 -!- Phantom_Hoover has quit (Ping timeout: 272 seconds).
19:27:15 -!- skj3gg has joined.
19:30:15 -!- kcm1700_ has quit (Remote host closed the connection).
19:32:06 -!- TieSoul has changed nick to TieSleep.
19:35:27 -!- kcm1700 has joined.
19:37:06 -!- nys has quit (Quit: quit).
19:44:08 <oerjan> int-e: behold my typeable monster
19:46:29 <oerjan> i'm not sure whether the Proxies or the UndecidableInstances are the worst
19:46:49 <oerjan> (https://ghc.haskell.org/trac/ghc/ticket/9858#comment:33)
19:48:57 * Melvar wonders if he can get cabal-install to only spit out a solution …
19:49:30 <oerjan> Melvar: have you tried -dry-run ?
19:50:00 <oerjan> (possibly with two -s, i never remember)
19:51:50 -!- Phantom_Hoover has joined.
19:52:36 <int-e> oerjan: beautiful.
19:53:36 <Melvar> oerjan: Well, that doesn’t look very machine-readable, though I guess it will work, and I think I need to set up a completely empty packageDB somehow for it to tell me everything.
19:54:23 <oerjan> Melvar: well that's as far as my expertise on getting output from cabal-install goes, i'm afraid
19:55:59 -!- MDream has quit (Quit: later chat).
19:57:21 <int-e> oerjan: to be useful you'll also need something like  instance (Typeable' (a :: k -> k'), Typeable' (b :: k)) => Typeable' (a b), I think?
19:57:47 <oerjan> int-e: well sure, but that's already in the current implementation afaik
19:58:09 <oerjan> i was just trying to include the basic PoC
20:00:10 <int-e> oerjan: it's just that Kindable will infect that one now. instance (Kindable' (Proxy :: k' -> *), Typeable' (a :: k -> k'), Typeable' (b :: k)) => Typeable' (a b) where
20:00:21 <int-e> oerjan: I thought it'd be harder.
20:01:35 <int-e> oerjan: and the proxies are worst. UndecidableInstances is generally harmless.
20:01:54 <oerjan> yes, i'm just wondering about it infecting everything
20:01:59 <oerjan> that uses Typeable
20:03:45 -!- skj3gg has quit (Quit: ZZZzzz…).
20:03:50 <oerjan> i assume both of the uglinesses would go away if kinds could be instances directly.
20:05:39 -!- Patashu has joined.
20:07:18 -!- skj3gg has joined.
20:07:23 <oerjan> which i vaguely think may be planned to happen as part of richard eisenberg's experiments?
20:07:33 -!- S1 has joined.
20:10:28 <oerjan> unless it's already happened, in which case this could be immediately simplified.
20:10:50 <int-e> oerjan: I'm confused: http://lpaste.net/3318663114416717824
20:11:33 <int-e> (ghc's error messages are extremely unhelpful without kinds)
20:12:06 <oerjan> i have noticed
20:13:47 -!- skj3gg has quit (Quit: ZZZzzz…).
20:14:04 <oerjan> ah yes, the added Kindable contexts is of course the ugliest part of this.
20:14:45 -!- skj3gg has joined.
20:15:04 <int-e> but as indicated I feel that there's some weakness in the instance checker there...
20:15:32 -!- evalj has joined.
20:15:39 -!- shikhin_ has joined.
20:15:39 <oerjan> this is similar to the final change i had to do to make it compile
20:16:42 <oerjan> int-e: it's actually rather simple.  you cannot deduce from  Kindable' (Proxy :: (k1 -> k2) -> *)   to    Kindable' (Proxy :: k -> *)  because of the open world assumption; the first instance _could_ come from somewhere else.
20:17:35 <oerjan> i had to change ((k -> *) -> *) to (k -> *) in the context of the Typeable' Proxy instance for similar reasons
20:17:42 <int-e> right. sigh.
20:18:43 -!- shikhin has quit (Ping timeout: 255 seconds).
20:19:08 <oerjan> i'm afraid similar stuff is going to make this very annoying to _use_, as well :(
20:20:36 <oerjan> the worst part was that it couldn't deduce Kindable' (Proxy ((k -> *) -> *) in the where clause  from Kindable' (Proxy ((k -> *) -> *) in the context
20:21:16 <oerjan> i assume it used instance resolution on the latter _before_ checking if it was in the context, leading to something that wasn't.
20:21:47 <oerjan> oh well.
20:25:30 <oerjan> <FireFly> they did increase the font size (and other small changes): https://www.reddit.com/r/changelog/comments/2tw6pm/reddit_change_changes_to_default_text_styling/ <-- i see the top comment is someone having essentially the same reaction as me.  let's hope there's enough backlash.
20:25:50 -!- Patashu has quit (Ping timeout: 244 seconds).
20:42:26 -!- skj3gg has quit (Quit: ZZZzzz…).
20:52:15 -!- skj3gg has joined.
20:52:17 -!- vanila has quit (Quit: Leaving).
20:52:32 -!- evalj has quit (Remote host closed the connection).
20:53:28 -!- skj3gg has quit (Client Quit).
20:54:23 -!- skj3gg has joined.
20:59:39 <int-e> oerjan: this looks a bit less infectious: http://lpaste.net/1496357053919133696
21:06:13 -!- int-e has quit (Ping timeout: 256 seconds).
21:06:26 <oerjan> oops
21:06:34 -!- nyuszika7h has quit (Remote host closed the connection).
21:07:37 -!- Deewiant has quit (Ping timeout: 264 seconds).
21:11:33 -!- conehead has quit (Ping timeout: 276 seconds).
21:11:50 -!- int-e has joined.
21:11:59 <int-e> hmpf.
21:12:51 -!- skj3gg has quit (Quit: ZZZzzz…).
21:13:02 -!- nyuszika7h has joined.
21:13:14 -!- skj3gg has joined.
21:13:18 <oerjan> fpmh?
21:13:23 * Melvar discovers why idris depends on wai.
21:15:25 -!- skj3gg has quit (Client Quit).
21:16:53 -!- conehead has joined.
21:19:20 -!- skj3gg has joined.
21:21:07 -!- PinealGlandOptic has quit (Ping timeout: 244 seconds).
21:25:35 <int-e> oerjan: ok, cleaning up a bit: http://lpaste.net/4263409010180358144
21:29:55 <elliott> Melvar: go on
21:31:32 <Melvar> elliott: idris uses cheapskate to parse markdown, and cheapskate has an optional executable that depends on wai, which apparently causes it to be pulled in.
21:31:35 <oerjan> int-e: btw they're planning to make typereps typed, that's what the TTypeRep stuff was about.
21:33:40 <oerjan> int-e: you better post that on the trac thread
21:33:56 -!- skj3gg has quit (Quit: welp, see you later.).
21:34:01 -!- Deewiant has joined.
21:39:54 <int-e> oerjan: hmm, I missed the typed typereps.
21:40:17 <int-e> oerjan: anyway, I added to the ticket
21:41:52 -!- nys has joined.
21:43:02 <int-e> oerjan: but anyway this was a great insight from your side, that the kind-level -> can be pattern matched against.
21:46:13 <int-e> oerjan: I would really like TypeRep to be an open GADT ;-)  (see http://lpaste.net/110434 for the reason. Of course there's prior art for this.)
21:47:35 <int-e> (Prior art: This is essentially how GRIN (jhc) works, as far as I understand it.)
21:59:13 -!- aretecode has joined.
22:14:08 <oerjan> mhm
22:22:56 <int-e> oerjan: hmh?
22:27:13 <oerjan> tht?
22:29:06 <oerjan> argh
22:29:57 <oerjan> every month my cookie for the reddit adserver expires and i get to see that bloody r/sciencefiction ad again
22:30:58 <elliott> what is it
22:31:57 <oerjan> http://static.adzerk.net/Advertisers/f1cd14ed8b3b4dffaadcc42bc8313180.jpg may be it
22:33:49 <elliott> this is a weird ad
22:34:02 <elliott> I hear there are browsers that can do ad blocking these days, hth
22:34:09 <oerjan> WHOA
22:34:32 <oerjan> (it's the only disturbing ad i've seen on reddit)
22:37:03 -!- S1 has quit (Quit: S1).
22:38:42 <int-e> A disturbed oerjan? My mind boggles!
22:39:00 <oerjan> it happens!
22:39:19 <mroman> disturbing in what way?
22:41:36 <mroman> http://img.izismile.com/img/img6/20130710/640/disturbing_and_revolting_facts_about_the_human_body_640_09.jpg
22:41:57 <mroman> (Don't click on that link if you are easily disturbed)
22:42:17 <oerjan> i won't hth
22:43:01 <mroman> It's just a human head without skin
22:43:18 <mroman> i.e. the cranium
22:44:29 <mroman> I guess you shouldn't google for open luxation then
22:44:43 <mroman> or smoker's leg
22:45:05 <elliott> let's not
22:45:15 <mroman> There's this game where who ever can look at the most disturbing picture wins
22:45:21 <mroman> It's a fun game
22:46:27 -!- Tritonio has quit (Ping timeout: 276 seconds).
22:47:36 -!- bb010g has joined.
22:47:44 <mroman> oerjan, elliott: Did you watch the Saw movies?
22:48:07 <elliott> no
22:48:20 <mroman> I see
22:49:17 <oerjan> pretty sure not hth
22:50:23 <mroman> Yeah
22:50:27 <mroman> Just download them all
22:50:34 <mroman> then watch them all in a marathon
22:50:48 <mroman> You won't be the same 
22:50:53 <olsner> or better yet, don't do that
22:51:08 <olsner> (hth)
22:51:27 <mroman> nah
22:52:03 <mroman> Just repeat the procedure until it doesn't disturb you anymore ;)
22:52:56 -!- spiette has quit (Quit: :qa!).
22:54:49 <mroman> I think it's called exposition training
22:55:20 <mroman> hm
22:55:22 <mroman> exposure training
22:55:24 <mroman> i see
23:00:04 <mroman> oh well
23:00:10 <mroman> I should go to sleep
23:00:34 <mroman> Or watch Saw I
23:00:36 <mroman> hm
23:01:35 <oerjan> sleep, or never sleep again, that's the question
23:02:02 <oerjan> and girl genius is back to late update again
23:02:09 -!- nycs has quit (Quit: This computer has gone to sleep).
23:02:38 <int-e> well, they still have a couple of hours left of yesterday
23:03:54 <oerjan> more than that if they go by seattle time
23:04:17 <int-e> that was "a couple" as in "a few" rather than "two", hth.
23:04:22 <oerjan> fiendish
23:05:56 <int-e> in the meantime I'm impressed by whio's handling of that 101 scrabble words data compression task.
23:06:26 <int-e> I expected solutions below 100 bytes. I didn't expect 74.
23:14:02 -!- adu has joined.
23:16:42 -!- Tritonio has joined.
23:17:32 -!- Lymia has quit (Ping timeout: 246 seconds).
23:20:07 -!- Tritonio has quit (Remote host closed the connection).
23:20:26 -!- Tritonio has joined.
23:23:36 -!- AnotherTest has quit (Remote host closed the connection).
23:23:53 -!- Eolus has joined.
23:24:19 <Eolus> Hi
23:25:45 <int-e> Oh Lilax.
23:26:05 <int-e> you don't pay attention for a day and more than 1% of the populace has a new name. Sigh :)
23:26:53 <Eolus> ?!
23:26:54 <lambdabot> Maybe you meant: v @ ? .
23:27:03 <Eolus> Yes I meant @
23:27:12 <Eolus> What int-e 
23:27:51 <Eolus> Everyone seems the same on the list?
23:28:41 <int-e> Okay, so it's been two days.
23:29:44 <Eolus> Yes?! it has
23:30:14 <Eolus> But lilax was here yesterday int-e
23:30:47 <int-e> wasn't.
23:30:54 <Eolus> Ah
23:31:04 <Eolus> But what are you talking about
23:31:13 <int-e> --- Lilax is now known as Eolus <-- that was 2 days ago.
23:31:21 <Eolus> Ye
23:31:26 <Eolus> We switched
23:31:31 <Eolus> Silly int-e 
23:31:59 <int-e> `welcome Eolus 
23:32:00 <HackEgo> Eolus: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on irc.dal.net.)
23:32:23 <Eolus> Non
23:32:33 <Eolus> Why would you welcome me
23:33:15 <int-e> Well since you pretend not to be Lilax I don't think you've been welcomed before.
23:33:45 <Eolus> please stop calling me lilax :l
23:36:26 <int-e> fungot?
23:36:26 <fungot> int-e:. i'm so kind, even to assholes! anmaster no not markov anmaster no not markov anmaster no not markov anmaster no not markov anmaster no not markov
23:37:00 <int-e> fizzie: that loop is also nice :)
23:37:31 <elliott> the best part is the "nick:."
23:37:34 <elliott> because of the punctuation handling
23:37:38 <int-e> fungot: try this again  try this again  try this again
23:37:39 <fungot> int-e:, so i'd be happy to help an fnord archive) x) bug? when i looked at it" and enjoy knowledge, and its kind, but my watch it toast? or decide. fnord 22:11, 17, 18, 19, 20, 21, 22, 22, 22, 22, 22, 22, 22, 22, 22, ...too much output!
23:39:26 -!- oerjan has quit (Quit: . Nite).
23:46:15 -!- hjulle has quit (Ping timeout: 264 seconds).
23:57:26 -!- Lymia has joined.