←2016-02-02 2016-02-03 2016-02-04→ ↑2016 ↑all
00:06:53 -!- tromp_ has quit (Remote host closed the connection).
00:29:30 <tswett> You know, when I put dates in filenames, for the most part I don't even consider using a format besides YYYYMMDD.
00:30:06 <tswett> So, I'm implementing everything in Coq!
00:30:10 <int-e> @google "interference system"
00:30:11 <lambdabot> https://en.wikipedia.org/wiki/RNA_interference
00:30:12 <tswett> And by "everything", I mean "a lot of things".
00:30:31 <tswett> But sort of everything.
00:30:37 <tswett> I'm gonna be doing a lot of category theory.
00:30:39 <mad> tswett : I've always liked DDMMYYYY but that's only because of my L1
00:30:56 <tswett> What's an L1?
00:30:59 <mad> I admit YYYYMMDD is more logical
00:31:03 <mad> native language
00:31:30 <mad> L2 is "the language you're learning in your language class" more or less
00:31:32 <tswett> I think DD-MM-YYYY is okay. DDMMYYYY is (with all due respect, sir or madam) horrible.
00:31:49 <fizzie> I think I'm YYYYMMDD 90% of the time, and YYYY-MM-DD the rest.
00:32:02 <tswett> And L3 is "the language you've learned about ten words of thanks to an iPhone app", right?
00:32:22 <mad> aka japanese? :D
00:32:30 <tswett> How did you know? :D
00:32:49 <mad> it's the language _everyone_ learns about ten words of :D
00:32:55 <tswett> So, I think I'm going to be implementing the concept of "a theory".
00:33:07 <tswett> I probably know at least 50 Japanese words. Lemme list off a few.
00:34:06 -!- tromp_ has joined.
00:35:07 <int-e> well... do igo terms count?
00:35:15 <tswett> no, neko, uma, inu, doa, wa, ga, desu, watashi, boku, imasu, ao, shiro, kuro, murasaki, kuruma, baka, hagane, mizu, oto, nonde, ringo, tamago
00:35:24 <tswett> int-e: do you know what they actually mean in Japanese?
00:35:51 <int-e> for most of them, no.
00:36:03 <tswett> They don't count in that case.
00:36:15 <mad> what does murasaki mean?
00:36:42 <tswett> Purple.
00:37:08 <lifthrasiir> tswett: DD-MM-YYYY is *not* okay, you cannot distinguish DD-MM from MM-DD. MMM-DD-YYYY or DD-MMM-YYYY are fine.
00:37:13 <int-e> tswett: no (domo) arigato? or the one that everyone knows, hai...
00:37:17 <lifthrasiir> (MMM for three-letter month abbreviations)
00:37:26 <tswett> int-e: I know a lot more words than I just listed.
00:37:47 <tswett> I guess a theory is just a special case of a presentation.
00:37:56 <int-e> Oh well, I only recognize the cat.
00:37:59 <mad> the 100-odd japanese words I know (+kanakana for gleaning the meaning of a tiny bit of japanese text) is like my L6
00:38:06 <hppavilion[1]> I am here
00:38:13 <hppavilion[1]> You may commence interesting conversation
00:38:16 <hppavilion[1]> :P
00:38:21 <lifthrasiir> is L6 a language that is somehow computerized? :p
00:38:26 <tswett> Lemme give the meanings of all those words. (Sometimes the "meanings as taught to English speakers".)
00:38:36 <hppavilion[1]> tswett: No thank you xD
00:38:45 <tswett> hppavilion[1]: this is not optional.
00:38:47 <hppavilion[1]> (unless someone else requests them)
00:38:49 <hppavilion[1]> Damn
00:39:01 <hppavilion[1]> tswett: Do I need it to graduate?
00:39:17 <tswett> Untranslatable, cat, horse, dog, Western-style door, untranslatable, untranslatable, is, I, I, is doing, blue, white, black, purple, car, stupid, steel, water, sound, drink, apple, egg
00:39:18 <tswett> hppavilion[1]: nope.
00:39:22 <mad> Tbh I could only have a conversation in like L3... past that it's just way too fragmental
00:39:39 <tswett> ("Wow", someone thinks, "Japanese sure has a lot of words for 'untranslatable'.")
00:39:54 <int-e> Hmm, an L3 cache...
00:39:57 <hppavilion[1]> tswett: No word is untranslatable to a Chomsky-complete language
00:40:23 <int-e> we can put languages in a box
00:40:39 <hppavilion[1]> (Chomsky completeness: Sufficiently overcomplicated such that you can express anything it, technically)
00:40:42 <mad> no you could translate with 'of'
00:40:43 <mad> no?
00:41:01 <mad> or 's
00:41:27 <tswett> Yeah, more or less.
00:41:29 <mad> I've seen 'wa' translated as 'as for'
00:41:44 <tswett> Yup.
00:42:11 <tswett> "Ga" can be translated as "is the one", though that's pretty dang inadequate.
00:42:27 <tswett> "Jerry wa mizu o nonde imasu." "As for Jerry, he's drinking water."
00:42:36 <tswett> "Jerry ga mizu o nonde imasu." "Jerry is the one who's drinking water."
00:42:46 <tswett> Or "it's Jerry who's drinking water" or whatever.
00:43:06 <tswett> The first one would probably just be translated as "Jerry is drinking water", really.
00:44:28 <tswett> I guess next I'll implement free monoids.
00:44:56 <mad> L3 cache... once you have that you have a really complex cpu :D
00:45:21 <lifthrasiir> tswett: they are (especially for verbs) non-standard forms, aren't they? for example nonde "drink" has a standard form of nomu.
00:46:27 <tswett> lifthrasiir: yeah, but I don't know those.
00:46:36 <tswett> I just know the -te forms.
00:46:40 <lifthrasiir> aha.
00:47:22 <lifthrasiir> kind of confusing thing for agglutinative languages
00:47:39 <mad> lifthrasiir : what is?
00:47:51 -!- Trioxin has quit (Read error: Connection reset by peer).
00:48:25 <lifthrasiir> mad: affixes can be freely attached to the word stem?
00:48:28 -!- XorSwap has quit (Quit: Leaving).
00:49:00 <mad> lifthrasiir : I thought it was more like "affixes are regular (instead of irregular like in fusional languages)"
00:49:50 <lifthrasiir> hmm, I didn't know about the clear distinction between agglutinative and fusional languages
00:50:21 <lifthrasiir> (was about to point out the distinction between agglutinative and inflectional languages, but then the realization came to me)
00:50:34 <mad> fusional is another term for inflectional
00:50:50 <lifthrasiir> hmm
00:50:52 <mad> unless I'm mistaken
00:51:01 -!- __Beavis__ has quit (Quit: Leaving.).
00:51:57 <lifthrasiir> AFAIK the distinction between agglutinative (ah fuck, I cannot easily remember this word) and inflectional languages is the "freely" part, i.e. the inflection to the word stem is not as simple and orthogonal as affixes
00:52:40 <mad> that's what I said :D
00:52:48 <mad> inflection is more irregular
00:56:03 <mad> agglutinative affixes still get phonetically adapted (vowel harmony, change depending on if the stem ends in a vowel or consonant, change depending on voicedness, etc) but generally not replaced entirely (which would more or less make it inflectional)
00:57:25 <lifthrasiir> yeah, can be regarded as a more common variations between consecutive words/morphemes
00:57:33 <lifthrasiir> s/ a / /
00:58:14 <mad> inflectional mostly stands out because it's in the most well known languages (european)
01:04:54 * oerjan note that tswett's list of japanese words looks pretty much disjoint from the set he'd consider "everyone" likely to pick up. in fact he only remembers "watashi".
01:05:08 <oerjan> oh wait, the cat yeah
01:06:58 <HackEgo> [wiki] [[HQ9+]] https://esolangs.org/w/index.php?diff=46349&oldid=37183 * Erinius * (+42)
01:08:13 <oerjan> also, the "untranslatable" reminds me of yudkowski's three worlds collide story.
01:13:01 <tswett> I read that, but I don't really remember how "untranslatable" featured in it.
01:13:12 <oerjan> in the speak of the superhappy people
01:13:15 <mauris__> i probably know at least 50 japanese words too: i can count to 50 in japanese
01:13:15 <oerjan> *speech
01:13:36 <oerjan> untranslatable-N for N from 1-4 or thereabouts
01:14:26 <oerjan> one of which seemed to denote the thing they did instead of _both_ sex and speech.
01:14:35 -!- tromp_ has quit (Remote host closed the connection).
01:14:40 <oerjan> (or rather, as both)
01:16:24 <oerjan> (both, to them, involved exchanging actual genetic material, because they had no genetic/neural information distinction)
01:16:47 <tswett> I'm pretty sure the word for that is "intercourse".
01:16:57 <oerjan> ...
01:20:43 <oerjan> and possibly as a result of this, they were incapable of lying.
01:22:07 <hppavilion[1]> Would it be possible to make an interpreter for a language that runs on bare metal such that that language can be used for OS development?
01:22:32 <oerjan> hppavilion[1]: forth is thataway, i think
01:23:06 <hppavilion[1]> oerjan: Ah, yes. Forth.
01:23:12 <oerjan> that's almost it's original purpose
01:23:36 <tswett> Don't forget the Lisp machines.
01:23:47 <oerjan> hm
01:23:58 -!- Phantom__Hoover has quit (Read error: Connection reset by peer).
01:26:09 <hppavilion[1]> oerjan: I'm kind of tempted to learn Rust, figure out how to cross-compile rust for OS dev, etc. JUST so I can get a bare-metal interpreter for that language I mentioned earlier working
01:28:17 <oerjan> okay
01:28:51 <hppavilion[1]> oerjan: The purpose of which would be... something, I'm sure
01:32:02 -!- mihow has quit (Quit: mihow).
01:45:19 <mad> I'm trying to figure out what are the "mixed relational concepts" of sapir's linguistic typology
02:02:09 -!- XorSwap has joined.
02:03:50 -!- ais523 has quit (Ping timeout: 245 seconds).
02:12:23 -!- bb010g has joined.
02:13:15 -!- mad has quit (Quit: Pics or it didn't happen).
02:15:12 -!- tromp_ has joined.
02:15:38 -!- mauris__ has quit (Ping timeout: 276 seconds).
02:20:10 -!- tromp_ has quit (Ping timeout: 276 seconds).
02:33:40 -!- Treio has quit (Quit: Leaving).
02:41:44 -!- mad has joined.
03:09:55 -!- gde33|2 has joined.
03:12:06 -!- gde33 has quit (Ping timeout: 240 seconds).
03:14:47 -!- XorSwap has quit (Quit: Leaving).
03:16:51 -!- tromp_ has joined.
03:18:04 -!- XorSwap has joined.
03:20:42 -!- ais523 has joined.
03:20:57 -!- tromp_ has quit (Ping timeout: 240 seconds).
03:21:17 <ais523> hey, you know how there's a commonly used type void/unit seen in many programming languages, which only has one value?
03:21:31 <ais523> and that it has a mathematical equivalent, normally called 1 (i.e. a 1 in bold)?
03:21:43 <ais523> what's the element of that mathematical set called?
03:22:43 <coppro> void is normally empty
03:22:57 <hppavilion[1]> ais523: unit is the one with an element
03:23:01 <mad> coppro : it's 0 bits yes
03:23:01 <shachaf> If you're talking about 1 the trivial group, I imagine people would call its element 1.
03:23:04 <shachaf> I don't know about the set.
03:23:06 <oerjan> 1 = { 0 } as von neumann numeral, so...
03:23:17 <ais523> oerjan: so the empty set
03:23:18 <coppro> the identity, the empty set, or simply the unit element, depending on context?
03:23:21 <hppavilion[1]> 1 = {{{}}}
03:23:22 <ais523> I considered that but thought it would be confusing
03:23:25 <ais523> coppro: void has one element in C
03:23:35 <hppavilion[1]> therefor 1=2
03:23:36 <ais523> Void has no elements in Haskell, though
03:23:41 <hppavilion[1]> Problem, maths?
03:23:43 <coppro> ais523: I assume you mean type theoretical stuff, where it has no elements
03:24:03 <ais523> coppro: well I'm doing type theoretical stuff, but picked a non-type-theoretical analogy
03:24:17 <coppro> I'd simply call it the unit element then
03:24:28 <coppro> because the point is that it's an arbitrary type with a single member
03:24:32 <hppavilion[1]> In my programming language I'm making
03:24:37 <coppro> it isn't necessarily going to be any one thing in particular
03:25:03 <hppavilion[1]> What should be the syntax for creating an instance of a class? e.g. a socket?
03:25:06 <coppro> since all unit types are isomorphic
03:25:14 <hppavilion[1]> The language is like Haskell
03:25:17 <mad> "identity element" for the number that produces no effect in a given operation (0 for addition, 1 for multiplication)
03:25:43 <hppavilion[1]> So it uses currying for functions- f x y z- instead of f(x, y, z) syntax
03:25:57 <ais523> coppro: the problem is I want a literal for it
03:25:59 <hppavilion[1]> mad: -1 for andation
03:26:03 <ais523> currently I'm leaning towards an empty tuple
03:26:14 <ais523> by analogy with the () that most programming languages use
03:26:22 <hppavilion[1]> ais523: Define your own syntax- e.g. 1*
03:26:36 <ais523> hppavilion[1]: this is for a mathematical paper-alike
03:26:43 <ais523> defining your own syntax tends to annoy people
03:26:55 <hppavilion[1]> ais523: Or $1- "select 1"- which selects the set of instances for a type
03:27:08 <hppavilion[1]> ais523: If there isn't a known syntax, you're allowed to define your own
03:27:17 <hppavilion[1]> That's rule 34 of math
03:27:23 <ais523> hppavilion[1]: well, in this case, I suspect there is a known syntax, but I just don't know what it is
03:27:34 <hppavilion[1]> ais523: Ah
03:27:44 <ais523> which is why I asked
03:27:47 <oerjan> @check \x -> (-1) .&. x == x
03:27:49 <lambdabot> +++ OK, passed 100 tests.
03:27:54 <oerjan> checks out
03:28:23 <hppavilion[1]> oerjan: Well duh
03:28:28 <quintopia> wow such activity
03:28:52 <hppavilion[1]> oerjan: -1 = 1xN, where N is the bitwidth of the number
03:28:58 <hppavilion[1]> At least, if you're doing 2's complement
03:28:59 <ais523> hmm, if oerjan doesn't know either, perhaps there isn't a standard notation after all
03:29:14 <oerjan> hppavilion[1]: this is haskell Integer the bitwidth is infinite hth
03:29:16 <mad> wouldn't it be 0?
03:29:17 <hppavilion[1]> ais523: So you get to make up your own
03:29:22 <hppavilion[1]> oerjan: Shit.
03:29:35 <mad> logically 0 is the only integer expressible in 0 bits
03:29:40 <hppavilion[1]> oerjan: Therefor -1 = 0b111111111111111111111111111111111...
03:29:47 <hppavilion[1]> mad: WRONG!
03:30:02 <hppavilion[1]> mad: You can express any integer in 0 bits if it is pre-known what integer that is
03:30:04 <oerjan> ais523: it's not something i recall using
03:30:18 <ais523> it's weird, you'd expect it to come up more often
03:30:30 <ais523> but Wikipedia doesn't mention it either (merely that all such sets are equivalent)
03:30:33 <hppavilion[1]> mad: e.g. if we agree that in our encoding for integers, 69=0b, then 69=0b
03:30:42 <ais523> I guess I'll define 1 as containing an empty tuple for now, I can always change later
03:30:49 <mad> hppavilion[1] : true but using the normal positional encoding, then it's 0
03:30:50 <oerjan> ais523: that's the problem in CT, elements are not canonical
03:30:58 <hppavilion[1]> mad: Unless you're including the bits to define the encoding, in which case WRONG
03:31:03 -!- XorSwap has quit (Quit: Leaving).
03:31:11 <shachaf> ais523: Sometimes I call that element ★
03:31:32 <mad> shouldn't the empty tuple simply be an empty tuple?
03:31:50 <ais523> oerjan: well in the category of sets, each object is an equivalence set of sets, right? otherwise it'd have more than one terminal object which is impossible
03:31:51 <hppavilion[1]> IE(<op>) perhaps, where <op> is the operator you want the identify for?
03:31:52 <ais523> shachaf: actually that rings a bell
03:31:54 <hppavilion[1]> *identity
03:32:01 <mad> represented by something like {}
03:32:21 <ais523> mad: the empty tuple is just an empty tuple; however, because there's only one empty tuple
03:32:44 <ais523> the set of all empty tuples is thus equivalent to 1, and is in fact the definition of 1 that most practical programming languages choose
03:33:22 <hppavilion[1]> ais523: Wouldn't it be that the /cardinality/ of the set of all empty tuples is thus equivalent to 1?
03:33:43 <oerjan> ais523: there is nothing preventing a category from having more than one terminal object
03:33:56 <oerjan> they just all have to be isomorphic
03:34:18 <mad> dunno, in C++ there's an infinity of empty vectors more or less
03:34:29 <mad> though they do have the same value
03:34:33 -!- callforjudgement has joined.
03:34:36 <hppavilion[1]> So can I get an answer? It'll onlt take a second
03:34:37 <callforjudgement> [03:32] <ais523> mad: the empty tuple is just an empty tuple; however, because there's only one empty tuple
03:34:39 <callforjudgement> [03:32] <ais523> the set of all empty tuples is thus equivalent to 1, and is in fact the definition of 1 that most practical programming languages choose
03:34:43 <callforjudgement> [03:34] <ais523> ah hmm, according to Wikipedia you can have more than one terminal object if they're all isomorphic
03:34:46 -!- ais523 has quit (Disconnected by services).
03:34:49 -!- callforjudgement has changed nick to ais523.
03:34:50 <oerjan> > [minBound .. maxBound :: ()]
03:34:51 <lambdabot> [()]
03:35:24 <ais523> > [minBound .. maxBound :: [()]]
03:35:25 <quintopia> ais523: is it like bottom? or just like bijective base-k 0?
03:35:25 <mad> I guess the problem with 1 is that it doesn't express type
03:35:25 <lambdabot> No instance for (Enum [()])
03:35:25 <lambdabot> arising from the arithmetic sequence ‘minBound .. maxBound :: [()]’
03:35:25 <lambdabot> In the expression: [minBound .. maxBound :: [()]] No instance for (Bo...
03:35:44 <ais523> mad: well, it is a type itself, really
03:35:48 <hppavilion[1]> Object Creation syntax in my language.
03:35:48 <mad> and calling a 0-size thing 1 is confusing
03:36:03 <mad> ais523 : why do you need a type for 0-sized stuff
03:36:11 <hppavilion[1]> For example, srv <- new ssv.srv
03:36:12 <ais523> mad: well 0 has fewer possibilities than 1 does
03:36:17 <ais523> mad: because you're using a generic type
03:36:26 <ais523> and one of the fields happens to be unused
03:36:37 <ais523> > [], [()], [(), ()]
03:36:39 <lambdabot> <hint>:1:3: parse error on input ‘,’
03:36:40 <mad> that makes no sense
03:36:46 <ais523> > [[], [()], [(), ()]]
03:36:48 <lambdabot> [[],[()],[(),()]]
03:36:52 <mad> 1 is already 0 bit
03:37:16 <ais523> mad: that was me using the type [()] in Haskell
03:37:17 <hppavilion[1]> \oren\_: You're the one who hates OO with a passion?
03:37:22 <ais523> i.e. a list of 1
03:37:38 <ais523> it's equivalent to the natural numbers
03:37:49 <mad> ais523 : oh, then I don't think a value for empty fields is a good idea
03:38:00 <shachaf> ais523: Does the category 2 have one or zero non-identity arrows?
03:38:07 <ais523> mad: you can't construct an object without being able to initialize all its fields, including the empty ones
03:38:24 <hppavilion[1]> SO MUCH ACTIVITY
03:38:26 <ais523> shachaf: that was hotly debated at a seminar I attended recently
03:38:27 <hppavilion[1]> BWWAAAAAAAAAAAAAAAA
03:38:46 <mad> imho the property of a field having a value should probably be separate from the value of that field itself
03:39:08 <ais523> the seminar presenter was using an arrow in the definition of 2, but some of the audience disagreed
03:39:47 <shachaf> Some people refer to the one without the arrow as 1+1
03:40:06 <oerjan> 2 as the category for the partial order of {0,1} needs an arrow from 0 to 1
03:40:17 <ais523> apparently it was needed for the definition of if to work correctly
03:40:44 <shachaf> I think 2 should probably have an arrow.
03:40:47 <ais523> I think I'm going to call the element of 1 •, because I vaguely remember seeing that name in the past
03:41:18 <ais523> so I guess 3 has three non-identity arrows, one of which is the composition of the other two?
03:41:32 <oerjan> :k Void
03:41:34 <lambdabot> *
03:41:47 <oerjan> > Right () :: Either Void ()
03:41:49 <lambdabot> Right ()
03:42:03 <ais523> oerjan: what answer were you expecting from that :k query?
03:42:06 <oerjan> that requires Void to have a Show instance.
03:42:11 <shachaf> ais523: 3 = {0,1,2}
03:42:19 <oerjan> ais523: i was just checking if it was imported.
03:42:23 <shachaf> As both a set and a poset.
03:42:26 <ais523> shachaf: err, types don't have other types as arguments
03:42:34 <ais523> 3 = {0,1,2}, without the bold, I'll believe
03:42:36 <ais523> oerjan: ah right
03:42:52 <shachaf> Well, OK.
03:42:58 <shachaf> I'm not sure what you mean by argument.
03:43:04 <ais523> I meant element
03:43:11 <ais523> and said the wrong word
03:43:32 <mad> so basically a 1 field can only contain {0}. a 0 field cannot contain any number? (so is basically a guaranteed exception on read?)
03:43:36 <shachaf> I was talking about the category, not the type.
03:43:36 <mad> ?
03:43:41 <shachaf> Or really the poset.
03:44:31 <shachaf> Anyway it didn't really make sense.
03:44:37 <ais523> well in the seminar in question, 2 had objects {ff,tt}
03:45:02 <shachaf> But the other day I was at a talk about Lawvere's fixed point theorem and we figured out a good example that used the poset 2.
03:45:02 <ais523> which is a semi-common notation for false and true
03:45:06 <ais523> presumably used to save space while being distinctive
03:45:09 <shachaf> Which has the fixed point property.
03:45:26 <oerjan> > read "Right ()" :: Either Void () -- Read instance, too
03:45:27 <shachaf> There's an epimorphism : N -> 2^N
03:45:28 <lambdabot> Right ()
03:45:48 -!- augur_ has changed nick to augur.
03:45:50 <ais523> oerjan: can't you trivially define instances of pretty much every typeclass for Void?
03:46:08 <shachaf> 2^N = N union {infinity}
03:46:16 <shachaf> I don't have all my Unicode things set up here. :-(
03:46:26 <ais523> assuming every function in the typeclass takes an argument of the type (which is very common, although not technically required)
03:46:33 <ais523> you can just use absurd as the body
03:46:35 <oerjan> ais523: yes, but this Either argument shows why they're needed (and thus they've been added to GHC base)
03:47:11 <ais523> ah right
03:47:16 <mad> what's the practical use of this stuff&
03:47:17 <mad> ?
03:47:29 <ais523> let's see; a hypothetical non-base-kind Void wouldn't be a monad because you couldn't define return
03:48:55 <oerjan> hm
03:49:05 <oerjan> > Proxy >>= \x -> Proxy
03:49:07 <lambdabot> Proxy
03:49:27 <oerjan> edwardk mentioned he'd added a Monad instance for Proxy
03:49:57 <ais523> I'm assuming from this that Proxy has only one constructor that takes no arguments, and has kind * -> *?
03:50:04 <oerjan> it's the only Monad that doesn't distinguish return of different values
03:50:25 <shachaf> oerjan: Also (e,) for any Monoid e.
03:50:25 <oerjan> technically it has kind forall k. k -> *
03:50:25 <ais523> unlike Void, I can't immediately see an obvious use for Proxy, but I can easily believe there is one
03:50:37 <oerjan> but here k = *
03:51:04 <ais523> wait, Haskell has kind polymorphism?
03:51:16 <shachaf> GHC does.
03:51:20 <oerjan> ais523: it's useful for passing a type to a function when you have no value of it
03:51:44 <oerjan> or when a value would be illogical
03:52:01 <ais523> oerjan: why would you pass a type to a function? can Haskell do enough dependent typing to make that useful?
03:52:10 <oerjan> ais523: 8.0 will have kinds = types
03:52:24 <ais523> I guess it let's you define Idris' =
03:52:28 <ais523> which is far from useless
03:52:35 <ais523> err, refl, I mean
03:52:36 <oerjan> or has. how far has it got i'm still back in December on /r/haskell
03:52:39 <ais523> ^prefixes
03:52:39 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
03:52:48 <ais523> ( refl
03:52:51 <idris-bot> No such variable refl
03:52:52 <shachaf> ais523: It's useful for all sorts of things. sizeOf :: ... a => Proxy a -> Int
03:53:03 <shachaf> Haskell has Idris's equality.
03:53:17 <shachaf> data a :~: b where { Refl :: a :~: a }
03:53:19 <shachaf> It's in base.
03:53:21 <ais523> shachaf: can sizeOf be defined in Haskell itself? or is it a compiler builtin?
03:53:28 <shachaf> It's just a class.
03:53:33 <ais523> ah right
03:53:39 <shachaf> It's for the FFI.
03:55:00 <oerjan> ais523: GHC is in the process of having dependent types added.
03:55:32 <oerjan> although not totality, so it will have an inconsistent logic.
03:55:53 <ais523> it's not necessarily a problem for it to have an inconsistent logic, is it?
03:56:19 <ais523> you can't create an actual runtime error like that, just send the compiler into an infinite loop, IIRC
03:57:31 <pikhq_> And C++ seems fine with the same issue.
03:59:45 <ais523> actually you could create an infinite loop at runtime
03:59:48 <oerjan> ais523: yes, Richard Eisenberg who is designing this argues that GHC's internal coercion evidence is enough to keep it sound
03:59:58 <ais523> but that really isn't a problem, most people would consider it a feature not a bug
04:00:20 <shachaf> What are interesting objects that have the fixed point property?
04:00:38 <oerjan> but it does mean you cannot use GHC directly as a theorem prover
04:00:41 <shachaf> I.e. everything : X -> X is a fixed point.
04:02:03 <oerjan> shachaf: balls hth
04:02:29 <oerjan> assuming you mean has
04:02:55 <shachaf> I do mean has. Everything is a fixed point.
04:03:07 <oerjan> wat
04:03:13 <shachaf> Only closed balls, presumably.
04:03:18 <oerjan> yeah
04:03:19 <shachaf> oerjan: (Of id.)
04:03:27 <shachaf> Anyway, what else?
04:03:39 <shachaf> Things like 2, of course.
04:04:02 <shachaf> Every type in Haskell has the fixed point property.
04:04:16 <shachaf> (And the proof is identical to Lawvere's proof.)
04:11:04 <ais523> how are we defining fixed point, here?
04:11:54 <shachaf> I think with global elements.
04:11:55 <oerjan> hm it does seem to require actual underlying sets.
04:12:06 <shachaf> So x : 1 -> X such that f . x = x
04:12:15 <oerjan> ooh
04:13:05 <oerjan> you can construct that if you have limits in the right direction, can't you
04:13:17 <oerjan> or wait
04:13:17 <shachaf> ?
04:13:45 <coppro> what is the "fixed point property"?
04:14:05 <shachaf> X has the fixed point property if every arrow : X -> X has a fixed point.
04:14:13 <coppro> ah
04:14:28 <oerjan> or wait, a limit of X'es may not itself be X, perhaps
04:15:02 <coppro> ais523: also in our discussion earlier about types and elements, technically Void in Haskell also has one value, and () has two.
04:15:19 <ais523> bottom isn't really a value
04:15:43 <shachaf> It can be.
04:15:49 <oerjan> ais523: that's a flamewar issue i think
04:16:09 <shachaf> Actual Haskell and Haskell where you pretend everything is total both make for legitimate categories.
04:16:10 <oerjan> the haskell report treats it as one
04:16:15 <coppro> it's very relevant to what shachaf is saying ;) The existence of bottom guarantees the fixed point property
04:16:26 <shachaf> Yes, 20:04 <shachaf> Every type in Haskell has the fixed point property.
04:16:41 <ais523> I remember reading an article that mentioned how Haskell was pretty much the only language whose definition specifically talked about infinite loop handling
04:16:59 <coppro> Each arrow X-> X is a function, which must either examine the value passed in or not. If it doesn't, it is constant, so its value is its fixed point. Otherwise, it examines it, and therefore bottom is a fixed point.
04:17:16 <ais523> coppro: right, I'd almost proved that myself
04:17:23 <coppro> (or the arrow 1 |-> bottom, if we go by generalized elements)
04:17:25 <coppro> err
04:17:25 <ais523> was thinking "x = undefined"
04:17:26 <shachaf> oerjan: Anyway, Set has all small limits, but only one-element sets have the fixed point property.
04:17:27 <coppro> global elements
04:17:30 <ais523> hadn't adjusted for laziness yet though
04:17:32 <oerjan> coppro: no, that's too simple
04:17:38 <shachaf> coppro: It doesn't have to be constant.
04:17:41 <oerjan> coppro: e.g. \x -> 1:x
04:17:47 <coppro> ah, hmm
04:17:55 <coppro> I hadn't thought of that
04:18:07 <shachaf> But certainly every type has the fixed point property, because of fix.
04:18:10 <coppro> right
04:18:15 <ais523> x = fix f
04:18:16 <oerjan> don't worry, i just made the same thought error 10 mins ago
04:18:37 <ais523> hmm, now I just remembered that ursala had pluggable fixed point operators
04:18:41 <ais523> I can't remember why, though
04:18:51 <ais523> it's ursala so we might not get sensible answers
04:19:49 <ais523> would you consider ursala an esolang, btw?
04:19:56 <coppro> right, so the non-examining case becomes "applies a possibly-empty series of constructors to its value" (we can beta reduce functions to get a series of constructors)
04:20:22 <ais523> it passes the weirdness test about as well as bancstar, but also has the advantage that its author considered that other people might find it surprising or hard to learn
04:20:23 <coppro> which can be made into a fixed point in the manner that fix works
04:21:01 <shachaf> If you consider lambda a constructor.
04:21:07 <shachaf> Or, you know what I mean.
04:21:28 <coppro> yes, in this case I do
04:21:37 <shachaf> Anyway Haskell is boring because every type has the fixed point property. And sets is boring because only one-element sets do.
04:22:05 <oerjan> and Top is less boring because, balls
04:22:19 <shachaf> Algebraic things like monoids or pointed sets or something are also boring because a monoid homomorphism maps the identity to the identity.
04:22:28 <shachaf> Topological spaces are more interesting for the reason oerjan mentioned.
04:22:35 <ais523> Top is Void, right?
04:22:38 <shachaf> Partial orders are a special case of topological spaces.
04:22:43 <shachaf> Top the category of topological spaces.
04:22:45 <ais523> and Bottom is ()
04:22:55 <ais523> shachaf: ah right
04:23:06 <shachaf> But if you're talking about initial and terminal objects in Haskell, it would be the other way around if anything.
04:23:36 <shachaf> (Or "subtyping", where (forall a. a) ~~ Void is bottom, and (exists a. a) ~~ () is top.)
04:23:48 <ais523> shachaf: bottom is initial, or terminal?
04:24:05 <shachaf> Usually people say initial.
04:24:49 <oerjan> it's not initial in haskell
04:24:51 <ais523> oh, that's what was confusing me
04:24:55 <oerjan> or wait, is it
04:25:06 -!- Alcest has joined.
04:25:07 <oerjan> darn
04:25:13 <shachaf> Void is initial in Haskell-without-bottoms.
04:25:20 <ais523> oerjan: absurd basically takes an initial value (i.e. a value of an initial type) and produces a value of any type
04:25:46 <oerjan> OKAY
04:25:46 <shachaf> There's no such thing as an initial value here. :-)
04:25:50 <ais523> which is very very close to the definition of initial types being an initial object
04:25:55 <ais523> shachaf: I know :-)
04:26:16 <ais523> or, well, you can view absurd in two ways
04:26:20 <ais523> either as being an empty function
04:26:24 <ais523> or as mapping bottoms to other bottoms
04:26:53 <oerjan> hm does the projective plane have the fixpoint property - there's this borsuk-ulam thing
04:27:26 <shachaf> ais523: In the second perspective (where _|_ is a value) Void isn't initial.
04:28:16 <ais523> shachaf: for it to not be initial implies that either: a) there's a type T for which there's no function of type Void -> T; or b) there's a type T for which there are two non-equivalent functions of type Void -> T
04:28:28 <ais523> a) can't be true because absurd is always a function that fits the requirement
04:28:59 <shachaf> ais523: (\_ -> ()) and (\() -> ()) are two different functions.
04:29:11 <ais523> ah right, laziness again
04:29:44 <shachaf> On the other hand Void is terminal.
04:31:36 <ais523> but only because all bottoms are equivalent
04:41:47 -!- tromp_ has joined.
05:02:39 -!- MDude has changed nick to MDream.
05:08:39 <\oren\_> orital docking achieve
05:24:33 -!- tromp_ has quit (Remote host closed the connection).
05:30:01 -!- ais523 has quit.
05:41:25 -!- nisstyre has joined.
05:42:02 -!- nisstyre has quit (Changing host).
05:42:02 -!- nisstyre has joined.
05:42:35 -!- oerjan has quit (Quit: Nite).
06:25:05 -!- tromp_ has joined.
06:25:57 <izabera> https://asciinema.org/a/35400
06:29:15 -!- tromp_ has quit (Ping timeout: 240 seconds).
06:32:36 * zgrep starts searching for words after losing them due to looking izabera's brainfuck mastery... (basically, zgrep is speechless)
06:32:43 <zgrep> s/ing /ing at /
06:32:47 <zgrep> Err...
06:32:50 <zgrep> s/king /king at /
06:33:13 <lifthrasiir> izabera: is it going to be faster than bff4? :)
06:39:14 <izabera> lol not any time soon
06:47:32 -!- Sgeo has quit (Ping timeout: 256 seconds).
06:57:01 -!- infinitymaster has joined.
07:03:24 -!- FreeFull has quit (Ping timeout: 256 seconds).
07:03:37 <HackEgo> [wiki] [[The chan-esoteric stack]] https://esolangs.org/w/index.php?diff=46350&oldid=46346 * Hppavilion1 * (+60) /* The Stack */ Clarification
07:03:48 <b_jonas> http://magic.wizards.com/en/articles/archive/feature/oath-gatewatch-update-bulletin-2016-01-29 M:tG OGW update bulletin
07:03:58 -!- Sgeo has joined.
07:05:23 <hppavilion[1]> Sghello
07:05:50 <b_jonas> (yes, I know it's like four days old, but I wasn't here)
07:06:11 <hppavilion[1]> Sgeo: I'm engineering my own personal solution stack :)
07:07:26 <Sgeo> hppavilion[1], cool. For what? (And meaning what?)
07:07:51 <hppavilion[1]> Sgeo: Just a general stack (like LAMP or XAMPP or MEAN) for web development :)
07:08:02 <hppavilion[1]> Sgeo: I'm rolling my own database and my own language
07:08:13 <Sgeo> Ah
07:08:14 <hppavilion[1]> The language is suitable for golphing, if one were to feel like it
07:08:19 <hppavilion[1]> Here's a cat server in it:
07:08:20 <hppavilion[1]> |ssv;srv<-$ssv.srv '' 4242;upn srv.srcv{sck<-caller.sck;(<<-sck)->>sck}
07:08:23 <b_jonas> That article says the update about the colorless mana symbol affects 316 cards, which ALMOST perfectly matches with my previous regex /\{[1-9X]\}[^:]*pool/ which matches 317 cards
07:10:08 <hppavilion[1]> Granted, that uses a library (ssv), but still
07:17:08 <shachaf> What's with the new colorless mana symbol?
07:17:11 <shachaf> Seems a bit scow to me.
07:38:53 -!- infinitymaster has quit (Remote host closed the connection).
07:39:47 <b_jonas> although some of the 317 matches are un-cards, certainly not updated, so it's not that good of a match
07:40:05 <b_jonas> shachaf: do you want a serious answer?
07:40:38 <shachaf> I know how it works, I'm just not quite sure of the motivation.
07:42:22 <b_jonas> The regex has at least one false hit: it matches Charmed Pendant's reminder text and Power Sink's ability and (embarassingly) Mirrorpool's trigger.
07:43:47 <b_jonas> /\{[1-9X]\}[^:\n]*\bpool/ is better, only two false positives
07:44:10 <shachaf> i,i Charmed Pedant
07:45:28 <shachaf> Hmm, I didn't know Power Sink.
07:45:41 <b_jonas> two false positives other than two un-cards
07:45:44 <shachaf> Is there something that has tapping all your lands as a cost?
07:45:51 <shachaf> I'm not sure how that would be phrased exactly.
07:46:04 <b_jonas> shachaf: I'm not sure if it exists as a cost, but it exists as an effect
07:46:58 <shachaf> Tap all lands you control: [...]. Activate this ability only if you control no tapped lands.
07:47:18 <shachaf> Or {X} where X is the number of lands you control. Of course those are quite different.
07:47:26 <shachaf> What has it as an effect?
07:48:20 -!- mad has quit (Quit: Pics or it didn't happen).
07:48:26 <b_jonas> shachaf: Pygmy Hippo and War's Toll -- note that they're somewhat different
07:49:13 <shachaf> Oh, that affects your opponent, not you.
07:51:30 <shachaf> Is there something which uses some other mechanism to be cheap in the early game and expensive in the late game?
07:55:06 <hppavilion[1]> The people of this channel could do so much good if Esolangs were useful in the slightest...
07:56:09 <izabera> we need something like an esolangs4charity marathon
07:58:38 <hppavilion[1]> izabera: That'd only work if the rest of the programming world was into esolangs
07:59:23 <izabera> ok, that's step 1
08:02:38 <hppavilion[1]> izabera: Good point
08:02:48 <hppavilion[1]> Step 1) Get the world to like esolangs
08:03:03 <hppavilion[1]> Step 2) Do an Esolangs4Charity competition/marathon/whatever
08:03:09 <hppavilion[1]> Step 3) WORLD DOMINATION
08:03:14 <hppavilion[1]> Step 4) Buy milk
08:03:22 <myname> good luck with step 1
08:03:35 <myname> even at my university, i am the strange one
08:05:00 <izabera> can we just move step 4 a bit higher in the list?
08:05:46 <myname> we may swap 3 and 4
08:05:53 <izabera> yay
08:07:16 -!- charles047 has joined.
08:07:18 <charles047> Hi. Just came across this, please read and comment with your thoughts http://chrishadnagy.com
08:07:42 <myname> no
08:08:20 <myname> first of all, i will not support spammers in any way
08:09:42 <izabera> not even *esoteric* spammers?!
08:10:09 <myname> only if i can clearly identify it as such
08:10:14 <myname> which i cannot
08:12:01 <shachaf> Invent an esoteric programming language where a program is only valid if it was written in good faith that it will terminate.
08:13:15 <izabera> do you have to invent it from scratch or can you just apply that property to something like python?
08:27:52 -!- ais523 has joined.
08:38:02 -!- hppavilion[1] has quit (Ping timeout: 256 seconds).
09:25:59 -!- tromp_ has joined.
09:26:03 -!- zadock has joined.
09:28:38 -!- AnotherTest has joined.
09:34:17 -!- ais523 has quit.
09:50:34 -!- tromp_ has quit (Ping timeout: 256 seconds).
10:07:24 -!- MoALTz has quit (Ping timeout: 252 seconds).
10:51:46 -!- J_Arcane has quit (Ping timeout: 252 seconds).
10:56:36 <b_jonas> `ftoc 73
10:56:51 <HackEgo> 73.00°F = 22.78°C
11:21:11 -!- mauris__ has joined.
11:22:57 -!- zadock has quit (Quit: Leaving).
11:26:58 -!- mauris__ has quit (Ping timeout: 252 seconds).
11:30:43 -!- boily has joined.
11:34:00 -!- ais523 has joined.
11:47:24 -!- tromp_ has joined.
11:48:28 <boily> @metar CYUL
11:48:28 <lambdabot> CYUL 031137Z 04016KT 3SM -FZRA -SG FEW010 OVC043 M03/M05 A3004 RMK SF2SC6 PRESFR SLP175
11:48:43 <boily> FZRA!
11:50:59 <ais523> is that freezing rain?
11:51:15 <boily> it's freezing rain.
11:51:26 -!- tromp_ has quit (Ping timeout: 240 seconds).
11:51:54 -!- AnotherTest has quit (Ping timeout: 252 seconds).
11:52:45 <izabera> it's -FZRA
11:53:32 <izabera> means "very definitely NOT freezing rain"
11:54:27 <boily> a - means light.
11:54:39 <izabera> whaaaaa
11:54:48 <boily> (strangely, everything tends to be light when reported here. -RA, -SN, -BR...)
11:55:04 <boily> no prefix is about average, and + is heavy. hth.
11:55:30 * izabera knows nothing about metar
11:56:40 <Melvar> @metal EDLW
11:56:41 <lambdabot> EDLW 031150Z 26010KT 240V310 9999 FEW027 06/M00 Q1015
11:58:01 <boily> Mellolvar. I see what you did there hth
11:58:14 <boily> izabera: where are you approximatively at?
11:58:42 <izabera> on a train going to milan
11:58:58 <Melvar> I wonder where the LW bit comes from.
11:59:53 -!- AnotherTest has joined.
12:00:36 <boily> @metar LIML
12:00:37 <lambdabot> LIML 031150Z 16003KT 130V190 2000 -DZ BR SCT003 BKN030 09/08 Q1014 NOSIG
12:01:02 <izabera> in english?
12:01:11 <boily> typing it...
12:02:12 <izabera> this train is awful
12:02:25 <izabera> shitty, stinks
12:02:46 <boily> report made today at 11:50 UTC, 3 kt south wind, varying between south-east and south-west, ground visibility 2 km, light drizzle, fog, scattered clouds at 300', broken clouds at 3000', it's +9 °C, dew point at 8 °C, sea level pressure 1014 hPa, nothing else to report.
12:02:53 <izabera> can't even charge my laptop
12:03:23 <izabera> boily: sooo... foggy?
12:04:12 <ais523> not very foggy if you can see 2km
12:04:14 <boily> foggy and humid.
12:05:14 <boily> where does the LW bit come from... can't find anything.
12:13:13 <b_jonas> `wisdom
12:13:24 <HackEgo> mojibake/mojibake _ÌÌÌ°_ÌÌ̦̻ͭͭͬÌÍÌÌÍ¡_ͧÍÌÍÌ­_ÍÍÍͧÍÌÌ̯Í̬̬̦̯_ÌÌÌͨÌÌ´Í
12:13:38 <b_jonas> that
12:13:43 <b_jonas> doesn't even make any sense
12:13:55 <b_jonas> it doesn't look realistic
12:13:57 -!- ais523 has quit.
12:14:14 <boily> it's an overencoded wisdomface.
12:14:19 <boily> `? asdfasfawtraritoa
12:14:21 <HackEgo> asdfasfawtraritoa? ¯\(°​_o)/¯
12:14:49 <b_jonas> hmm
12:15:05 <b_jonas> should we try to make an automatic decoding tool for this?
12:15:13 <b_jonas> or would that be heretical?
12:15:21 <b_jonas> yes, I know the format isn't completely uniform
12:15:22 <b_jonas> but still
12:19:03 <boily> Ì.
12:20:10 -!- deltab has quit (Ping timeout: 256 seconds).
12:22:01 -!- boily has quit (Quit: SUBLAYER CHICKEN).
12:24:16 -!- mezkhalin has joined.
12:27:15 -!- deltab has joined.
12:32:43 <mezkhalin> @tell LexiciScriptor bad day yesterday and i lost the logs. remind me again what form of O() did you write? :P
12:32:43 <lambdabot> Consider it noted.
12:34:03 -!- Alcest has quit (Ping timeout: 240 seconds).
12:50:14 -!- mauris__ has joined.
12:54:10 <b_jonas> `? game
12:54:14 <HackEgo> game? ¯\(°​_o)/¯
12:58:54 -!- myname has quit (Ping timeout: 250 seconds).
13:02:56 -!- mauris__ has quit (Quit: Leaving).
13:11:37 -!- mauris has joined.
13:20:54 -!- TodPunk has quit (Read error: Connection reset by peer).
13:21:22 -!- TodPunk has joined.
13:41:55 -!- FreeFull has joined.
13:44:57 -!- tromp_ has joined.
13:59:41 -!- tromp_ has quit (Remote host closed the connection).
14:21:30 -!- `^_^v has joined.
14:27:18 -!- tromp has quit (Killed (Sigyn (Spam is off topic on freenode.))).
14:28:02 -!- tromp has joined.
14:28:27 -!- mauris_ has joined.
14:28:41 -!- myname has joined.
14:29:22 -!- mauris has quit (Ping timeout: 256 seconds).
14:42:43 -!- Treio has joined.
15:00:13 -!- tromp_ has joined.
15:03:58 -!- charles047 has quit (Quit: :D).
15:05:04 -!- tromp_ has quit (Ping timeout: 256 seconds).
15:18:43 -!- bb010g has quit (Quit: Connection closed for inactivity).
15:20:57 -!- spiette has joined.
15:49:52 -!- Treio has quit (Ping timeout: 252 seconds).
16:03:39 <HackEgo> [wiki] [[Special:Log/newusers]] create * FricativeMelon * New user account
16:05:23 <b_jonas> `wisdom
16:05:33 <b_jonas> `8-ball is that a spam user?
16:05:33 <HackEgo> phantom_hoover/Phantom Michael Hoover is a true Scotsman, hatheist, and completely out of the loop.
16:05:35 <HackEgo> Concentrate and ask again.
16:12:36 -!- oerjan has joined.
16:17:41 <quintopia> Fricative eh
16:17:49 <quintopia> Like a chicken fricative?
16:17:58 <quintopia> (this will be in a boily part message soon)
16:20:40 <Melvar> “Melon” doesn’t even contain any fricatives.
16:26:31 <oerjan> it's surprisingly devoid of them.
16:36:15 -!- `^_^v has quit (Ping timeout: 260 seconds).
16:37:13 -!- `^_^v has joined.
16:37:31 <oerjan> @metar ENVA
16:37:32 <lambdabot> ENVA 031620Z 25013KT 9999 6000E -SHSNRA FEW010CB SCT024 BKN034 02/M01 Q0993 TEMPO 1200 SHSN VV007 RMK WIND 670FT 25014G24KT
16:42:34 <Melvar> @metal EDDL
16:42:34 <lambdabot> EDDL 031620Z 26014G24KT 9999 SCT018 BKN050 05/01 Q1019 NOSIG
16:43:24 <oerjan> dusseldörf
16:43:37 <Melvar> Hmm. Is @metal better than @messages-lewd …?
16:44:56 <oerjan> @fetal LIRO
16:44:56 <lambdabot> Maybe you meant: metar keal eval
16:45:00 <oerjan> darn
16:45:08 <oerjan> stupid ambiguities
16:49:46 -!- `^_^v has quit (Ping timeout: 240 seconds).
16:51:48 <Taneb> Line in a blog post I am writing: «most people call 1 dimensional triangles "lines"»
16:53:15 <oerjan> those lines, so degenerate
16:53:32 <b_jonas> aren't those line segments?
16:53:33 <int-e> line segments with a distinguished point...
16:53:40 -!- `^_^v has joined.
16:53:41 <int-e> my bet would be s/lines/stupid/ though
16:54:26 <Taneb> I'm talking about generalizing triangle numbers into other dimensions
16:54:32 <Taneb> Like tetrahedron numbers
16:55:00 <int-e> oh, simplices
16:55:36 <int-e> That's fine then; a one-dimensional simplex is a line segment.
16:56:10 <Taneb> Oh, there's a word for these?
16:56:32 <Taneb> That's useful
16:57:48 <b_jonas> T: wouldn't that be just the binomial coefficients?
16:57:48 <Taneb> Am I allowed to talk about, say, the 6th 5-simplex number?
16:57:55 <HackEgo> [wiki] [[Beeswax]] https://esolangs.org/w/index.php?diff=46351&oldid=46090 * Albedo * (+183) /* Local/global stack interaction */ Instruction U added
16:59:16 <HackEgo> [wiki] [[Beeswax]] M https://esolangs.org/w/index.php?diff=46352&oldid=46351 * Albedo * (+3) /* Global stack related I/O */
17:06:10 <oerjan> Taneb: those are usually called "binomial coefficients" hth
17:06:15 <oerjan> oops
17:06:24 <oerjan> stupid skipping of lines
17:06:51 <Taneb> oerjan, I'm trying to explain where the binomial coefficients are coming from
17:06:56 <Taneb> And what they have to do with yahtzee
17:10:33 <zgrep> What do they have to do with yahtzee
17:10:33 <zgrep> +
17:10:34 <zgrep> ?
17:11:23 <Taneb> zgrep, the number of ways you can roll 5 dice if you don't care about order is the 6th 5-simplex number
17:11:37 * zgrep looks up simplex numbers
17:12:31 -!- Reece` has joined.
17:13:46 <zgrep> Does yahtzee care about order?
17:14:08 <int-e> the game doesn't; the associated probabilities do.
17:15:40 <Taneb> And in general, the number of ways you can roll n d-sided dice if you don't care about order is the dth n-simplex number
17:20:24 -!- oerjan has quit (Quit: Later).
17:51:05 -!- MoALTz has joined.
17:54:24 -!- jaboja has joined.
17:58:39 <izabera> guys
17:58:46 <izabera> strpbrk runs in linear time
17:59:16 * izabera astonished by this
17:59:47 -!- vodkode has joined.
18:01:08 -!- tromp_ has joined.
18:04:08 -!- hppavilion[1] has joined.
18:06:04 -!- tromp_ has quit (Ping timeout: 272 seconds).
18:06:18 -!- Reece` has quit (Quit: Alsithyafturttararfunar.).
18:08:44 -!- LexiciScriptor has joined.
18:10:36 -!- Reece` has joined.
18:13:49 <Melvar> izabera: Linear in what?
18:14:18 <izabera> lenght of the string
18:14:35 <izabera> char *strpbrk(const char *s, const char *accept); <- of s
18:15:20 <Melvar> Well, the most naive algorithm would do that (where you loop through accept for each char in s).
18:15:46 <izabera> no
18:15:57 <izabera> unless your naive algorithm is way more advanced than mine
18:15:58 -!- mauris__ has joined.
18:15:58 -!- jaboja has quit (Remote host closed the connection).
18:16:00 <Melvar> Oh, you mean the runtime is independent of accept?
18:16:07 <izabera> yes
18:17:13 <Melvar> That *is* surprising.
18:17:20 <izabera> there's a version in assembly for x86_64 in glibc, very well commented
18:18:19 <izabera> http://git.musl-libc.org/cgit/musl/tree/src/string/strpbrk.c http://git.musl-libc.org/cgit/musl/tree/src/string/strcspn.c musl does it in O(n+m)
18:18:21 <izabera> still linear
18:18:40 <izabera> and no comments because fuck you
18:18:44 -!- mauris_ has quit (Ping timeout: 252 seconds).
18:19:35 -!- hppavilion[1] has quit (Ping timeout: 276 seconds).
18:20:09 <shachaf> Punycode is too complicated.
18:22:31 -!- Reece has joined.
18:22:35 -!- Reece` has quit (Ping timeout: 245 seconds).
18:23:46 <fizzie> It's still linear in length of s even if it depends on the length of accept.
18:24:29 <fizzie> (I mean, if you only paramterize by length of s.)
18:28:01 <fizzie> I don't think the musl one really needs comments, it's pretty obvious of what it does.
18:29:16 <izabera> comments don't make your executable larger
18:30:11 -!- sebbu has quit (Ping timeout: 264 seconds).
18:31:52 * izabera didn't see a jnz in glibc and it was obviously needed so both run in O(n+m)
18:34:38 <fizzie> No, but there's no need to add comments where it's obvious either. Granted, the musl example might not be quite.
18:34:50 <fizzie> But, for example, return result; // Returns the result.
18:36:07 <izabera> int main(int argc, char **argv) { /* program starts here */
18:41:07 <fizzie> int /* return type of integer */ main /* <- this is the function name */ /* watch out, a parenthesis: */ ( int argc, ...
18:43:37 <izabera> could probably use some vertical whitespace
18:47:38 -!- sebbu has joined.
18:49:50 -!- sebbu has quit (Read error: Connection reset by peer).
18:50:58 -!- sebbu has joined.
18:51:20 <b_jonas> fizzie: yeah, there's some assembly code out there commented that way
18:51:36 <b_jonas> it's even more horrible because it's like
18:51:50 <b_jonas> XOR AL, AL ;clear the AL register
18:52:33 <b_jonas> registers aren't named meaningfully for the code, and comment doesn't tell what AL is actually used for in that section
18:59:48 -!- Treio has joined.
19:07:30 -!- augur has quit (Ping timeout: 272 seconds).
19:10:44 -!- bb010g has joined.
19:15:38 -!- XorSwap has joined.
19:20:24 -!- augur has joined.
19:26:42 -!- augur has quit (Ping timeout: 250 seconds).
19:31:06 -!- augur has joined.
19:33:48 -!- hppavilion[1] has joined.
19:39:08 <hppavilion[1]> i<-'$';w!i.eof{i<-gln inp;out<<-i}
19:41:47 <b_jonas> what is that?
19:43:29 <hppavilion[1]> b_jonas: Cat that terminates on EOF
19:43:41 <hppavilion[1]> b_jonas: In Shorthand
19:44:10 <b_jonas> I see
19:44:29 <b_jonas> um, what's Shorthand?
19:44:51 -!- Reece` has joined.
19:44:57 <hppavilion[1]> b_jonas: Language I'm making for golphing and scientific computing as part of my personal webstack
19:45:09 <b_jonas> that's golfed?
19:45:16 <hppavilion[1]> mezkhalin: Hi
19:45:17 -!- Reece` has quit (Max SendQ exceeded).
19:45:26 -!- Reece has quit (Ping timeout: 240 seconds).
19:45:28 <hppavilion[1]> b_jonas: It's as short as I can get it in my language xD
19:45:52 <hppavilion[1]> b_jonas: I suppose I could do perl's thing with undef for undefined variables...
19:46:04 <mezkhalin> hppavilion[1]: greetings!
19:46:14 <hppavilion[1]> mezkhalin: How's it going?
19:46:14 <mezkhalin> whats the topic?
19:46:31 <mezkhalin> haha verlet integration how about you?
19:48:05 -!- Reece` has joined.
19:48:16 -!- vodkode has quit (Quit: Leaving).
19:50:10 <HackEgo> [wiki] [[AnnieFlow]] N https://esolangs.org/w/index.php?oldid=46353 * FricativeMelon * (+6069) Created page with "'''AnnieFlow''' is a [[StackFlow]] derivative that has mostly the same behavior, except for the following: # It is much terser than StackFlow, with more condensed syntax. Ever..."
19:51:26 -!- augur has quit (Ping timeout: 250 seconds).
19:52:15 -!- Reece` has quit (Read error: Connection reset by peer).
19:52:18 <izabera> cat in bash is 3 characters
19:53:47 -!- Reece` has joined.
19:54:27 -!- Reece` has quit (Client Quit).
19:56:55 -!- Reece` has joined.
20:02:36 -!- tromp_ has joined.
20:04:21 -!- mihow has joined.
20:06:11 -!- hppavilion[1] has quit (Ping timeout: 276 seconds).
20:06:55 -!- tromp_ has quit (Ping timeout: 240 seconds).
20:11:40 -!- Treio has quit (Ping timeout: 252 seconds).
20:15:25 -!- augur has joined.
20:16:45 -!- XorSwap has quit (Quit: Leaving).
20:17:56 -!- jaboja has joined.
20:22:02 -!- Treio has joined.
20:22:23 -!- augur has quit (Ping timeout: 264 seconds).
20:22:42 <HackEgo> [wiki] [[AnnieFlow]] https://esolangs.org/w/index.php?diff=46354&oldid=46353 * FricativeMelon * (+332)
20:30:55 -!- augur has joined.
20:31:31 -!- hppavilion[1] has joined.
20:31:55 -!- mihow has quit (Ping timeout: 260 seconds).
20:34:04 -!- mihow has joined.
20:38:22 -!- augur has quit (Remote host closed the connection).
21:00:48 -!- vodkode has joined.
21:05:37 -!- hppavilion[1] has quit (Read error: Connection reset by peer).
21:06:26 -!- hppavilion[1] has joined.
21:08:21 -!- J_Arcane has joined.
21:09:42 -!- augur has joined.
21:16:32 -!- Reece has joined.
21:17:26 -!- Reece` has quit (Ping timeout: 240 seconds).
21:20:56 -!- oerjan has joined.
21:28:43 -!- bb010g has quit (Quit: Connection closed for inactivity).
21:34:35 -!- hppavilion[1] has quit (Ping timeout: 276 seconds).
21:35:38 -!- hppavilion[1] has joined.
21:38:56 -!- Reece has quit (Quit: Alsithyafturttararfunar.).
21:51:32 -!- hppavilion[1] has quit (Ping timeout: 272 seconds).
21:54:14 -!- MDream has changed nick to MDude.
21:59:23 <tswett> @tell ais523 I've seen ★ used as the element of "the" one-element collection.
21:59:23 <lambdabot> Consider it noted.
21:59:25 <tswett> Hmm.
21:59:35 <tswett> > read " Right ( ) " :: Either () ()
21:59:37 <lambdabot> Right ()
21:59:56 <tswett> > read " Right ( ( ) ) " :: Either () ()
21:59:57 <lambdabot> Right ()
22:00:03 <tswett> > read " ( Right ( ( ) ) ) " :: Either () ()
22:00:05 <lambdabot> Right ()
22:00:13 <tswett> > read " ( ( Right ) ( ( ) ) ) " :: Either () ()
22:00:15 <lambdabot> *Exception: Prelude.read: no parse
22:00:37 <tswett> > read "(((((Right((((())))))))))" :: Either () ()
22:00:39 <lambdabot> Right ()
22:02:31 -!- nycs has joined.
22:02:35 -!- hppavilion[1] has joined.
22:02:43 <oerjan> > read "(((((Right((((()),((()))))))))))" :: Either () ((),())
22:02:45 <lambdabot> Right ((),())
22:03:09 <oerjan> that's gonna need some backtracking for tuples...
22:03:31 <oerjan> > read "(((((((((()),((()))))))))))" :: ((),())
22:03:33 <lambdabot> ((),())
22:04:15 -!- `^_^v has quit (Ping timeout: 240 seconds).
22:04:24 <oerjan> hm can we get it to blow up
22:05:10 <oerjan> > read "(((((())))),())" :: ((),())
22:05:12 <lambdabot> ((),())
22:05:21 <oerjan> > read "(((((((())))))),())" :: ((),())
22:05:22 <lambdabot> ((),())
22:24:20 <oerjan> > read "((( ((((),()),()),()) )))" :: ((((),()),()),())
22:24:21 <lambdabot> ((((),()),()),())
22:24:35 <oerjan> > read "((((((( ((((),()),()),()) )))))))" :: ((((),()),()),())
22:24:37 <lambdabot> ((((),()),()),())
22:25:01 -!- XorSwap has joined.
22:27:54 <oerjan> i think this ReadP thing is thwarting me by not actually using backtracking.
22:38:37 -!- lleu has joined.
22:51:36 -!- mezkhalin has quit (Ping timeout: 252 seconds).
22:53:20 <hppavilion[1]> Overdone Programming: Taking a programming project that should be simple and producing the most horribly complicated possible version of it
22:53:28 -!- spiette has quit (Quit: :qa!).
22:54:00 <hppavilion[1]> Example: A command-line utility for saying "Hello, World" in a highly advanced way
22:56:42 <hppavilion[1]> Sort of like GNU Hello
22:58:34 <b_jonas> `hello
22:58:51 <HackEgo> Hello
23:00:22 -!- boily has joined.
23:01:40 -!- hppavilion[1] has quit (Ping timeout: 276 seconds).
23:06:34 -!- AnotherTest has quit (Ping timeout: 240 seconds).
23:07:29 -!- nycs has quit (Quit: This computer has gone to sleep).
23:10:29 <boily> @metar CYUL
23:10:29 <lambdabot> CYUL 032300Z 15013KT 15SM BKN033 OVC045 06/04 A2963 RMK SC6SC2 SLP037
23:11:09 <boily> there should be a lumens measure somewhere in those metars twh
23:11:23 <boily> today was distressingly dark.
23:14:44 -!- Treio has quit (Ping timeout: 248 seconds).
23:17:51 <fizzie> We used to have one at the university's weather thing.
23:18:00 <fizzie> http://outside.aalto.fi/
23:18:25 <fizzie> Or http://outside.aalto.fi/lite.html for the history.
23:21:25 <boily> fizziello!
23:21:46 <boily> not very bright out there.
23:27:16 -!- Treio has joined.
23:31:05 -!- Phantom_Hoover has joined.
23:31:15 -!- jaboja has quit (Remote host closed the connection).
23:34:27 -!- tromp_ has joined.
23:36:46 <zgrep> `hello world.
23:36:48 <HackEgo> Hello
23:38:56 -!- tromp_ has quit (Ping timeout: 250 seconds).
23:39:07 <boily> `hello hello
23:39:14 <HackEgo> Hello
23:39:21 -!- hppavilion[1] has joined.
23:41:03 <boily> hello hello helloppavellon[1] ♪
23:41:13 <boily> zgrellop!
23:45:53 -!- mauris__ has changed nick to mauri.
23:49:38 <oerjan> belloily
23:50:12 -!- XorSwap has quit (Ping timeout: 252 seconds).
23:50:56 -!- Treio has quit (Quit: Leaving).
23:53:22 <zgrep> helloily.
←2016-02-02 2016-02-03 2016-02-04→ ↑2016 ↑all