←2013-07-27 2013-07-28 2013-07-29→ ↑2013 ↑all
00:01:18 <zzo38> I think the mirrors act like they do in Floyd's Bumpershot (a game I have read about somewhere; I haven't played). Adding the other pieces of that game and of Black Box game, can make it a generalized version of those game; I already said the computer tells you ahead of time how many mirrors, how many arrows, etc; you could also make the user configure the possible range of how many. Now it can make a superset of these games.
00:02:05 -!- doesthiswork has joined.
00:09:30 <oerjan> there's also the undead puzzle from tatham's collection that is a bit similar.
00:10:06 <oerjan> hm didn't doesthiswork say something in the logs i wanted to quibble about :P
00:10:16 <doesthiswork> yes?
00:10:27 <oerjan> i've just forgotten what it was
00:10:45 <doesthiswork> probably something about lambda calc fixed points
00:11:07 <Sgeo> I am addicted to Listerine PocketPak strips
00:12:26 <oerjan> oh right. i think the others shot that down for me. what i wanted to say is that the fixed point theorem doesn't apply to _typed_ lambda calculus, because the types are usually specifically made to avoid nontermination (without explicit recursion), which is essential to construct the usual diagonal argument.
00:18:18 <doesthiswork> ok
00:19:22 <oerjan> or perhaps equivalently, the fixed point theorem is incompatible with types that give you a curry-howard isomorphism with a consistent logic.
00:20:09 <oerjan> which looked like what you were trying to look at
00:20:32 -!- yorick has quit (Remote host closed the connection).
00:21:26 <doesthiswork> What have people used the fixed point theorem to prove?
00:25:38 -!- copumpkin has quit (Ping timeout: 246 seconds).
00:25:46 <oerjan> that you can do arbitrary recursive computations?
00:26:14 -!- copumpkin has joined.
00:26:31 <oerjan> i am not aware of any more technical uses
00:27:45 <oerjan> i suppose it also destroyed church/curry's original attempts to do logic in lambda calculus/combinatory logic without any types
00:28:05 <oerjan> which may be what you have rediscovered
00:28:25 <doesthiswork> Yes, that is exactly the problem I was trying to understand
00:29:20 <oerjan> and it does this in a way that is similar to how russell's paradox destroyed naive set theory, i think. in fact they are both diagonal arguments.
00:29:55 <oerjan> as are godel's incompleteness theorem and turing's halting problem proof
00:29:59 <oerjan> *gödel
00:30:50 <oerjan> a great deal of rampage and destruction from just one basic proof idea, there.
00:31:03 <doesthiswork> yes, it is wonderful
00:31:20 <oerjan> there are also the complexity hierarchy theorems, which might not be considered destructive.
00:32:03 <zzo38> Is the typed lambda calculus basically like what Hofstadter called "rule of detachment" and "fantasy rule" (also, as it says, often called the "Modus Ponens" and "Deduction Theorem")?
00:33:52 <oerjan> zzo38: um there's the curry-howard isomorphism with intuitionistic propositional logic terms in -> , those would both be rules of that so i suppose they are included...
00:34:14 <oerjan> oh hm
00:34:23 <zzo38> Yes, of intuitionistic logic, I know, not of classical
00:34:33 <oerjan> you mean application is like modus ponens and lambda is like the deduction theorem?
00:34:43 <oerjan> when you look at what they do to types
00:34:45 <zzo38> Yes.
00:34:56 <oerjan> i suppose so, yes
00:37:59 -!- brainstorming has joined.
00:38:54 -!- brainstorming has left.
00:39:17 <zzo38> What would be the shortest possible sequent calculus which is Turing complete?
00:40:57 <zzo38> Do Wang tiles remain Turing complete when generalized to different geometries?
00:41:13 <doesthiswork> I would expect so
00:42:00 <doesthiswork> if you restricted them to a finite area they wouldn't
00:42:33 <zzo38> Yes, I know, I mean geometries which have infinite areas?
00:43:43 <doesthiswork> since you can embed 2d wang tiles in any such geometrty I would have to say yes they'd still be turing equivalent
00:45:44 <zzo38> But what if the tiles are triangular or something like that?
00:47:41 <doesthiswork> stick two triangles together and you have a parallelogram. Tile the plane with this shape
00:50:41 <doesthiswork> (I don't know how to embed 2 dimensions in a one dimensional line)
00:51:05 <zzo38> O, yes, you can make a parallelogram like that, if you add an extra color.
00:56:05 <oerjan> doesthiswork: i am pretty sure one-dimensional tiling is _not_ TC (should be a finite automaton, essentially)
00:58:14 <doesthiswork> Then I wonder what the minimum number of dimensions needed for a tiling to be TC. I think 1.5 is possible
01:02:20 <oerjan> i am not sure that fractal dimensions are compatible with tilings.
01:02:51 <oerjan> maybe they are, though
01:05:09 <doesthiswork> I think the serpinski triangle could host a TC wang tiles.
01:06:35 <doesthiswork> *take out the 'a'
01:06:54 <oerjan> **-a
01:07:54 <doesthiswork> thank you
01:16:02 -!- sacje has quit (Ping timeout: 246 seconds).
01:18:16 <tswett> zzo38: are Wang tiles a sequent calculus?
01:18:55 <tswett> And what does it mean for a sequent calculus to be TC? Does it mean that there's a such-and-such which maps Turing machines onto statements in the calculus such that the statement is provable if and only if the machine halts?
01:33:06 <oerjan> sounds like the obvious interpretation, anyway
01:34:06 <zzo38> tswett: I don't know, maybe it would be possible to make a sequent calculus of Wang tiles but I don't know
01:34:44 <zzo38> tswett: Yes, that is what I mean by a sequent calculus to be TC (and I have made a set of sequent calculus rules which implement a Turing machine).
01:37:56 <zzo38> I have also made up a way to interpret a sequent calculus as an asymmetric game (although the initial state isn't a part of these rules; it must be decided separately somehow). Put the initial state at the bottom, and follow the rules going up. The first player's job is to select a rule and substitutions in it. The second player's job is to select one of the sequents above the line in that rule. Whoever has no legal move loses.
01:41:02 <zzo38> (Because it is Turing-complete, it is possible to result in a draw, and there isn't necessarily any way to know it is a draw, although sometimes it is possible to tell.)
01:44:05 <tswett> There is a game semantics for linear logic.
01:45:39 <tswett> But I don't really know what its significance is.
01:46:47 <Gracenotes> a lot of things and logics have game semantics, where you have a goal and things which both help and hinder you from reaching that goal.
01:47:43 <zzo38> I think that is a different kind of game semantics though.
01:48:30 <Gracenotes> I like to call them 'adversarial models'. I think they're called that.
01:49:58 <CADD> Gracenotes: now the question is, how do you make a program that will make qualifying and quantifying human knowledge into a logical framework that can be interpreted by computers as fun as a video game!?!
01:50:41 <Bike> "trivial pursuit, forever"
01:52:09 <CADD> you are right, you can never make programming a computer as fun as farmville..
01:52:48 <CADD> actually i take that back, farmville sucks.
01:52:57 <CADD> programming is much better
01:53:05 <doesthiswork> I thought your first statement was sarcastic
01:53:22 <CADD> its a pie in the sky idea
01:53:41 <Gracenotes> human knowledge isn't logical, and it can't be put into a logical framework
01:53:55 <doesthiswork> I have heard of people happily doing repetitive tasks over and over without the slightest thought of automation.
01:53:56 <CADD> well you can create a mapping of the illogic
01:54:00 <Gracenotes> although perhaps you refer to the small subset of human knowledge that has explicit structural representations
01:54:44 <zzo38> Well, you can make some kinds of human knowledge into a logical framework, and some kinds of logical framework can be used for representing human knowledge, but actually it is different things, and their purposes can also vary a lot, and these also aren't the only two things.
01:55:43 <Gracenotes> neurplasticity is pretty remarkable
01:56:17 <Gracenotes> In any case, a lot of pieces of knowledge are not universally true; they come attached with probabilities.
01:56:29 <Gracenotes> with priors, both explicit and implicit
01:56:44 <CADD> right thats true, but there is a lot of data out there that could be structured but isnt.
01:57:06 <CADD> now the question is how do you make structuing that data appealing to a wide, non techinical audience?
01:57:14 <Gracenotes> I 'know' that this car 100ft ahead of me is going to change into my lane in front of the car in front of me within 5 seconds
01:57:16 <CADD> even for vanities sake
01:57:18 <Gracenotes> for instance
01:58:12 <Gracenotes> (without a turn signal, in this case)
01:58:13 <quintopia> such as the relationship between all dongs which contain a particular four note riff
01:58:14 <zzo38> Well, if it helps (or is even the least bit relevant at all), I have made a sequent calculus for sokoban game.
01:58:28 <CADD> as in structuing data about yourself, to create a "social media collage" of the unstructued data available on the internet.
01:58:32 <quintopia> stupid swype
01:58:42 <Bike> dongs
01:58:49 <quintopia> s/dongs/songs/
01:59:03 <Bike> no, i like this one.
02:00:16 <CADD> so although the collage may not have much structured data attached to it, it would be possible to publish this data structure and further integrate it with other structures that people have made.
02:00:45 <Gracenotes> in general, people assume universality a lot more than it actually exists
02:01:07 <Bike> What do you do with the multiple incompatible strucctures obtainable from different social networks?
02:01:49 <Gracenotes> language (both natural and constructed/computer, actually) flattens it into communicable form. Very very restrictive.
02:01:51 <CADD> well, so im trying to see if it is possible to have a semantic network of information slowly built by individual actors
02:02:31 <CADD> so you could create a judgement that "obama is the president". although that would obviously have to have some sort of symbolic representation.
02:02:57 <CADD> and that like i said earlier, it would even be open to vanity statements. such as "this is a picture of what i had for lunch"
02:03:22 <CADD> so now you have all this associations that are only semi structured at this point
02:03:50 <Bike> How do these "judgments" relate to intuitionistic type theory? Or the unstructured information ("intuitions")?
02:03:57 <CADD> the interesting part comes from when a large amount of people agree on the symbolic representation that "obama is the president"
02:05:08 <CADD> or even the minor unimportant details as affirming symbolically that your firend did indeed have what she said for lunch
02:05:23 <CADD> thus adding more weight to the judgement, or proposition
02:06:35 <CADD> any thoughts?
02:06:46 <elliott> what is going on
02:06:54 <CADD> lol, im talking about my crazy idea
02:07:19 <Bike> i already asked questions :-(
02:08:11 <quintopia> stuff
02:08:16 <CADD> right, ok so the most important part is the consensus on symbolic representation of our "common knoledge" in the world. the social media bit is essientially just a hook.
02:08:19 <CADD> Bike: ^
02:08:42 <Bike> But that's where you have to get information from. And people deploy different "personae" on different networks.
02:09:09 * oerjan wonders if Cyc is still around
02:09:15 <CADD> exactly. its not like a spider, but more of a knowledge base.
02:10:15 <CADD> but what im trying to wrestle with is appeal to a general audience.
02:11:37 <CADD> or more generally, how you would interact with the system. so would you be presented with information that affirms or refutes your collection of symbolic expressions.
02:12:54 <CADD> so say you decide to claim that "obama is not the president". it would display the fact that you did, and the cout of times that that symbol has been affirmed and possibly a list of the people that publically affirm that symbol
02:13:38 <CADD> so now you have the affirmation of the symbol that obama is NOT the president. so obviously there will be magnitued more people affirming that he is the president
02:14:18 <CADD> so there is a shared truth value associated with him being the president. say 99% say he is and 1% say he isnt.
02:14:38 <CADD> so thats boring
02:15:22 <CADD> or well, it will be interesting what comes out of it, but in essence its just a massive collection of abstract representations of fact
02:15:42 <CADD> so now how do you present this, or more specifically what?
02:16:48 <CADD> obviously there are some simple things, like creating a profile of the user. and finding individuals that have said similar things, and then present things that these similar individuals have said
02:17:31 <CADD> so essentially it would be similar to "collaborative filtering".
02:18:13 <CADD> but the problem with systems like those is that you are only shown things that agree with your worldview.
02:20:01 <CADD> anyway, like i was saying. this is kind of a pie in the sky idea..
02:20:38 <CADD> but i think its on a thread that we have been attempting to follow for a long time..
02:21:02 <CADD> i mean OWL, RDF and all those technologies failed hardcore
02:21:38 <CADD> and i want to see how to make that an integral part of the general publics experience of the internet.
02:22:11 <CADD> </hand-wavy-rant>
02:23:01 <Gracenotes> the best successes that have been had so far with human-like learning are neural nets
02:23:20 <Gracenotes> in particular, semisupervised deep learning architectures
02:24:24 <CADD> yeah, ive heard similiar things too. i have some experience with NN, they are really interesting. sadly they like all models still suffer from the curse of dimensionality
02:24:49 <CADD> have you heard about hierarchical temporal models?
02:25:04 <CADD> they are really interesting for "streaming" sources of data
02:25:42 <Gracenotes> yes, that's mainly where unsupervised pretraining makes NNs amazing
02:25:42 <CADD> and can pic out not just static patterns, but temporal ones as well. its very interesting.
02:25:54 <Gracenotes> regarding dimensionality curse
02:26:43 <Gracenotes> and I've seen interesting applications of NNs embedded in Bayes nets/fields
02:26:50 <Gracenotes> to represent temporal things
02:27:00 <CADD> interesting
02:27:06 <CADD> do you have any links?
02:27:39 <Gracenotes> http://www.youtube.com/watch?v=VdIURAu1-aU
02:28:08 <Gracenotes> hm, there might be an updated version of this recently released... /me will have to watch it
02:28:10 <CADD> Oh!
02:28:15 <CADD> ive see that video
02:28:26 <CADD> hmm, its been a while though..
02:28:31 <CADD> ill have to rewatch it
02:28:49 <CADD> yeah, i think the HTM is also mentioned in a google tech talk
02:29:13 <Gracenotes> in a talk? hm, do you know which one?
02:29:19 <CADD> i guess not
02:29:20 <CADD> http://youtu.be/48r-IeYOvG4
02:34:38 -!- oerjan has set topic: 22nd IOCCC opens August 1 http://ioccc.org/2013/rules.txt | jsvine is doing an esolang survey!: https://docs.google.com/forms/d/1OvEsdBioOFcXFAiscO34kctUWKs3dWQs5-ZouXdwy9Q/viewform | logs: http://codu.org/logs/_esoteric & http://tunes.org/~nef/logs/esoteric/.
02:34:53 -!- oerjan has set topic: 22nd IOCCC opens August 1: http://ioccc.org/2013/rules.txt | jsvine is doing an esolang survey!: https://docs.google.com/forms/d/1OvEsdBioOFcXFAiscO34kctUWKs3dWQs5-ZouXdwy9Q/viewform | logs: http://codu.org/logs/_esoteric & http://tunes.org/~nef/logs/esoteric/.
02:39:39 <Bike> A description of the Unicode character set, written in the Georgian language, phonetically transcribed into mirror-reversed Devanagari script. Footnotes to the text are in Cree (phonetically transcribed in Kannada script), Occitan (transcribed in Pitman shorthand), Xhosa (transcribed into a variant of Braille normally used for Russian), Pennsylvania German (transcribed in Glagolitic script), Miqmaq hieroglyphs, an unidentified language transcr
02:40:13 <oerjan> an unidentified language transcr
02:41:30 <oerjan> i find it somewhat unlikely they could get together enough speakers to make that with any better than google translate quality
02:41:53 <oerjan> also, i doubt google translate does cree.
02:47:48 <zzo38> Bike: How are they going to do that?
02:48:10 <Bike> who's they
02:49:06 <zzo38> I don't know; I hoped you know.
02:50:05 <oerjan> Bike: when i say say "an unidentified language transcr" it's suppose to be a hint to you that your message got cut off, hth
02:50:14 <oerjan> *supposed
02:51:24 <Bike> I didn't think it was important, but "ibed into vertical Manchu script, and several unidentified scripts."
02:54:41 <oerjan> WELL HOW CAN WE KNOW IT'S UNIMPORTANT IF YOU DON'T PASTE IT HTH
02:55:23 <Bike> You can't, but I can.
02:55:49 <zzo38> Or, at least, you can believe it to be unimportant to you.
02:56:27 <oerjan> THIS IS A FLAGRANT VIOLATION OF MY CONSTITUENT RIGHTS HTH
02:57:02 <Gracenotes> taking away your natural rights k
02:57:59 <doesthiswork> Gracenotes: that's just not right
02:58:51 <Gracenotes> help Amazon is recommending Hello Kitty things to me
02:59:10 <Gracenotes> and also College Living Essentials
02:59:33 <oerjan> are there Hello Kitty College Living Essentials
03:00:38 <Gracenotes> probably twin XL bedsheets
03:04:40 <doesthiswork> Gracenotes: Are you in college?
03:05:19 <zzo38> Do you know about Z-machine? The new version of my Z-machine assembler is now released.
03:06:14 <zzo38> Although I want to make up a SSA intermediate language for use with Z-machine, and some Haskell library for making Z-machine files.
03:29:56 -!- JesseH has joined.
03:32:15 <doesthiswork> if you add reflection does it become an S-machine?
03:34:32 * oerjan swats doesthiswork -----###
03:35:19 <zzo38> doesthiswork: I have never heard of such a thing.
03:38:17 <doesthiswork> zzo38: it was just a bad joke. When you look at Z in the mirror it looks like S
03:42:46 <oerjan> doesthiswork has this special curve-smoothing mirror
03:43:56 <kmc> rip hexagons
03:44:03 <kmc> hexagonal wang tiles would be cool tho
03:44:14 <kmc> <Sgeo> I am addicted to Listerine PocketPak strips
03:49:33 <Gracenotes> doesthiswork: nop
03:50:26 <doesthiswork> are you a girl from 13 to 48?
03:51:27 <doesthiswork> if not then I don't know why it suggests hello kitty college things.
03:51:51 <Gracenotes> because I was looking at tea spoons
03:52:08 <Gracenotes> did you know there are Hello Kitty spoon sets?
03:52:35 <Bike> are they good?
03:53:01 <Gracenotes> maybe, check the reviews.
03:53:04 <doesthiswork> yes I did, there are hello kitty every thing. Sanrio milks their cash cow for all she's worth
03:53:15 <Gracenotes> cash kitten
03:53:25 <Gracenotes> everyone loves cat milk.
03:56:46 -!- mnoqy has quit (Quit: hello).
03:56:50 <zzo38> doesthiswork: It isn't quite "S".
04:03:01 -!- Bike has quit (Ping timeout: 276 seconds).
04:04:28 -!- Bike has joined.
04:08:01 <zzo38> kmc: Yes, see if you can make hexagonal wang tiles too. And other shapes.
04:11:10 <zzo38> Could ordinary wang tiles be made into just shapes (no colors) (like puzzle pieces)? Such as different shape for each color (according to the direction, too) and the shapes are made so it also won't fit if it is rotated or flipped.
04:13:08 <doesthiswork> yes
04:13:46 <oerjan> yep
04:14:08 <doesthiswork> sorry for the short answer but it takes longer to describe than to imagine
04:15:37 <oerjan> zzo38: one way is to code matchingness as having corresponding zigzag patterns on their bordering edges
04:16:32 <oerjan> you can encode 0 as /\ and 1 as __ say
04:17:08 <oerjan> and \/ for the matching one
04:18:14 <oerjan> and apart for the zigzag patterns the rest can still be squares and whatever
04:18:23 <oerjan> *from
04:22:02 <zzo38> oerjan: Yes those are the kind of things I was thinking of
04:22:46 <zzo38> Although you use a different set of patterns for each edge, such that the opposite edges will fit together though, I think.
04:24:14 <oerjan> well yes that's what i mean
04:25:14 <doesthiswork> it helps if you have asymmetrical teeth, but those are hard to show in text.
04:25:48 <zzo38> doesthiswork: Yes I thought of that too.
04:26:21 <oerjan> hm right you could do that, although i was thinking you could just fix the direction by having /\ on one end and __ on the other. oh hm __ may not be the best choice.
04:26:43 <oerjan> /\ and |^| perhaps
04:27:37 <doesthiswork> Yes, the nice thing about trinary is it has a direction
04:27:40 <oerjan> oh well that's a small detail.
04:28:29 <Jafet> Cut out the outline of "GREEN" along the edge
04:28:52 <doesthiswork> Brilliant in it's simplicity
04:29:04 <Jafet> And "TEAL" and "COSMIC LATTE" (you may need a fine craft knife for this one)
04:30:08 <oerjan> ...that _is_ brilliant :P
04:38:17 <Bike> http://25.media.tumblr.com/a81cc3de8df6eab463ac666079105112/tumblr_mqmppwmOZA1qjr3c0o4_250.jpg
04:55:14 <oerjan> thx bookmarked
05:14:49 -!- CADD has quit (Read error: Connection reset by peer).
05:14:55 -!- CADD has joined.
05:21:44 -!- nooodl__ has joined.
05:22:03 -!- nooodl_ has quit (Read error: Connection reset by peer).
05:23:13 -!- zzo38 has quit (Disconnected by services).
05:23:18 -!- zzo38 has joined.
05:27:47 <zzo38> OK
05:27:53 <zzo38> ?
05:29:35 -!- nooodl__ has quit (Read error: Connection reset by peer).
05:35:47 <doesthiswork> I want to make a board game that exercises skill at organizing things the same way you have to do for a program.
05:36:14 <zzo38> How would such a thing be made?
05:37:22 <doesthiswork> I don't know, my best idea so far is some puzzle peices that each turn you have to use to make a structure that satisfies that rule
05:39:37 <doesthiswork> because jigsaw puzzles have the dynamic of organizing pieces
05:39:55 <doesthiswork> but I'm having trouble thinking of the right sort of rules
05:42:15 <zzo38> I don't know either.
05:48:45 <doesthiswork> but also the necessity of organizing a program is only learned when you have to keep modifying it to match the changed plans
05:49:03 <doesthiswork> so I think that would be a fun game too
05:50:16 -!- Bike has quit (Ping timeout: 276 seconds).
05:50:53 -!- Bike has joined.
05:52:29 -!- Bike_ has joined.
05:53:54 -!- oerjan has quit (Quit: ghint).
05:55:28 -!- Bike has quit (Ping timeout: 276 seconds).
06:05:05 <zzo38> Sometimes a program might be organized before it is put into the computer.
06:06:51 <Sgeo> Note to self: What I have been considering to be "Moonlight Sonata" is just the first part of Moonlight Sonata
06:17:48 <Bike_> fyi that's true of like every "classical" piece of music you know
06:17:52 -!- Bike_ has changed nick to Bike.
06:18:36 <Jafet> Anything is true of every classical piece of music you know
06:19:35 <zzo38> Classical music often has multiple parts; in what I have seen, if there are three parts, the first and third parts are with the same key but the second part may be of a different key, and often shorter, too.
06:22:12 <doesthiswork> 15 minutes is the whole thing right?
06:23:33 -!- CADD has quit (Ping timeout: 248 seconds).
06:26:45 -!- copumpkin has quit (Ping timeout: 248 seconds).
06:27:21 -!- copumpkin has joined.
06:30:32 -!- CADD has joined.
06:30:56 -!- CADD has changed nick to Guest97377.
06:31:10 -!- stuntaneous has quit (Read error: Connection reset by peer).
06:31:32 -!- stuntaneous has joined.
06:37:38 -!- Guest97377 has changed nick to CADD.
07:20:40 -!- conehead has quit (Quit: Computer has gone to sleep.).
07:34:04 -!- carado has joined.
07:34:22 <zzo38> Once somebody made up a global enchantment card (for Magic: the Gathering) called "Nirvana" with the text "Goblins cannot reach Nirvana." I made up a meaning for this card, although it would hardly ever actually do anything.
07:36:38 <zzo38> If the Magic: the Gathering cards programming language I had the idea of, would exist and would be able to treat "reach" as a verb, then if you enter it as "Goblin=s cannot reach ~" then it might be able to understand it, too.
07:47:58 -!- dessos_ has joined.
07:48:05 -!- dessos has quit (Read error: Connection reset by peer).
07:52:41 -!- epicmonkey has joined.
07:53:53 -!- douglass has quit (Ping timeout: 240 seconds).
07:58:50 -!- mnoqy has joined.
08:00:35 * Sgeo wonders what zzo38's opinion of Magic the Gathering Online is
08:11:06 -!- CADD has quit (Read error: Operation timed out).
08:19:19 -!- CADD has joined.
08:25:08 -!- Taneb has joined.
08:25:17 <Taneb> Morning!
08:26:23 -!- zzo38 has quit (Remote host closed the connection).
08:28:52 -!- epicmonkey has quit (Ping timeout: 276 seconds).
08:30:13 <fizzie> Taneb: Feeling bright and happy and sober there, I guess?
08:30:21 <Taneb> :D
08:30:25 <Taneb> Barely hung over at all
08:30:36 <fizzie> Good genes, I guess.
08:31:06 <Taneb> I think last night I assumed I'd have forgotten a lot more
08:31:29 <Taneb> So I left myself a bunch of notes
08:31:35 <Taneb> But I remember what I wrote on the notes
08:33:26 <Taneb> Also I met someone called Panda
08:45:28 -!- CADD has quit (Ping timeout: 264 seconds).
08:46:40 <kmc> Sgeo: what about the Magic: The Gathering Online eXchange
08:47:14 -!- iamfishhead1 has joined.
08:47:29 <shachaf> `relcome iamfishhead1
08:47:31 -!- carado has quit (Ping timeout: 246 seconds).
08:47:35 <HackEgo> iamfishhead1: 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 esoterica, try #esoteric on irc.dal.net.)
08:47:57 <iamfishhead1> Hi shachaf
08:48:16 <shachaf> hiamfishhead1
08:50:46 <iamfishhead1> Me. myself and I
08:51:11 <Fiora> Taneb: good meowrning?
08:51:25 <Taneb> Better than I expected
08:52:32 <Taneb> You?
08:55:57 <Fiora> I fell asleep for a nap at 7 and then suddenly it was 2
09:03:16 -!- iamfishhead1 has quit (Quit: Leaving.).
09:04:13 <Taneb> :O
09:04:48 <Taneb> I think that means you had 5 more hours of sleep than me :(
09:05:20 <Fiora> aww :<
09:15:15 -!- Frooxius has quit (Read error: Connection reset by peer).
09:15:32 -!- Frooxius has joined.
09:17:23 <kmc> glad you're feeling well Taneb :)
09:17:44 <Taneb> :)
09:18:05 <shachaf> hi kmc
09:18:09 <kmc> hi shachaf
09:18:20 <Taneb> I hope my friends are all okay
09:21:27 * kmc → sleep
09:23:32 <Fiora> goodnight!
09:23:51 <Fiora> wow, apparently one of the categories for the UK censorship thing is "esoteric material" they're onto us ;_;
09:24:36 <shachaf> as long as hexham doesn't start censoring things too
09:26:28 -!- Frooxius_ has joined.
09:29:19 -!- Frooxius has quit (Ping timeout: 276 seconds).
09:29:24 <Taneb> Goodnight, kmc
09:30:19 -!- Frooxius_ has quit (Client Quit).
09:41:05 -!- sebbu2 has joined.
09:44:44 -!- sebbu has quit (Ping timeout: 260 seconds).
09:52:36 -!- MindlessDrone has joined.
10:07:13 -!- sacje has joined.
10:42:59 -!- epicmonkey has joined.
10:45:57 -!- doesthiswork has quit (Ping timeout: 248 seconds).
10:49:02 -!- carado has joined.
11:14:08 <Vorpal> fizzie, clang-analyzer actually found a bug, if you used a mode less than zero or larger than 5 (invalid values) to FILE O it would access uninitialized memory when trying to clean up the already allocated file handle. Heh
11:14:59 <Vorpal> fizzie, In total it found 11 items, one of them has a path length of 33 and is inside the genx library. Trying to figure out what is going on there now.
11:17:41 -!- carado has quit (Ping timeout: 246 seconds).
11:19:25 -!- carado has joined.
11:31:04 -!- carado_ has joined.
11:32:01 -!- carado has quit (Ping timeout: 246 seconds).
11:34:58 <Deewiant> The analyzer always gives me a dozen "uninitialized argument value" errors that I don't care about :-/
11:52:24 <elliott> Fiora: did you see this quote about the "on-by-default" filters I pasted in here a few days ago?
11:52:27 <elliott> "They have negotiated with the government and agreed on a system called "Active Choice +" in which customers opt in for filters [...] The leaked letter [...] suggests: "Without changing what you will be offering (ie active-choice +), the prime minister would like to be able to refer to your solutions [as] 'default-on'"."
11:52:39 <elliott> pretty great
12:12:51 -!- epicmonkey has quit (Read error: Operation timed out).
12:14:43 <Vorpal> Deewiant, hm, not much of that for me. I have two false positives in the funge space write-to-file-in-text-mode code, where the analyzer appears to simply fail at basic arithmetics.
12:16:14 <Vorpal> Deewiant, and I have one real bug (but that doesn't affect me) in the getline-code I took from gnulib or glibc or some such, where it can leak memory if a realloc to grow a buffer fails. But that doesn't affect me since I always provide an already allocated buffer I believe
12:16:45 <Deewiant> You can add an assert to make the analyzer shut up about stuff like that
12:16:58 <Vorpal> Deewiant, tried, but no luck currently
12:17:10 <Vorpal> #ifdef __clang_analyzer__
12:17:10 <Vorpal> 1065assert(offset->x < maxx);
12:17:10 <Vorpal> 1066assert(lastspace == maxx - offset->x);
12:17:10 <Vorpal> 1067#endif
12:17:10 <Vorpal> 1068for (funge_cell x = offset->x; x < maxx; x++) {
12:17:11 <Vorpal> ...
12:17:17 <Vorpal> Even with that it doesn't see that loop as taken
12:17:20 <Vorpal> I have no idea why
12:17:36 <Deewiant> I meant for the realloc thing
12:17:43 <Vorpal> Deewiant, oh that, right, possibly
12:18:23 <Deewiant> Why #ifdef them out?
12:19:16 <Deewiant> According to http://clang-analyzer.llvm.org/faq.html#use_assert that first assert should work for that but oh well
12:19:19 <Vorpal> Deewiant, because those asserts are inside a loop, and since they were loop invariant I first put them outside the outermost loop, but since that didn't help I tried putting them inside instead
12:19:22 <Vorpal> Not working either
12:19:38 <Vorpal> and yes I agree, the first one should work
12:19:40 <Vorpal> but doesn't
12:20:21 <Deewiant> What does it matter if they're inside a loop, do you leave asserts in release builds or something
12:20:48 <Vorpal> Deewiant, In RelWithDebInfo builds, but not in full Release no
12:20:55 <Vorpal> anyway they didn't work for the analyzer anyway
12:21:10 <Vorpal> So meh, giving up on trying to tell it about the false positives
12:21:26 <Vorpal> I fixed all the real issues anyway, don't really care about there being 3 false positives in the code.
12:22:40 <Vorpal> Deewiant, where did you get those uninit arg value errors from btw?
12:23:04 <Vorpal> I mean, some sort of example code or such
12:23:04 <Deewiant> In mushspace
12:23:15 <Deewiant> They're not false positives, I just don't care about them
12:23:22 <Deewiant> Example code: int x; f(x); :-P
12:23:30 <Deewiant> And then f() doesn't read x
12:23:35 <Vorpal> Well, that doesn't look well defined to me, unless f is a macro
12:23:55 <Deewiant> AFAICT it shouldn't matter as long as f doesn't read it
12:24:12 <Vorpal> Deewiant, pretty sure it isn't well defined to call with an uninitialized l-value, since the calling convention would end up reading it and putting it in a register or such
12:24:18 <Vorpal> you could pass a pointer to x though
12:24:44 <Vorpal> Deewiant, I'm not 100% certain though
12:24:58 <Deewiant> It's possible, I haven't found anything specific in the standard though
12:25:03 <Vorpal> Hm
12:25:17 <elliott> oh geez
12:25:22 <elliott> I just realised what I should write shiro 2 in!
12:25:23 <elliott> rust
12:25:23 <Vorpal> Deewiant, anyway why pass the argument if f doesn't need it anyway?
12:25:31 <elliott> that way i can beat Deewiant and still be a hipster
12:25:37 <Vorpal> elliott, how far did you get with shiro 1 anyway?
12:26:09 <Deewiant> Vorpal: Basically to simplify the code since it needs it sometimes
12:26:15 <elliott> Vorpal: um, it passed pure mycology except for like one annoying file IO technicality I didn't want to fix, and implemented like 15-20 fingerprints.
12:26:23 <Vorpal> Deewiant, ah
12:26:24 <elliott> with varying degrees of Mycology-passingness, but fairly good on the whole
12:26:32 <elliott> it was missing a couple of fingerprints to run fungot iirc
12:26:32 <fungot> elliott: " fnord", ou " fnord" seems to not parse them well.
12:26:37 <Vorpal> elliott, fair enough
12:27:12 <Vorpal> elliott, what about the stuff that mycology doesn't test? Like text mode for o.
12:27:15 <elliott> Deewiant: is mushspace at the point where you don't really want to compete with it with a GC yet :p
12:27:23 <elliott> Vorpal: that was probably broken
12:27:25 <elliott> i/o are annoying
12:27:40 <Vorpal> elliott, quite so, text mode o especially
12:27:50 <Vorpal> since you need to strip trailing ws from the end of each line
12:28:07 <Deewiant> elliott: Depends on your GC? I dunno :-P
12:28:43 <Vorpal> Though I just thought of a more efficient way to do it... Except it will be even more complicated to write the code for.
12:29:59 <Vorpal> What does a GC have to do with mushspace anyway?
12:31:27 <elliott> Vorpal: well, pauses.
12:33:02 <Vorpal> hm?
12:35:02 <elliott> GCs tend to cause them.
12:35:33 <Vorpal> Well yes
12:35:49 <Vorpal> Deewiant, are you using a GC?
12:36:30 <Deewiant> OK, I think foo x; f(x) is unspecified, but if x is a partially initialized struct I think it's still fine, hmm
12:36:32 <Deewiant> Vorpal: No
12:36:49 <Vorpal> Makes sense since you said you were aiming for performance iirc
12:36:50 -!- yorick has joined.
12:37:12 <elliott> how does Vorpal understand how a GC could harm performance when talking to Deewiant but not when talking to me??????
12:39:14 <Vorpal> elliott, the initial cause was some parsing confusion on "want to compete with it with a GC". I first parsed that as him competing with it + a GC against something.
12:40:40 <elliott> uh. okay :P
12:53:43 <Vorpal> bbl
12:58:31 <fizzie> Deewiant: How do you make a partially initialized struct?
12:59:26 <fizzie> Uninitialized, and set a couple of members, I guess.
13:00:41 <Deewiant> Or initialize it with { .foo = bar }
13:00:48 <fizzie> That's not partially initialized.
13:01:00 <Deewiant> Well clang's analyzer claims it is
13:01:12 <fizzie> It's talking out of its ass, then.
13:01:15 <fizzie> "If there are fewer initializers in a brace-enclosed list than there are elements or members of an aggregate -- the remainder of the aggregate shall be initialized implicitly the same as objects that have static storage duration."
13:02:58 <Deewiant> Oh whoops, it's actually referring to a struct member of the struct, my bad
13:05:03 <fizzie> Actually, I guess the version stating almost the same thing few paragraphs up, "-- all subobjects that are not initialized explicitly shall be initialized implicitly the same as --", is more relevant.
13:05:23 <fizzie> Good thing that's there, otherwise presumably struct { int a, b; } f = { .a = 42, .a = 69 }; would leave b uninitialized.
13:13:14 <Deewiant> Actually this thing just seems to be confused
13:15:34 <fizzie> Also I concur with the foo x; f(x) being okay for a partially uninitialized struct -- "the value of struct or union object is never a trap representation, even though the value of a member of the structure or union may be a trap representation" -- and apparently so does the committee in DR222: http://std.dkuug.dk/jtc1/sc22/wg14/www/docs/dr_222.htm
13:16:33 <Deewiant> Yes, I was reading C11 which has those DR222 changes
13:42:58 -!- FreeFull has quit (Quit: Rebooting).
13:57:39 -!- FreeFull has joined.
14:27:04 -!- pikhq_ has joined.
14:27:32 -!- pikhq has quit (Ping timeout: 260 seconds).
14:50:52 -!- nooodl has joined.
14:58:11 -!- copumpkin has quit (Quit: Computer has gone to sleep.).
15:01:11 <Vorpal> what exactly is a trap representation?
15:01:48 <Deewiant> Vorpal: "an object representation that need not represent a value of the object type"
15:04:26 <Vorpal> Ah right
15:04:40 <Vorpal> Deewiant, would null be considered one of those?
15:04:47 <Fiora> I think null is sort of a trap representation?
15:04:55 <Fiora> I wonder if NaN counts too.
15:05:17 <Deewiant> No, null is a valid value that a pointer can have, and likewise NaN for floats
15:05:32 <Vorpal> Deewiant, So on common systems there are no trap representations?
15:05:43 <Deewiant> Certain object representations need not represent a value of the object type. If the stored value of an object has such a representation and is read by an lvalue expression that does not have character type, the behavior is undefined. If such a representation is produced by a side effect that modifies all or any part of the object by an lvalue expression that does not have character type, the behavior is
15:05:45 <Deewiant> undefined. Such a representation is called a trap representation.
15:06:11 <Deewiant> Vorpal: Not on x86 afaik
15:06:14 -!- aloril_ has quit (Ping timeout: 246 seconds).
15:06:36 <Deewiant> Vorpal: You can set the FPU to trap on some stuff but I wouldn't consider that part of this
15:07:33 <Vorpal> So what platforms do have it hm?
15:07:59 <Fiora> http://stackoverflow.com/questions/6725809/trap-representation oh, huh, this sems to explain some of it (?)
15:08:52 <elliott> that's nasty
15:08:54 <elliott> fake values
15:09:37 <Fiora> I guess one example might be "negative 0" in a ones' complement number format?
15:09:48 <Fiora> I'm not sure
15:10:45 <elliott> yeah the SO answer gives that as an example
15:10:49 <elliott> or, oh, the standard does
15:11:06 <Deewiant> Evidently signalling NaNs remain undefined in C11 so those count
15:13:26 <Deewiant> "Some combinations of padding bits might generate trap representations, for example, if one padding bit is a parity bit. Regardless, no arithmetic operation on valid values can generate a trap representation other than as part of an exceptional condition such as an overflow, and this cannot occur with unsigned types."
15:13:53 <Vorpal> hm
15:18:31 <Deewiant> "An integer may be converted to any pointer type. Except as previously specified, the result is implementation-defined, might not be correctly aligned, might not point to an entity of the referenced type, and might be a trap representation."
15:20:06 -!- aloril_ has joined.
15:54:18 -!- mnoqy has quit (Quit: hello).
15:55:18 -!- doesthiswork has joined.
15:55:52 <doesthiswork> good morning
16:03:11 -!- doesthiswork has quit (Remote host closed the connection).
16:09:28 -!- doesthiswork has joined.
16:09:43 -!- Lumpio- has quit (Ping timeout: 245 seconds).
16:09:44 -!- doesthiswork has quit (Client Quit).
16:10:06 -!- doesthiswork has joined.
16:13:35 -!- Lumpio- has joined.
16:23:02 -!- Taneb has quit (Ping timeout: 240 seconds).
16:28:41 -!- Taneb has joined.
16:35:15 -!- atriq has joined.
16:36:14 -!- Taneb has quit (Ping timeout: 240 seconds).
16:40:42 -!- Frooxius has joined.
16:44:47 <doesthiswork> good morning
16:52:57 -!- atriq has changed nick to Taneb.
17:06:03 -!- Phantom_Hoover has joined.
17:08:31 -!- zzo38 has joined.
17:34:30 -!- conehead has joined.
17:34:50 -!- doesthiswork has quit (Max SendQ exceeded).
17:35:10 -!- conehead has quit (Remote host closed the connection).
17:35:30 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds).
17:35:36 -!- conehead has joined.
17:49:15 -!- doesthiswork has joined.
18:08:59 <tswett> Hm. They make a distinction between undefined behavior and unspecified behavior.
18:09:20 <Fiora> I think "unspecified" means "something predictable happens, but it could be platform-dependent"?
18:09:26 <tswett> So undefined behavior means "the implementation is allowed to do literally anything when this happens".
18:09:33 <Fiora> while undefined means "this should never happen, code is wrong if it does this, demons could shoot out your nose"?
18:09:44 <Fiora> so the latter is "the compiler can assume this doesn't happen"?
18:09:58 <tswett> And unspecified behavior means "the implementation has some leeway in choosing what the result is when this happens".
18:10:05 <Fiora> yeah...
18:10:07 <Fiora> that sounds right.
18:13:23 <Deewiant> There's undefined behaviour, unspecified behaviour, and implementation-defined behaviour
18:13:46 <elliott> what's the difference between unspecified and implementation-defined?
18:14:28 <Deewiant> Undefined = anything can happen; unspecified = there are many specified alternatives but which one happens at any given time can vary
18:15:36 <Deewiant> "use of an unspecified value, or other behavior where this International Standard provides two or more possibilities and imposes no further requirements on which is chosen in any instance"
18:16:07 <Deewiant> (unspecified value = "valid value of the relevant type where this International Standard imposes no requirements on which value is chosen in any instance")
18:16:21 <Deewiant> (implementation-defined value = "unspecified value where each implementation documents how the choice is made")
18:17:10 <tswett> So, my lazy expression reducer is pretty inefficient, I guess.
18:17:16 <elliott> I see
18:17:28 <elliott> so implementation-defined = unspecified but it has to be consistent within an implementation?
18:17:43 <tswett> In that it can potentially traverse the entire expression every time a reduction step is performed.
18:17:53 <Bike> unspecified by the standard, specified by the implementation
18:18:23 <Deewiant> elliott: Depends on what you mean by consistent, I guess; it has to be documented
18:18:32 <Bike> probably hard to enforce though :p
18:18:41 <Deewiant> So it could still be e.g. selection by /dev/random
18:18:53 <elliott> Deewiant: okay so it is just a documentation requirement and nothing more
18:19:12 <Deewiant> "unspecified behavior where each implementation documents how the choice is made"
18:19:20 <elliott> right
18:19:38 <tswett> The intelligent way to do this would probably be to mark each sub-expression as to whether it's already been evaluated or not.
18:19:42 <Deewiant> It's possible that there are further consistency requirements for specific things, I guess
18:19:44 <Bike> http://www.jwz.org/images/gm.gif cow
18:21:18 <tswett> That sure is a lot of agitation.
18:22:04 <tswett> If that cow were real, would it really slosh that much?
18:22:36 <tswett> I'm trying to figure out whether they did a good job with subsurface scattering or not.
18:23:41 <ion> Perfect cube tutorial http://i.imgur.com/fctEUfv.gif
18:29:02 <ion> http://www.kickstarter.com/projects/2010618696/dkss-reality-death-maze
18:30:52 <elliott> someone pledged over $1,000 on that.
18:34:13 <Bike> Could be the people funding their own kickstarter to make it look like it's supporte.
18:34:29 <doesthiswork> luckily they get their money back
18:35:00 <ion> Well, most of it.
18:35:28 <Bike> "Help us support the Portal! Please fund DKS's Reality Death Maze to help us open our dimensional portal." er
18:36:05 <Deewiant> Only most of it?
18:56:19 <FreeFull> ion: I prefer twisted cubes
19:02:59 -!- MindlessDrone has quit (Quit: MindlessDrone).
19:04:02 <Taneb> Are all beginnings non-sequiturs?
19:04:44 <olsner> sounds like a question for fungot
19:04:44 <fungot> olsner: well there. fight about whether to play keen or watch demos. he didn't tell anything ( they don't)
19:16:15 <tswett> Having written a basic proto-Hylisk interpreter, suddenly I have no desire to use it.
19:16:30 <Sgeo> Oh hey Edward Kmett reads HPMOR
19:29:31 <Taneb> Harry Potter: Man on Rhea?
19:32:15 <Sgeo> Harry Potter and the Methods of Rationality
19:32:18 <doesthiswork> I'm not such a fan of that story
19:34:10 <doesthiswork> because among other things genetics is a lot more interesting than presented there
19:35:50 -!- carado has joined.
19:35:53 -!- carado has quit (Read error: Connection reset by peer).
19:36:24 -!- carado has joined.
19:38:43 -!- carado_ has quit (Read error: Connection reset by peer).
19:43:04 -!- carado has quit (Ping timeout: 246 seconds).
20:17:30 -!- Bike has quit (Ping timeout: 264 seconds).
20:20:00 -!- ssue__ has quit (Ping timeout: 245 seconds).
20:20:35 -!- Guest18414 has quit (Ping timeout: 264 seconds).
20:20:53 -!- Guest18414 has joined.
20:25:37 -!- Bike has joined.
20:38:51 <Taneb> Tracking the #haskell tag on Tumblr may not have been the best idea
20:38:59 <Taneb> It's one of the most multi-purpose tags there is
20:39:22 <Taneb> And half of the stuff that is the programming language is just links to things I've already seen
20:40:09 <fizzie> Well. The UI is real clunky, the code may be buggy, half of the features are missing and the compositing is all wrong, but here it is anyway: http://zem.fi/ircvis/esoteric/people_presence.html
20:40:11 -!- Sgeo has quit (Read error: Connection reset by peer).
20:41:25 -!- Sgeo has joined.
20:41:37 <doesthiswork> interesting
20:41:56 <Taneb> kallisti's is unusual
20:42:12 <doesthiswork> it does show different things than the weekly and hourly graphs did
20:43:40 <doesthiswork> lambdabot doesn't have much of an hourly schedule either.
20:47:54 <doesthiswork> We can calculate the mutual information between two nicks to see how similar their sleep schedules are
20:48:46 -!- tertu has joined.
20:49:33 <doesthiswork> although kullback-divergance might be more fitting
20:49:47 <elliott> fizzie: it seems I lost my sleep schedule in 2009.
20:50:25 <ion> FWIW, i also like git more. https://twitter.com/molovo/status/360346792602259456
20:51:01 -!- epicmonkey has joined.
20:51:20 <fizzie> I don't know offhand how to make SVG's simple alpha compositing do the operation I wanted, which was to blend colors with uniform weights where they overlap. The current scheme of setting layer opacities to 1, 1/2, 1/3, ... from bottom to top does the right thing if there's a pixel in all layers, but it dims the non-bottom layers where they composit with the black background. Filter effects ...
20:51:26 <fizzie> ... could probably do it, though.
20:53:23 <doesthiswork> kmc gained a sleep schedule mid 2012
20:54:04 <Taneb> I think I remember that!
20:54:57 <elliott> MKRY on the list of nicks. :/
20:54:59 <doesthiswork> taneb suddenly sprang into being in 2011
20:55:29 <Taneb> Yup
20:55:49 <Taneb> Actually, I've used the name "Taneb" since at least October 2007
20:55:51 <ion> Sleep schedule? What’s that?
20:56:04 <Taneb> I think I first used it July 2007
20:56:18 <doesthiswork> I suspect you are an irc bot ion
20:56:39 <ion> What makes you think you are an irc bot ion?
20:57:29 <olsner> I seem to do a lot of breakfast irc between about 9 and 11
20:58:10 <fizzie> Note that there's a curious singular Taneb dot somewhere in September 2010.
20:58:23 <elliott> that one is good iirc
20:58:25 <elliott> if you pastelogs it
20:59:18 <Taneb> The weird thing is, I remember doing that, but I remember doing that in 2011
20:59:57 <ion> I can’t place p. much anything to a specific year, my sense of time is horrible.
21:01:17 <fizzie> http://codu.org/logs/log/_esoteric/2010-09-06#204051Taneb it seems that when Taneb appeared in 2010, I was... doing plots.
21:01:57 <Taneb> It definitely sounds like me
21:02:22 <doesthiswork> and then you didn't come back for a year?
21:02:52 <Taneb> Apparently!
21:03:01 <Taneb> Maybe it was a time-traveller impersonating me
21:03:06 <Taneb> But for what purpose?
21:03:17 <Taneb> Obviously, to save the space-time continuum!
21:03:20 <olsner> fizzie: is Taneb and atriq merged in that graph?
21:04:14 <Taneb> olsner, I believe they are
21:04:17 <Taneb> Ngevd, too
21:04:27 <olsner> are you ngevd too?
21:05:02 <Taneb> Yes
21:05:08 <Taneb> `rot13 atriq
21:05:12 <HackEgo> ngevd
21:05:34 <olsner> oh, I thought taneb was rot13 of atriq for some reason
21:05:42 <Taneb> My initials were ALMOST N. G. E. v. D
21:05:59 <Taneb> But my parents thought that was too long and dropped the E (which stood for Eliot)
21:06:01 <fizzie> olsner: Yes.
21:06:20 <fizzie> olsner: 'Taneb': ['Taneb', 'Ngevd', 'atriq'],
21:06:42 <Taneb> Shouldn't CakeProphet and kallisti be merged? Or am I misremembering?
21:08:01 <fizzie> Taneb: I think that was a merging I was supposed to do but couldn't be bothered rerunning the statistics-collection system on the entire logs. (Don't have a merging tool for them.)
21:08:39 <fizzie> I'll get it next time.
21:09:09 <Taneb> :)
21:09:18 <Taneb> Huh, I've been active in the channel for about as long as shachaf
21:12:09 <fizzie> And your schedules are pretty much complementary. Are you... are you shachaf?
21:12:33 <Taneb> What a twist!
21:12:54 <Taneb> And I read Homestuck and won't read OotS and he reads OotS and won't read Homestuck!
21:13:42 <fizzie> When comparing two things, thanks to the crummy blending, setting the first to red and the second (dimmed one) to turquoise seems to be a reasonably good pair. (I'll fix it properly at some point.)
21:15:04 <fizzie> (Though sadly the layers aren't always in the order specified.)
21:17:37 <shachaf> I can confirm that I am Taneb.
21:17:43 <Taneb> Totally called it
21:18:18 <Taneb> More evidence that shachaf and I are one and the same:
21:18:23 <Taneb> shachaf is not a rabbi
21:18:26 <Taneb> As far as I am aware
21:18:33 <Taneb> shachaf, are you a rabbi?
21:18:45 <shachaf> Have we ever been seen in the same IRC channel together?
21:18:57 <Taneb> I don't think so
21:18:58 <shachaf> Taneb: Nope.
21:19:04 <Taneb> Neither am I!
21:19:06 <Taneb> `? Taneb
21:19:08 <HackEgo> Taneb is not elliott, no matter who you ask. He also isn't a rabbi although he has pretended in the past. He has at least two backup keyboards. (see also: d-modules)
21:19:25 <olsner> `? d-modules
21:19:27 <HackEgo> D-modules are just modules over the ring of differential operators. Taneb invented them.
21:19:36 -!- CADD has joined.
21:19:52 <Taneb> `? modules
21:19:53 <HackEgo> modules? ¯\(°_o)/¯
21:19:54 <myndzi> |
21:19:54 <myndzi> o/`¯º
21:19:57 <Taneb> `? ring
21:19:59 <HackEgo> Addition, subtraction and multiplication have a certain ring to them.
21:20:07 <Taneb> `? differential operators
21:20:09 <HackEgo> differential operators? ¯\(°_o)/¯
21:20:10 <myndzi> |
21:20:10 <myndzi> º¯`\o
21:20:43 <shachaf> imo checkmate
21:30:04 -!- epicmonkey has quit (Read error: Operation timed out).
21:58:59 -!- Taneb has quit (Quit: Leaving).
22:02:05 * tswett ponders what a ~list is.
22:02:13 <tswett> I.e., what's the comonad corresponding to the list monad?
22:03:17 <tswett> Looks like it's... something that consumes an arbitrary number of items and then exits.
22:03:55 <elliott> it's not a comonad in Hask
22:04:01 <elliott> like shachaf said some days ago
22:04:09 -!- upgrayeddd has quit (Ping timeout: 246 seconds).
22:04:25 <elliott> the comonad you get is in the "other category" of the adjunction that gives you a monad
22:04:42 <tswett> Right, it's that other category.
22:04:43 <elliott> State/Store is just a "happy coincidence" because the two functors involved are endofunctors on Hask
22:05:02 <elliott> the comonad is in Mon
22:05:05 <elliott> IIRC extract is fold
22:05:11 <elliott> I forget what duplicate is but I recall it's boring
22:05:47 <tswett> Mon must be one of those... closed symmetric what-have-yous.
22:06:24 <tswett> Closed symmetric monoidal categories.
22:06:40 <elliott> Mon has monoid homomorphisms as morphisms
22:06:46 <elliott> and monoids as objects
22:08:18 <tswett> So a monoidal category is one with a "tensor product" bifunctor which is associative with identity up to natural isomorphism.
22:08:52 <tswett> And it seems like the "usual tensor product" is just the cartesian product or something?
22:09:18 <elliott> also in particular, a ~list is just a list.
22:09:27 <tswett> Is it now.
22:09:34 <elliott> with a monoidal element type, if you insist.
22:09:58 <tswett> So then now a closed monoidal category is one that has that currying thing.
22:10:39 <tswett> And a *symmetric* monoidal category is, uh...
22:12:58 <tswett> Apparently a braided monoidal category is one which is commutative and also satisfies some weird hexagon thing.
22:13:34 <tswett> Mm, not quite commutative?
22:15:13 <tswett> A symmetric monoidal category is one that actually is commutative?
22:16:47 <tswett> Okay whatever.
22:17:45 <tswett> Okay, so... yeah, what are the component functors of the list monad?
22:18:18 <tswett> They take Set to Mon and back to Set, aye? So, the free functor (is... is that a thing?) followed by the forgetful functor?
22:19:39 <elliott> hint: free monoid
22:19:52 <elliott> and stuff.
22:19:57 <elliott> I worked it out with shachaf once.
22:19:57 <tswett> The free monoid functor?
22:20:01 <elliott> unfortunately the comonad is boring.
22:20:21 <elliott> but I don't remember the exact details...
22:20:34 <tswett> Yeah, it looks like the comonad also pretty much makes lists, doesn't it?
22:20:57 <tswett> A co-list of monoidal things is pretty much just a list of monoidal things.
22:22:40 <tswett> "Extract" just multiplies all the elements together. And "extend", that's the w a -> w (w a) thing, right?
22:22:49 -!- copumpkin has joined.
22:23:01 -!- copumpkin has quit (Client Quit).
22:23:06 <elliott> yeah
22:24:02 <tswett> Oh, what's a monoid. How about the monoid of... things you can do with a pile of string.
22:24:04 <tswett> That's a lovely monoid.
22:24:33 -!- copumpkin has joined.
22:24:42 <tswett> So then a Colist StringThing is a list of things you can do with a pile of string. "extract"ing that concatenates all those things together.
22:24:51 <tswett> I guess the things you can do with a pile of string actually form a category, not a monoid.
22:26:54 <tswett> And "extend", what's that supposed to do?
22:28:44 <tswett> Anyway, so far, this seems completely unrelated to the linear logic dual of List I've come up with.
22:29:00 <tswett> Which is: ~List a = Bottom & (a -o ~List a)
22:31:30 -!- oerjan has joined.
22:32:19 <tswett> Hum. In a closed monoidal category, must there exist a bifunctor & such that there's a natural transformation from A & B to A, and from A & B to B?
22:33:37 <tswett> Rather, in a symmetric monoidal category, must there be such and such?
22:35:42 <tswett> Rather, a closed symmetric monoidal category.
22:35:58 <tswett> And, rather, must there exist product objects?
22:43:44 <Bike> "wanted to ask u guys - Markov Chans with lotto Numbers...good idea?"
22:55:08 <tswett> Hmm. The category of quantum state spaces.
22:55:59 <tswett> Let's say this. Quantum state spaces where every state is required to be a mixture of finitely many pure states.
22:56:17 <tswett> I'm not actually communicating right now, am I; I'm just talking to myself out loud.
22:58:26 <tswett> Let's be fun and drop the mixture of finitely many whatever.
22:59:02 <tswett> Nah, let's forget about the whole thing.
23:01:49 <tswett> Oh, here's what a ~list is in linear typing. It's actually quite simple.
23:02:00 <tswett> It's an object that, given an arbitrary length, gives you a list of that length.
23:05:44 <tswett> Seems obvious in retrospect.
23:07:06 <Bike> hey tswett, what's your favorite color? Does she know?
23:07:33 <tswett> You don't seem to be giving me the context necessary to understand your questions.
23:08:44 <Bike> 64133,918181,262626,0194823,753957192719394739109375728,281917466
23:09:33 <tswett> Oh, okay.
23:09:46 <tswett> The answer is A.
23:11:24 <Bike> That's not a color.
23:13:01 <tswett> A is the answer to the greater surrounding question.
23:16:32 <tswett> Though it's not meant to be a useful answer. It's more like a proof that all of the prerequisites for answering the greater surrounding question have been satisfied.
23:34:38 <oerjan> tswett: are you deep thought
23:43:12 <tswett> oerjan: A
23:45:01 <Sgeo> What candies exist that are as deliciously minty as Listerine strips?
23:48:44 <shachaf> mint candy flavor = the worst hth
23:53:40 -!- yorick has quit (Ping timeout: 256 seconds).
23:54:07 <Sgeo> Listerine strips taste so good
←2013-07-27 2013-07-28 2013-07-29→ ↑2013 ↑all