←2017-04-22 2017-04-23 2017-04-24→ ↑2017 ↑all
00:08:15 -!- oerjan has joined.
00:08:41 * DHeadshot has built quite a powerful gopher server program. I may make it opensource, I haven't decided yet...
00:10:02 <zzo38> What kind of features you put in? I have made a xinetd based gopher server program in C.
00:10:29 <zzo38> (A very simple one, but you can use external programs for adding additional functions)
00:11:13 <DHeadshot> I have full CGI compatibility, so it's fully extensible with existing applications.
00:11:23 <DHeadshot> No Gopher+ though
00:11:33 <DHeadshot> I still need to add that in.
00:14:49 <DHeadshot> (At least, that is the Linux version I made in 2015-16. The original Windows one was built in VB6 many years ago and is very simple).
00:14:59 -!- oerjan has set topic: Motivation: NaN | http://esolangs.org/ | logs: http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D | https://www.dropbox.com/s/fyhqyvy3i8oh25m/wisdom.pdf?dl=0 | For extensive phở testing, use #esoteric-blah.
00:24:32 -!- DHeadshot has quit (Ping timeout: 268 seconds).
00:32:45 <zzo38> I also have no Gopher+ and do not intend to add it either. Mine is using a prefix database, and then if the prefix matches (the prefix can include the null terminator), then does according to that record. The action can be: a text file, a binary file, execute a program, change directory, display error message, or load another prefix database.
00:33:38 <zzo38> There is also a compiler to create menus and compiled prefix databases from a source file.
00:33:44 -!- boily has joined.
00:38:16 <oerjan> @time rdococ
00:38:16 <lambdabot> Local time for rdococ is UTC!
00:38:27 <oerjan> shocking
00:38:31 <oerjan> helloily
00:38:35 <oerjan> `? har
00:38:36 <HackEgo> har? ¯\(°​_o)/¯
00:38:43 <oerjan> ah.
00:40:00 <zzo38> One thing named "har" is this: http://zzo38computer.org/prog/har.c
00:40:15 <oerjan> heh shachaf got enough
00:40:36 <oerjan> zzo38: it was one of rdococ's wisdom additions, but it got reverted.
00:40:39 <shachaf> ?
00:40:45 <zzo38> Got enough of what?
00:41:00 <shachaf> Is that as in "had enough"?
00:41:01 <oerjan> zzo38: of rdococ's very bad wisdom entries
00:41:07 <zzo38> O, OK
00:41:12 <oerjan> APPARENTLY
00:41:32 <shachaf> I don't think that's idiomatic English but maybe it should be.
00:41:45 <shachaf> I'll try to incorporate it into my lexicon maybe.
00:42:16 <oerjan> as long as you don't think it's scow.
00:45:42 <boily> hellørjan, hezzo38, helloochaf.
00:46:29 <boily> @massages-loud
00:46:30 <lambdabot> oerjan said 20h 14m 49s ago: your pdf is missing the "unary" in `? and hth
00:46:37 <oerjan> `slwd rdococ//s,all,almost &,
00:46:41 <HackEgo> rdococ//rdococ is apparently from Budapest, but he is actualmost ally on Mars. Thanks to boily he is approaching permanent boredom & mapoledom. Additionally, all of his wisdom entries are bad.
00:46:44 <oerjan> oops
00:46:46 <oerjan> `revert
00:46:48 <HackEgo> Done.
00:47:05 <oerjan> `slwd rdococ//s,all ,almost &,
00:47:08 <HackEgo> rdococ//rdococ is apparently from Budapest, but he is actually on Mars. Thanks to boily he is approaching permanent boredom & mapoledom. Additionally, almost all of his wisdom entries are bad.
00:47:26 <oerjan> i recall at least one that had potential.
00:50:14 <oerjan> `? overflow
00:50:16 <HackEgo> Overflow is a phenomenon that occurs when too much water pours into the inner tanks of a hydraulic computer.
00:50:23 <oerjan> this one, although i improved the wording.
00:50:43 <boily> oerjan: yes, I'm missing the unary. the PDF isn't exactly up to date >_>'...
00:51:53 <oerjan> shocking
00:55:36 <oerjan> shachaf: but today's entries were bad even by his standards.
00:55:49 <shachaf> Yes.
01:11:34 -!- augur has joined.
01:14:15 -!- augur has quit (Remote host closed the connection).
01:14:28 -!- augur has joined.
01:16:22 -!- HackEgo has quit (Read error: Connection reset by peer).
01:16:52 -!- HackEgo has joined.
01:24:48 <int-e> `? thought
01:25:03 <HackEgo> ​. o O ( Why are they asking me what a thought is? )
01:25:43 <int-e> `cwlprits thought
01:25:51 <int-e> r.dococ, o.erjan?
01:25:52 <HackEgo> oerjän rdocöc
01:26:08 <int-e> thought so
01:26:26 <oerjan> ah that one wasn't so bad either
01:26:53 <oerjan> `dowg thought
01:27:00 <HackEgo> 10764:2017-04-18 <oerjän> slwd thought//s,for ,, \ 10716:2017-04-16 <rdocöc> le//rn thought//. o O ( Why are they asking me for what a thought is? )
01:28:02 <boily> `? wisdom
01:28:03 <HackEgo> wisdom is always factually accurate, except for this entry, and, uh, that other one? It started with, like, an ø?
01:28:08 <boily> `wisdom
01:28:10 <HackEgo> metasepia//metasepia knew the weather at your nearest airport, and also something about ducks.
01:28:48 <int-e> @metar lowi
01:28:48 <lambdabot> LOWI 230020Z AUTO 08006KT 050V130 9999 -RA FEW015 BKN026 05/03 Q1020
01:28:57 <shachaf> @metar koak
01:28:58 <lambdabot> KOAK 222353Z 28019KT 10SM FEW012 FEW032 SCT070 OVC220 18/13 A3000 RMK AO2 SLP160 T01780128 10194 20178 56014
01:29:16 <int-e> . o O ( is that the time? ;-) )
01:29:47 <oerjan> int-e: what?
01:30:08 <int-e> oerjan: well it says it's 00:20 GMT.
01:30:25 <int-e> (or was, when that entry was made)
01:30:40 <oerjan> so 8 minutes old, then.
01:30:53 <int-e> yeah, surprising...
01:31:14 <oerjan> it was bound to happen eventually.
01:31:49 <int-e> actually that 23:53 seems a bit stranger
01:32:16 <int-e> `icao KOAK
01:32:17 <HackEgo> Metropolitan Oakland Intl (OAK, KOAK)
01:32:38 <boily> depends on the airfield, really. METAR are “usually” on the hour, with SPECI inbetween as needed.
01:32:41 <boily> @metar CYUL
01:32:42 <lambdabot> CYUL 230000Z 31005KT 30SM SCT040 BKN052 09/02 A3001 RMK SC3SC3 SLP164
01:34:42 <int-e> `? metar
01:34:43 <HackEgo> metar is a service Taneb invented that allows nerds to talk about the weather.
01:35:04 <int-e> `cwlprits metar
01:35:11 <HackEgo> shachäf oerjän
01:35:54 -!- Phantom_Hoover has quit (Quit: Leaving).
01:42:00 * Zarutian reads an adpt quote on the 'Net: „The job of a soldier is to die for his country“ -unknown.
01:47:00 -!- dingbat has joined.
01:51:15 <boily> `relcome dingbat
01:51:16 <HackEgo> dingbat: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
01:51:34 <dingbat> holy batman everything is rainbows!
01:51:48 <dingbat> to what do I owe this flamboyant greeting?
01:52:06 <boily> newcomers to this fine channel are always welcomed.
01:52:16 <boily> (`relcomed if I happen to be here. mwah ah ah.)
01:55:45 <shachaf> dingbat is hardly a newcomer
01:56:41 <shachaf> flamboyant
01:59:44 <boily> oh hm. eh.
01:59:59 <boily> knew him all way back. long time ago. la la la <_<... >_>...
02:04:54 <oerjan> `learn dingbat is a famous font designer for Microsoft.
02:04:56 <HackEgo> Learned 'dingbat': dingbat is a famous font designer for Microsoft.
02:05:32 <shachaf> are you sure you're not confusing dingbat with dingbatman
02:06:15 <oerjan> nah. nah nah nah nah nah nah nah.
02:06:48 <shachaf> Do you actually know that from the Batman music or just from people talking about the Batman music on the Internet?
02:12:48 <oerjan> >_>'...
02:13:19 * oerjan should maybe listen to it sometime.
02:16:15 <oerjan> hm that sounds to me like da da da not na na na
02:21:49 <boily> na na na na na na na katamari damacy ♪
02:26:26 <shachaf> I asked because I'd never listened to it before.
02:26:48 <oerjan> me neither! at least that i can recall
02:27:50 <oerjan> `? bananaphone
02:27:51 <HackEgo> bananaphone? ¯\(°​_o)/¯
02:33:10 <dingbat> i don't like bananas, therefore bananaphones are similarly icky
02:34:35 <boily> bell peppers were declared scow, and now bananas? that's horrible!
02:34:57 <oerjan> bananas are good, as long as they are just the right ripeness.
02:35:16 <oerjan> aka for about 5 minutes.
02:36:19 <boily> as long as there is no green showing, they're delicious.
02:36:37 <boily> avocadoes, on the other hand...
02:37:18 * oerjan guacks boily with a mole ~~~(===)o
02:37:56 <shachaf> oerjan: Plantains are good at many levels of ripeness.
02:38:00 <shachaf> From green to black.
02:38:09 <shachaf> I cooked three green plantains today.
02:38:19 <oerjan> OKAY
02:38:30 <shachaf> Do you like plantains?
02:38:33 -!- MoALTz has quit (Quit: Leaving).
02:39:58 <shachaf> fizzie: Hmm, did you get a sword after fighting your snake?
02:41:44 * boily uses a tortilla shield to protect himself from the... what the hell is that flying thing?
02:41:52 <oerjan> i may not have tasted plantains. norwegian wikipedia says they have essentially nothing in common with ordinary bananas other than the shape.
02:42:18 <shachaf> I think when they're ripe they have a bananish flavor.
02:42:21 <shachaf> But now I'm not sure.
02:42:36 <shachaf> English Wikipedia says there's nothing that distinguishes them from ordinary bananas.
02:42:52 <shachaf> "The term "plantain" is loosely applied to any banana cultivar that is eaten when cooked. However, there is no formal botanical distinction between bananas and plantains. Cooking is also a matter of custom, rather than necessity."
02:44:10 <shachaf> Google translates the Norwegian Wikipedia text to "Plantain have quite different properties than usual banana , and it can be more considered a vegetable than fruit , as it, among other things can not be eaten raw."
02:44:14 -!- orby has joined.
02:44:19 <shachaf> English Wikipedia says "Ripe plantains can be eaten raw, since the starches are converted to sugars as they ripen."
02:44:40 <orby> greetings!
02:44:44 <boily> hellorby!
02:44:53 <shachaf> good afternorby
02:45:32 <boily> fried plantain is delicious, along with pilaf and oxtail stew.
02:45:44 <orby> mmmm plantains are indeed delicious
02:46:37 <shachaf> Now I made mashed plantains with fried halloumi.
02:46:48 <orby> ooo, what's halloumi?
02:47:02 <shachaf> A squeaky cheese.
02:47:14 <orby> what does it taste like?
02:47:26 <shachaf> Like halloumi.
02:47:30 <orby> :)
02:47:50 <shachaf> It's white, firm, and is often grilled.
02:48:07 <orby> how does one fry it? is it typically breaded? or placed on bread?
02:48:23 <shachaf> One can fry it all sorts of ways.
02:48:35 <shachaf> It has a high melting point so it doesn't melt.
02:48:50 <orby> I see, I don't think I've ever dealt with a cheese with a high melting point.
02:49:22 <orby> I have a terrible habit of using commas where I should use periods,
02:49:34 <boily> halloumi and havarti are the perfect cheeses for râclette.
02:49:41 <shachaf> Well, you should try some halloumi.
02:49:52 <orby> I'll have to try it. I love trying new things :)
02:50:04 <orby> What is râclette?
02:50:22 <shachaf> When you bite halloumi, it squeaks against your teeth.
02:50:42 <orby> That doesn't sound very pleasant...
02:51:24 <oerjan> "Halloumi is set with rennet"
02:51:46 <boily> https://en.wikipedia.org/wiki/Raclette
02:52:00 <shachaf> oerjan: Non-animal rennet in this case.
02:52:01 <boily> you know your poutine is true if the cheese squeaks.
02:52:37 <boily> orby: forget the ^. that's my accent slipping.
02:53:03 <orby> Gotcha, sounds lovely
02:54:30 <orby> rennet is one of those tricky things for us vegetarians that I most often ignore but secretly feel guilty about ignoring
02:54:46 <orby> but I'm too lazy to be vegan :)
02:55:25 <boily> halloumi is also quite good in palak paneer :D
02:55:38 <orby> yummy
02:57:03 <oerjan> * [...] what the hell is that flying thing? <-- a mole, i said. they're somewhat competing with the moons for my lawn.
02:58:18 <shachaf> a mole of what?
02:59:34 <boily> oerjan: ah! that kind of mole!
02:59:58 <oerjan> shachaf: a mole of guacks
03:03:15 -!- sleffy has joined.
03:03:44 <orby> are there any functional languages on the wiki that deal only with boolean values that anyone knows about?
03:04:10 <orby> I was thinking today about a functional language whose only operator is nand
03:05:02 <shachaf> Is it true that no property of computable reals is decidable?
03:05:59 <orby> wouldn't the decidability of properties of computable reals be a property of computable reals?
03:06:16 -!- augur has quit (Remote host closed the connection).
03:06:39 <shachaf> OK, no nontrivial property.
03:07:12 <orby> I do not know. I suppose it depends upon how you define nontrivial. Oerjan is probably a good person to ask. Oerjan is smart.
03:07:26 * oerjan waves
03:07:50 <oerjan> we have several languages with nand in the name but i'm not sure if any of them are functional.
03:07:54 <shachaf> In the same sense as Rice's theorem -- a property is trivial if it's true for all computable reals or false for all of them.
03:08:01 <oerjan> might depend on your definition.
03:08:01 -!- augur has joined.
03:08:19 <shachaf> Are concatenative languages functional?
03:08:39 <orby> I do not know what a concatenative language is
03:08:41 <oerjan> good question.
03:08:53 <oerjan> orby: underload is one.
03:09:51 <orby> I see
03:10:34 <oerjan> and although it's standard definition uses stacks, you can also think of it as a rewriting system.
03:10:38 <oerjan> *its
03:10:54 <orby> cool :)
03:14:49 -!- boily has quit (Quit: FOREWORD CHICKEN).
03:14:57 <orby> I was thinking, a functional language that only contains nand as an operator could define its functions with 3 tokens: a b c where a is the name of the function and it's return value is "b nand c" where b and c are function calls. If you wanted to get fancy you could do partial evaluation and first class functions but I don't think it's necessary.
03:15:25 <oerjan> shachaf: ok, if a property of reals is nontrivial, then by applying the least upper bound property you can find a real that has no open neighborhood that doesn't intersect both sets, which would imply what you want if it were computable... but i'm not sure it must be.
03:15:59 <oerjan> (both sets being the ones that have the property and those that don't.)
03:16:02 <shachaf> oerjan: If "decidable" means "clopen", then no property of the reals is decidable with the standard topology.
03:16:52 <orby> are computable reals dense in the reals?
03:16:59 <oerjan> orby: yes.
03:17:01 <shachaf> Yes.
03:17:01 <orby> I suppose they have to be since rationals are
03:17:38 <orby> neato
03:18:09 <oerjan> shachaf: there are sets that are clopen in the relative topology of the computable reals, but they're probably then undecidable for other reasons.
03:18:33 <oerjan> (e.g. "is this number > omega")
03:21:12 -!- sleffy has quit (Ping timeout: 260 seconds).
03:21:34 <shachaf> omega?
03:22:08 -!- augur has quit (Remote host closed the connection).
03:22:16 <oerjan> orby: your 3 tokens seem to be functionally defining a circuit of nand gates, then. you're going to need some initial variables too.
03:22:18 -!- sleffy has joined.
03:22:55 <oerjan> shachaf: chaitin's omega, wasn't it?
03:23:17 <shachaf> Oh, that omega.
03:23:46 <orby> oerjan: yes, that's what I'm thinking. What do you mean by initial variables? Like the ability to define f(x, y) := x nand y?
03:24:23 <oerjan> shachaf: hm can't you take your decision algorithm and turn it around into a search for an element at the boundary of where it applies...
03:24:44 <oerjan> orby: yeah
03:25:11 <orby> Yeah, I was imagining something like:
03:25:19 <orby> and
03:25:19 <orby> nand(x, y) x y
03:25:20 <orby> and(x, y) nand(x, y) nand(x, y).
03:25:25 <orby> etc.
03:25:51 <orby> but I'm still searching for a more elegant way to define the relationships between the functions because I think it can be written more simply
03:26:55 <zzo38> Oops, there are some thing missing in GURPS. Such as, if you want your familar's wounds to affect you too but not other way around (it says how to do it both ways, and how to do it so that your wounds affect your familiar only, but it doesn't say how to do if your familiar's wounds affect you only).
03:29:41 <oerjan> shachaf: hm i think you can do a bisection search, if you start with two computable reals that have different answers.
03:30:19 <oerjan> that will give you a new computable real in the limit of both sets.
03:31:27 <oerjan> and then it cannot halt for that real because then there would be a neighborhood where it also gave the same answer.
03:31:37 <oerjan> Q.E.D.
03:32:10 <oerjan> s/it/the decision algorithm/
03:34:48 <oerjan> orby: well you could leave out the variables if all the functions in the definition took the same list
03:34:59 -!- sleffy has quit (Ping timeout: 240 seconds).
03:35:01 <oerjan> but that's not good for reuse.
03:35:26 -!- sleffy has joined.
03:35:38 <orby> oerjan: reuse is for sissies :)
03:35:52 <oerjan> or you could identify them by index, then you can drop them on the result.
03:36:46 <oerjan> perhaps combine those, so the default is to have the same list
03:36:57 <orby> hmmm, well, what is really essential here? I think it's necessary that we be able to support different arities
03:37:22 <orby> would including first class functions make this simpler in any way?
03:37:37 <orby> or currying?
03:37:55 <oerjan> not simpler
03:38:09 <oerjan> perhaps more concise
03:38:18 <orby> yeah, concise is a better word
03:38:23 <oerjan> and nand nand
03:38:48 <oerjan> or wait
03:38:56 <oerjan> yes.
03:38:59 <orby> but how would we know that's not and(a, b, c, d) nand(a, b) nand(c, d) instead of and(a, b) nand(a, b) nand(a, b)
03:39:38 <oerjan> orby: because by default, that's equivalent to and(1,2,3,...) nand(1,2,3,...) nand(1,2,3,...)
03:39:50 <oerjan> and nand only uses its first two arguments
03:40:15 <orby> I see what you're saying
03:40:18 <oerjan> i.e. make them all have infinite arguments, just don't use them.
03:40:25 <orby> right right
03:40:36 <orby> hmmm interesting
03:41:39 <oerjan> or nand(1,1) nand(2,2)
03:41:51 <orby> exactly
03:42:05 <orby> do you think that is enough for turing completeness?
03:42:11 <oerjan> not nand(1,1) nand(1,1)
03:42:12 <orby> w/o fcf?
03:42:20 <orby> not 1 1
03:42:23 <oerjan> no. you're not going to get infinite memory.
03:42:39 <oerjan> *unbounded
03:42:51 <oerjan> it's enough for boolean completeness.
03:43:36 <oerjan> hm not 1 1 wasn't a syntax i was considering, but i guess it works
03:44:05 <oerjan> oh of course nand(1,1) was wrong.
03:44:20 <orby> f f(1) g(2)
03:44:34 <orby> err, f f(1, 2) g(2)
03:44:35 <oerjan> id nand(1,1) nand(1,1)
03:44:41 <orby> yeah
03:44:52 <orby> f f g(3)
03:44:53 <orby> there we go
03:45:41 <orby> resolving loops would be interesting
03:45:53 <orby> from an interpreters point of view
03:46:14 <oerjan> could give a paradox.
03:46:39 <oerjan> if the circuit is time-dependent, it's no longer functional...
03:47:11 <orby> I don't understand how that introduces time dependency
03:47:51 <orby> wouldn't it just be an infinite expression tree?
03:47:57 <oerjan> well it's either time dependency or potential paradox.
03:48:03 <oerjan> oh
03:48:04 <oerjan> ic
03:48:20 <oerjan> you're not identifying any nodes...
03:48:30 <oerjan> that might give nondeterminism instead.
03:48:40 <orby> I do not know
03:48:48 <orby> I haven't thought about it in depth
03:49:26 <oerjan> no wait it doesn't create an infinite number of nodes.
03:49:42 <oerjan> or...
03:49:49 <oerjan> argh
03:50:18 <oerjan> f f(1,2) g(2) means f(x,y) = nand(f(x,y),g(y))
03:50:50 <orby> so if f f g(3), then f(true, true, false) := (((f(true, true, false) nand g(false)) nand g(false)) nand g(false))...
03:50:52 <oerjan> that's a paradox if g(y) is true.
03:51:14 <orby> I don't think so, because each nand alternates
03:51:28 <orby> and g(y) is either true or false
03:51:39 <orby> so one of them trips a nand
03:51:51 <orby> or maybe I'm just confusing myself
03:52:15 <zzo38> What is the probability distribution of the difference of two independent uniform random variables with different ranges?
03:52:21 * orby is thinking
03:52:28 <oerjan> if you don't consider the inner f(x,y) to give the same result, then you have nondeterminism.
03:53:44 <zzo38> (And what is the way to figure it?)
03:54:53 <orby> yeah, I think you're right
03:55:57 <orby> but isn't that just the equivalent of an infinite loop?
03:56:01 <oerjan> zzo38: you could draw a rectangle representing the ranges of each, then diagonal lines where the subtraction is constant, then the probability of a difference should be the length of the intersection.
03:56:17 -!- augur has joined.
03:56:37 <oerjan> that looks like it would be a piecewise linear thing.
03:56:47 <oerjan> or wait
03:56:59 <oerjan> yes.
03:57:29 <oerjan> *proportional to the length.
03:57:35 <zzo38> I intend the equation rather than the graph, but OK
03:57:48 <oerjan> well i'm too lazy to find the equation.
03:58:37 <zzo38> What is the method of figuring out the equation?
03:59:02 <oerjan> geometry?
04:01:11 <oerjan> orby: it's an infinite loop into the past, yeah
04:01:31 <orby> hmm, consider f 1 g, g 1 f, f(true) := (true NAND g(true)) = (true NAND (true NAND f(true))
04:01:56 <orby> if we were using a reversible gate rather than NAND, then it'd be possible to isolate the f's
04:02:36 <orby> but it would be much less concise :(
04:09:01 <orby> oerjan: what if we introduced a third truth value for undeterminable
04:09:56 <oerjan> zzo38: oh. subtracting is the same as adding after negating the range of the second variable.
04:10:01 <orby> so, in the case above, f(true) = undeterminable, f(false) = true
04:12:24 <orby> the problem of deciding whether or not a function is determinable is probably undecidable :(
04:12:29 <zzo38> oerjan: Yes, it is that. (I am still not quite sure how to figure it?)
04:12:38 <zzo38> (But I did realize that already)
04:15:55 <oerjan> oh hm i'm thinking wrong about the scaling factor
04:17:31 <oerjan> ok when adding ranges [0,a] and [0,b] where b >=a, i think the distribution function is x, 0 <= x <= a; sqrt(2), a <= x <= b; a+b-x, b <= x <= a+b
04:18:45 <oerjan> probability density function, that is.
04:18:50 <oerjan> er
04:19:42 <oerjan> make that sqrt(2) into 1, maybe.
04:19:54 <oerjan> (it was left over after i fixed the scaling for the rest)
04:20:57 <oerjan> zzo38: ^
04:21:07 <zzo38> I did think of setting the ranges to start at zero, actually, so I suppose it can help. Because, then you just have one more constant so, is more easily.
04:21:48 <zzo38> But then, I would need the cdf rather than the pdf. Can that be figured by the antiderivative?
04:21:58 <oerjan> yeah
04:22:06 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...).
04:22:11 <oerjan> x^2/2 for the first branch
04:22:38 <oerjan> 1-(a+b-x)^2/2 for the last one, i should think
04:23:03 <oerjan> (by symmetry)
04:23:49 <zzo38> OK
04:25:05 <orby> What if we allowed first class functions and used explicit function evaluation, so f f 1 would be ((f(x))(y))(z) := (((f nand x) nand y) nand z), wouldn't that allow for the equivalent of unbounded memory access?
04:28:14 <oerjan> oh wait i'm still messing up the scaling.
04:30:23 <oerjan> a*x^2/(2*b), 1 - (a+b-x)^2/(2*a*b)
04:36:17 <oerjan> wait wat
04:36:23 <oerjan> x^2/(2*a*b)
04:39:37 -!- Zarutian has quit (Ping timeout: 240 seconds).
04:45:20 <orby> I think that makes more sense with tail recursion, so f 1 f would be (f(x))(y) ... := (x nand (y nand f)) ... then f would consume an infinite number of values and would halt and return 1 iff one of those values was 0
04:47:14 <orby> no that's not exactly right, it would return the parity of the position of the first 0
04:47:51 <oerjan> zzo38: x^2/(2*a*b) for x <= a; a/(2*b) + (x - a)/b for a <= x <= b; 1 - (a+b-x)^2/(2*a*b) for b <= x <= a+b
04:48:50 <oerjan> um the middle one is also x/b - a/(2*b)
04:49:41 <oerjan> and that seems to fit together at least.
05:04:51 <zzo38> OK
05:37:16 <rdococ> hbv
06:10:36 <shachaf> Cale: So if you want to put "Foo a" in a data type, you have three options: data T = T (forall a. Foo a); data T = forall a. T (Foo a); data T a = T (Foo a)
06:11:12 <shachaf> What if you have a constraint? You can write data T = T (forall a. K a => Foo a); data T = forall a. K a => T (Foo a)
06:11:22 <shachaf> Is there an equivalent for the parameterized version?
06:13:10 -!- dingbat has quit (Quit: Connection closed for inactivity).
06:15:45 <\oren\> Apparently literally every empire is denouncing Egypt
06:16:53 <oerjan> @let data T a = forall b. (b ~ a, Ord a) => T (Maybe a)
06:16:55 <lambdabot> Defined.
06:17:04 <oerjan> :t T
06:17:05 <lambdabot> Ord a => Maybe a -> T a
06:18:25 <oerjan> @let data U a = Ord a => T (Maybe a)
06:18:26 <lambdabot> .L.hs:193:12: error:
06:18:26 <lambdabot> Multiple declarations of ‘T’
06:18:26 <lambdabot> Declared at: .L.hs:191:12
06:18:32 <oerjan> @let data U a = Ord a => U (Maybe a)
06:18:34 <lambdabot> Defined.
06:18:44 <oerjan> :t U
06:18:45 <lambdabot> Ord a => Maybe a -> U a
06:18:50 <oerjan> seems equivalent, hm
06:19:19 <oerjan> shachaf: anything wrong with that?
06:19:27 <shachaf> With what?
06:19:32 <shachaf> Oh, I see.
06:19:41 <shachaf> You could also write data U a = U (Ord a => Maybe a)
06:19:55 <shachaf> One is "existential", the other is "universal".
06:20:25 <shachaf> But neither is a "parameter"
06:20:31 <shachaf> Whatever that would mean. Maybe it's meaningless.
06:20:33 <oerjan> how so?
06:20:46 <shachaf> I mean that one is a tuple and the other is a function.
06:21:40 <shachaf> Your U a = (Ord a *> Maybe a)
06:22:48 <oerjan> i have no idea what you're asking, then.
06:25:25 <shachaf> I'm not sure either.
06:26:01 <shachaf> There are three standard ways to bind a variable, and only two standard ways to constrain it.
06:26:18 <shachaf> Well, the *> version is the opposite of a constraint. Whatever that is.
06:26:31 <shachaf> An endowment.
06:28:30 <oerjan> @data Ord a => AncientEvil a => A a
06:28:30 <lambdabot> Unknown command, try @list
06:28:34 <oerjan> @let data Ord a => AncientEvil a => A a
06:28:35 <lambdabot> Parse failed: Illegal data/newtype declaration
06:28:43 <oerjan> ooops
06:28:47 <oerjan> @let data Ord a => AncientEvil a = A a
06:28:47 <lambdabot> .L.hs:195:6: error:
06:28:47 <lambdabot> Illegal datatype context (use DatatypeContexts): Ord a =>
06:29:07 <oerjan> it's so evil my fingers refuse to type it correctly
06:43:39 -!- sleffy has quit (Ping timeout: 240 seconds).
06:50:22 -!- augur has quit (Remote host closed the connection).
06:50:39 <shachaf> Yes, there's that, but that's clearly not it.
06:50:42 <shachaf> Whatever it is.
07:21:07 -!- orby has quit (Ping timeout: 260 seconds).
07:34:35 -!- augur has joined.
07:34:43 -!- augur has quit (Remote host closed the connection).
07:36:02 -!- augur has joined.
08:22:59 <shachaf> You must do X and you must do Y <-> you must do (X and Y)
08:23:14 <shachaf> You may do X and you may do Y <-> you may do (X or Y)
08:23:35 <shachaf> What's a logic context for that?
08:23:49 <shachaf> Constraints vs. freedoms.
08:24:46 <oerjan> deontic logic?
08:25:41 <shachaf> whoa, that's more specific an answer than I expected.
08:35:36 -!- augur has quit (Remote host closed the connection).
08:35:59 -!- augur has joined.
08:37:10 -!- augur has quit (Remote host closed the connection).
08:47:54 -!- xfix has quit (Read error: Connection reset by peer).
08:49:10 -!- xfix has joined.
08:49:30 -!- prooftechnique has quit (Ping timeout: 246 seconds).
08:50:12 -!- j-bot has quit (Ping timeout: 260 seconds).
08:54:34 -!- prooftechnique has joined.
09:03:00 <rdococ> hi
09:03:07 -!- Hoolootwo has quit (Ping timeout: 255 seconds).
09:05:06 <shachaf> oerjan: But you have the same situation with e.g. Haskell-style constraints.
09:05:09 -!- FireFly has quit (Ping timeout: 600 seconds).
09:05:17 -!- AnotherTest has joined.
09:05:19 <shachaf> I think there's a more general thing I'm thinking of whose name I can't remember.
09:05:59 -!- FireFly has joined.
09:07:17 <oerjan> shachaf: modal logic? the "alethic" section of that wikipedia page might also match dependent on exactly what you mean by "must" and "may".
09:07:39 <shachaf> Maybe.
10:05:18 -!- MoALTz has joined.
10:10:07 -!- oerjan has quit (Quit: Nite).
10:31:21 -!- Phantom_Hoover has joined.
10:49:25 <diginet> A modal logic programming language would be col
11:05:34 -!- LKoen has joined.
11:06:26 -!- AnotherTest has quit (Ping timeout: 260 seconds).
11:17:29 -!- AnotherTest has joined.
11:25:11 <Jafet> would you think, perhaps, that it would necessarily be cool?
11:56:33 -!- boily has joined.
12:03:26 -!- LKoen has quit (Remote host closed the connection).
12:13:31 <boily> `wisdom
12:13:33 <HackEgo> madness//madness lies thataway.
12:19:33 * rdococ pushes a number onto the stack
12:21:04 * boily observes rdococ pushing numbers on stacks
12:21:40 * rdococ writes a blank onto the tape
12:22:27 <rdococ> I've just realized why the universe is so weird at the microscopic level.
12:22:46 <rdococ> it runs on a hybrid of Entropy and Malbolge :P
12:50:54 -!- DHeadshot has joined.
13:38:38 -!- augur has joined.
13:43:21 -!- augur has quit (Ping timeout: 260 seconds).
13:51:20 -!- MoALTz has quit (Quit: Leaving).
13:54:03 -!- yorick has joined.
14:12:43 -!- MoALTz has joined.
14:33:38 -!- bender has joined.
14:34:24 -!- LKoen has joined.
14:48:06 -!- bender has quit (Quit: [rebooting]).
14:51:24 -!- bender has joined.
15:10:12 -!- DHeadshot has quit (Ping timeout: 240 seconds).
15:20:08 -!- boily has quit (Quit: YAK CHICKEN).
15:54:22 -!- Zarutian has joined.
16:37:39 -!- FreeFull has joined.
16:52:40 -!- DHeadshot has joined.
17:33:09 -!- augur has joined.
17:42:44 -!- augur_ has joined.
17:44:46 -!- erkin has joined.
17:45:06 -!- bender has quit (Ping timeout: 258 seconds).
17:46:11 -!- sleffy has joined.
17:46:22 -!- augur has quit (Ping timeout: 240 seconds).
17:46:30 -!- MoALTz_ has joined.
17:49:03 -!- contrapumpkin has joined.
17:49:42 -!- MoALTz has quit (Ping timeout: 240 seconds).
17:51:32 -!- bender has joined.
17:58:58 -!- augur has joined.
18:02:02 -!- augur_ has quit (Ping timeout: 240 seconds).
18:09:56 -!- bender has quit (Ping timeout: 260 seconds).
18:12:42 -!- augur_ has joined.
18:16:21 -!- augur has quit (Ping timeout: 260 seconds).
18:16:30 -!- augur has joined.
18:19:09 -!- MoALTz_ has changed nick to MoALTz.
18:20:08 -!- augur_ has quit (Ping timeout: 255 seconds).
18:24:52 <\oren\> when do le polls fermay in le fronsais election
18:32:30 -!- sleffy has quit (Ping timeout: 260 seconds).
18:36:04 -!- sleffy has joined.
18:40:32 -!- Phantom_Hoover has quit (Quit: Leaving).
18:53:21 <shachaf> oerjan: More generally, you have F(A and B) = F(A) and F(B) vs. F(A or B) = F(A) and F(B)
18:53:55 <shachaf> What are those called?
18:58:04 -!- augur has quit (Remote host closed the connection).
19:24:25 <quintopia> i feel like i'm letting oerjan down right now
19:24:59 -!- augur has joined.
19:25:06 <shachaf> he has that effect on people hth
19:25:33 <quintopia> sitting in a theatef for a performance of the royal shakespeare company's matilda
19:28:34 -!- Zarutian has quit (Quit: Zarutian).
19:34:13 -!- augur has quit (Remote host closed the connection).
19:46:18 -!- Zarutian has joined.
19:47:02 -!- Zarutian has quit (Read error: Connection reset by peer).
19:47:37 -!- Zarutian has joined.
19:54:07 -!- bender has joined.
20:00:11 -!- bender has quit (Ping timeout: 260 seconds).
20:00:38 -!- angrykoala has joined.
20:02:35 -!- bender has joined.
20:05:32 <\oren\> https://www.youtube.com/watch?v=De4-aF2DIiw
20:18:52 -!- Cale has quit (Remote host closed the connection).
20:19:09 -!- angrykoala has quit (Quit: Page closed).
20:21:22 -!- Cale has joined.
20:27:18 -!- DHeadshot has quit (Ping timeout: 260 seconds).
20:44:44 -!- LKoen has quit (Remote host closed the connection).
20:47:21 -!- augur has joined.
20:52:02 -!- sleffy has quit (Ping timeout: 260 seconds).
20:55:36 -!- bender has quit (Ping timeout: 260 seconds).
20:57:05 -!- sleffy has joined.
20:58:45 -!- j-bot has joined.
20:59:34 -!- Cale has quit (Remote host closed the connection).
21:33:31 -!- MoALTz has quit (Quit: Leaving).
21:57:06 -!- bender has joined.
22:02:24 -!- Kanoxbox_ has joined.
22:07:55 -!- Kanoxbox_1 has joined.
22:09:42 -!- Kanoxbox_ has quit (Ping timeout: 240 seconds).
22:12:47 -!- sebbu2 has joined.
22:14:11 -!- Kanoxbox_ has joined.
22:15:30 -!- Kanoxbox_1 has quit (Ping timeout: 240 seconds).
22:15:59 -!- sebbu has quit (Ping timeout: 240 seconds).
22:17:37 -!- Kanoxbox_ has left.
22:39:16 -!- AnotherTest has quit (Quit: ZNC - http://znc.in).
22:40:22 -!- LKoen has joined.
22:42:38 <\oren\> https://www.youtube.com/watch?v=328TJP0WDvE
22:44:52 -!- LKoen has quit (Ping timeout: 258 seconds).
22:49:19 <\oren\> https://www.youtube.com/watch?v=Va9GbB-Meok&t=220s
22:58:17 -!- bender has quit (Ping timeout: 258 seconds).
23:32:34 -!- LKoen has joined.
23:33:56 -!- augur has quit (Remote host closed the connection).
23:34:33 -!- augur has joined.
23:34:39 -!- DHeadshot has joined.
23:38:42 -!- augur has quit (Ping timeout: 240 seconds).
23:49:51 -!- Zarutian has quit (Quit: Zarutian).
23:51:37 -!- DHeadshot has quit (Ping timeout: 240 seconds).
←2017-04-22 2017-04-23 2017-04-24→ ↑2017 ↑all