00:00:01 <kmc> i think no
00:00:05 <elliott> I know for a fact you've said cocks things in #esoteric
00:00:10 <elliott> but that cocks thing in particular
00:00:53 <Fiora> Bike: it seems like the thing in this paper is that without the weak interaction you can't have core collapse supernovae, so it's way harder to get interesting elements out into the universe
00:00:54 <lexande> i was in kmc's Caltech qdb before being accepted to Caltech
00:00:55 <Bike> i hope we run into l-form aliens
00:01:17 <Bike> Fiora: hmmmmmmmm i remember some stuff about how to form carbon without the usual reactions
00:01:42 <Bike> unfortunately it was in a pop sci book i don't have
00:01:44 <Fiora> it's not about forming but about getting out of stars, I think
00:01:47 <Bike> the links were, i mean
00:02:06 <Fiora> like without the weak interaction you'd get a bunch of white dwarfs, I think? I'm not sure
00:02:27 <Fiora> I wonder how bigger stars would collapse
00:02:36 <Phantom_Hoover> the point seems to be that proton + electron -> neutron is necessary for neutronium to form
00:02:50 <Fiora> there's also the thing that neutrinos are a huge part of the supernovae process, I think
00:02:53 <Fiora> like, neutrino pressure
00:03:08 <Phantom_Hoover> i assume there'd still be gravitational collapse though?
00:03:14 <Fiora> yeah... geez. that is an interesting question
00:03:26 <Fiora> like what would happen if you had a graviationally collapsing iron core
00:05:12 <Bike> "weakless universe" sounds kinda cool though
00:05:36 <Fiora> bike wants a strong universe
00:05:47 <kmc> i wonder what security holes my 2004 era perl quote webapp had
00:06:45 <kmc> CSRF for sure
00:07:40 <shachaf> csrf is a really annoying sort of bug because you get it from not doing something, as opposed to doing something wrong
00:08:06 <shachaf> (as opposed to, say, buffer overflows, xss, etc.)
00:08:31 <shachaf> i wonder whether there are unknown classes of bugs like that that exist everywhere and no one knows about
00:08:35 <kmc> why would you want it to be secure by default, why not write a secure code for it
00:08:38 <Bike> Fiora: maybe i want a universe that isn't so hardassed about strength/weakness dichotomies!!
00:08:53 <kmc> xss is also framed as from not doing something, "not escaping"
00:09:08 <Bike> where's the mediocre force, i ask you. the "ok at friendly boxing but can't run" force
00:09:22 <Fiora> Bike: electromagnetic, right?
00:09:25 <kmc> it happens because web developers only acknowledge one type
00:10:11 <Fiora> it's the medium force
00:10:13 <Fiora> the mediocre force
00:10:27 <Bike> i thought gravity was the weakest force
00:10:38 <Bike> or protons are really light or whatever.
00:10:57 <Fiora> yeah, gravity is like 10^30 something times weaker
00:11:09 <Bike> "the kind of bullshit force, tbh"
00:11:16 <Bike> the why bother force
00:11:42 <ion> Gravity is so weak i don’t even bother to submit to it.
00:13:38 <Fiora> it's only a theory, right?
00:14:43 <oerjan> <Bike> i don't click pdfs usually <-- i'm with Bike
00:14:59 <Fiora> I-I'll try to link the arxiv pages from now on instea.d..
00:15:47 <elliott> counterpoint: I click all pdfs
00:16:29 <shachaf> counterpoint: i click links whenever Bike doesn't
00:18:16 <lexande> Fiora: weak is stronger than electromagnetic right?
00:18:40 <lexande> i thought it was like strong > weak > electromagnetic >> gravity
00:19:02 <kmc> aren't electromagnetic and weak secretly the same thing somehow
00:19:03 <Fiora> is it? I can never remember >_<
00:19:07 <Fiora> I thought weak was less
00:19:40 <Fiora> wikipedia says strong=10^38
00:19:44 <Fiora> electromangetic 10^36
00:20:03 <shachaf> that's a p. big difference
00:20:03 <elliott> rename gravity superweak force imo
00:20:07 <Fiora> https://en.wikipedia.org/wiki/Fundamental_interaction
00:22:58 <Fiora> but gravity makes event horizons :<
00:23:01 <Phantom_Hoover> quantum physicists just try to put it down because they can't really work it out
00:23:23 <shachaf> gravity more like depravity
00:23:28 <shachaf> the joke is that gravity is bad
00:24:20 <oerjan> `addquote <elliott> you know, when people talk about emacs being an OS I doubt what they had in mind was that it needed a package manager
00:24:24 <HackEgo> 1064) <elliott> you know, when people talk about emacs being an OS I doubt what they had in mind was that it needed a package manager
00:29:48 <kmc> yay rust has or-patterns
00:30:48 <kmc> patterns that match either of two subpatterns
00:31:31 <shachaf> What happens when they bind variables?
00:31:42 <kmc> they have to bind the same set of variables at the same types, I think
00:33:37 <kmc> i'm reading the rust tutorial and also building rust
00:34:12 <elliott> maybe I asked that already
00:34:31 <shachaf> elliott: the tutorial is p. simple
00:34:41 <shachaf> kmc: I like how they're going to take "for" out of the language.
00:34:49 <shachaf> (And then put it back in with a different, more reasonable behavior.)
00:34:59 <kmc> i like that too, then, I guess?
00:35:15 <shachaf> The point is that it's not all that stable yet.
00:35:32 <kmc> my first job will be to rewrite all the for loops in Servo, I'm sure
00:36:05 <shachaf> I hear Option<T> is actually represented as a potentially-null pointer at runtime.
00:36:13 <kmc> i wonder why it has such curly-bracy, non-layout syntax. if it's what they really want or if it's some "people will be scared" thing
00:36:15 <shachaf> I don't know how Option<Option<T>> is represented.
00:36:31 <shachaf> You know how in C you can do things like foo(T *x) { if (x == NULL) return ...; ...; }, without introducing an extra level of nesting?
00:36:41 <shachaf> Is there a nice pattern-matchy of doing that safely?
00:37:12 <kmc> elaborate?
00:38:01 <shachaf> If you were matching on Maybe, you would say fn foo(x: Maybe<x>) { match x { Nothing => ...; Just(y) => ... } }
00:38:14 <elliott> kmc: yeah rust's syntax seems erally ugly to me
00:38:17 <shachaf> And everything in the Just case is nested an extra level -- which probably means your entire function.
00:38:18 <elliott> on a purely aesthetic level
00:39:06 -!- Nisstyre-laptop has joined.
00:39:43 <shachaf> "You're invited to Human API Hackathon (Jul 6, 2013 - Jul 7, 2013)"
00:40:18 <kmc> one day they'll hack that thon for good
00:40:41 <shachaf> will rust have rank-2 types.....
00:40:57 <shachaf> They have type-class-ish things which you can also use as a type and then they become existential.
00:40:58 -!- Bike_ has joined.
00:41:46 -!- sprocklem has joined.
00:41:49 <shachaf> does rust have polymorphic recursion.....i bet the answer is no
00:42:00 <shachaf> does rust support constructor classes......
00:42:31 -!- Bike has quit (Ping timeout: 264 seconds).
00:42:34 <shachaf> kmc: I found the distinction between one-variant enums and structs kind of odd.
00:42:35 <kmc> i think no
00:42:42 <kmc> I was just going to remark on that
00:42:48 -!- Bike_ has changed nick to Bike.
00:42:52 <shachaf> I guess it's because structs guarantee memory compatibility with C structs.
00:43:03 <shachaf> So I wonder whether it's better to use a one-variant enum when you don't care about that.
00:43:23 <shachaf> Or maybe you can get them to merge the two!
00:44:08 <kmc> also it doesn't infer function arg / return types??
00:44:43 <kmc> well for top level 'fn'
00:45:01 <kmc> it does infer them on lambdas, so I guess this amounts to enforcing a rule that GHC warns about anyway
00:45:31 <shachaf> With GHC it's still sometimes nice to write a function and then ask for its type.
00:45:39 <shachaf> Though it's not all that common.
00:45:48 <shachaf> rusti doesn't support :t :'(
00:46:29 <shachaf> The semicolon thing is kind of weird.
00:46:42 <shachaf> You can say { ...; x } or { ...; return x; } but not { ...; x; }
00:47:02 <shachaf> Seems like a very easy thing to accidentally write or forget a semicolon.
00:47:10 <Bike> I guess x last isn't a statement, in the same waY?
00:47:15 <shachaf> I guess the typechecker would catch most of those kinds of bugs, though.
00:47:16 <kmc> you can say the latter and it gives you a function returning () right?
00:51:09 <Bike> do you get a warning for a spurious statement?
00:54:52 <elliott> imo kmc should turn rust into haskell.
00:55:09 <kmc> haskel über alles
00:55:18 <kmc> did not care enough to fix typo, hth
00:55:18 <shachaf> rust is already k. haskell
00:55:39 <shachaf> people say "foo is haskell-inspired" a lot when they mean something like list comprehensions
00:55:51 <shachaf> but rust has more significant similarities than that
00:55:56 <kmc> Haskell is the cool language to know and be inspired by and never use
00:55:58 <shachaf> of course maybe they're similarities to ocaml or whatever it is
00:56:09 <kmc> but yeah I think rust is more substantial than that
00:56:12 <Bike> some language that ends with an l
00:56:26 <kmc> Go's interfaces whatever are supposed to be "haskell like" but the language doesn't even have polymorphism
00:56:35 <elliott> I really doubt any part of Go is explicitly inspired by haskell
00:56:35 <kmc> `quote haskell-like
00:56:37 <HackEgo> 870) <kmc> i'm looking for a haskell-like programming language, meaning that it supports nesting multi-line comments
00:56:41 <Phantom_Hoover> kmc, do you... have something against being inspired by haskell but not using it?
00:56:51 <kmc> Phantom_Hoover: not really
00:56:52 <Bike> read the cconversation man
00:57:04 <kmc> i mean it's what i do
00:57:07 <kmc> for the most part
00:57:57 <Bike> a complaint is with languages saying they're haskell-inspired when it's something boringer than inference and type constructors and stuff
00:58:43 <Bike> he does that's true
00:58:51 <kmc> yes I'm bitter and stuff
00:58:56 <kmc> and PH is annoyed by it
00:59:11 <shachaf> kmc: pigworker pointed out that type classes are a kind of program-inference-from-types, rather than type-inference-from-programs
00:59:19 <Bike> i'll be really happy when i get into A Field and can feel dumb and behind the times about that instead of wih CS
00:59:30 <kmc> shachaf: that's cool
00:59:39 <elliott> Bike: I hear you're a biomathematician.........
00:59:53 <Bike> come at me bro
01:00:27 <Bike> oh i read one of that guy's books
01:00:30 <Bike> ..................on biology
01:01:59 <Bike> ooh oscillators
01:02:07 <kmc> going to get on this plane soon
01:02:14 <ion> Look out for the snakes.
01:02:21 <kmc> afk (maybe back once I'm on the plane?)
01:02:25 <Bike> "A group-theoretic approach to rings of coupled biological oscillators." well then
01:02:51 <Bike> hmmmmmmmmmm did i read one of these papers, lessee
01:02:53 <Phantom_Hoover> although he did it on insects so he also has a lot of those on his walls
01:03:06 <Bike> insects are animals maaaaan
01:03:26 <Phantom_Hoover> yes, he did it on them specifically rather than animals in geneal
01:03:52 <Bike> aww, my book on neuroethological robotics doesn't have any of these
01:03:57 <Bike> clearly a new anthology is called for
01:09:54 <elliott> kmc: planes shouldn't ahve internet
01:11:13 <Bike> elliott: voice gregor.
01:11:22 -!- ChanServ has set channel mode: +v Gregor.
01:11:36 <Bike> elliott how can you fail your constituency like that!
01:11:42 <elliott> oerjan: does 2 mean you op me instead
01:11:56 <elliott> btw have you noticed ais523 left for good
01:12:00 <ion> No, he’ll nop you instead.
01:12:02 <oerjan> elliott: it would if shachaf had said "op" instead of "nop"
01:12:24 <elliott> an advantage of opping me is that i'm already in the access list
01:12:26 <elliott> less work to just modify it
01:12:28 <ion> You haven’t nopped him yet, though.
01:12:39 <Bike> hasn't he, ion? hasn't he?
01:12:47 <shachaf> oerjan: the advantage of opping me is that i'm p. groovy
01:13:04 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
01:13:10 <ion> Oh, that kind of nop.
01:13:13 <ion> Fair enough.
01:13:45 <Sgeo> I want to buy more memory for my work computer :/
01:13:47 <HackEgo> 2013-06-21 04:13:29: <ais523> yeah, me not knowing how they work is a problem for working out ways to program with them, though
01:14:04 <HackEgo> not lately; try `seen ais523_ ever
01:14:20 <oerjan> elliott: hm it's been a while
01:14:43 <Bike> his worldview was inadequate, obviously
01:14:57 <Bike> just couldn't take the full force of Bike
01:15:07 <elliott> oerjan: iirc the logs were down when he /parted forever, though.
01:16:08 <shachaf> the logs that is, the logs that isn't, and the logs that may or may not be
01:16:42 <oerjan> shachaf: so are you made of vinyl
01:19:46 -!- Bike_ has joined.
01:21:11 <kmc> elliott: this plane doesn't have internet, I'm just tethering while I'm still on the ground
01:21:41 <kmc> you're really sad
01:21:44 <kmc> (not really)
01:21:49 -!- Bike has quit (Ping timeout: 246 seconds).
01:21:56 <Bike_> can you send internet through flight radar
01:21:59 -!- Bike_ has changed nick to Bike.
01:22:01 <kmc> i built rust 0.6 and i'm going to write some rust 0.6 code during this flight
01:22:11 <kmc> I assume my knowledge will be woefully out of date by the time i land
01:22:12 <Bike> i'm pretty sure you should find an exploit in the plane software while you're in the hair
01:22:23 <Bike> do some movie shit
01:22:27 <Bike> redirect to the bahamas
01:23:30 <Fiora> so like, by the time you land
01:23:34 <Fiora> your knowledge will be a bit rusty?
01:23:41 <Bike> no shut up nooooo
01:23:58 -!- SirCmpwn has quit (Quit: ZNC - http://znc.in).
01:24:11 <kmc> Fiora: -____-
01:24:22 <Bike> glad you got that in before you hit the air
01:24:55 <kmc> hit the air running
01:25:01 <elliott> i like the idea that kmc is learning rust on the flight in an emergency before the interview
01:25:12 <elliott> like "oh shit, I don't actually know any rust"
01:25:21 <kmc> yeah that's basically the case
01:25:22 <Fiora> is the process of learning rust "oxidizing"?
01:25:24 <kmc> except s/interview/job/
01:25:25 <Fiora> kmc is oxidizing on his flight
01:25:29 -!- SirCmpwn has joined.
01:25:36 <kmc> fair point
01:25:38 <elliott> job = really long interview that you get paid for
01:25:41 <kmc> in an at will employment state
01:26:05 <kmc> yeah some companies only hire through internship / contract work
01:26:13 <kmc> which is a long interview that you get paid for
01:27:53 <Bike> truly, isn't life an interview, in the large
01:28:27 <HackEgo> 372) <Phantom_Hoover> oerjan, little do you realise that everything you say and do is part of that great monad tutorial we call life.
01:28:56 <Fiora> life is an interview for applying to madoka's^W heaven?
01:29:18 <Bike> kmc i'm not sure you get the c.c thing
01:29:18 <Sgeo> Who was that person who didn't watch PMMM yet
01:29:27 <kmc> PMMMMMMMMMMMMMMM
01:29:52 <kmc> I guess it's time for laptop to sleep now
01:29:56 <kmc> see you all later
01:30:04 <Bike> have fun a billion feet up
01:33:35 <HackEgo> Fiora: 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.)
01:33:50 <Bike> `pastelogs come Fiora
01:33:59 <elliott> no shachaf.... remember what happened the last time we `*elcomed Fiora!!
01:34:09 <shachaf> I don't think that'll find WeLcOmE or WELCOME or all those things.
01:34:20 <shachaf> elliott: no...........what happened
01:34:26 <Bike> fuck the18:19 pleez
01:34:29 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.10777
01:35:17 <shachaf> Fiora: elliott said "hi kmc" and you said "hi elliott !" so the joke was that you were kmc.
01:35:41 <Bike> `run welcome shachaf | tr 'a-zA-Z' 'n-za-mN-ZA-M'
01:35:43 <HackEgo> funpuns: Jrypbzr gb gur vagreangvbany uho sbe rfbgrevp cebtenzzvat ynathntr qrfvta naq qrcyblzrag! Sbe zber vasbezngvba, purpx bhg bhe jvxv: uggc://rfbynatf.bet/jvxv/Znva_Cntr. (Sbe gur bgure xvaq bs rfbgrevpn, gel #rfbgrevp ba vep.qny.arg.)
01:36:03 <shachaf> elliott: please arrange for uggc://rfbynatf.bet/jvxv/Znva_Cntr to be a valid url
01:36:13 <shachaf> invent a new protocol if you have to
01:36:17 <Fiora> shachaf: oh, sorry
01:36:31 <Fiora> um.... for being confusing!
01:36:59 <shachaf> I think *I* was the confusing one here...
01:37:12 <shachaf> You should be mad at me for not apologizing.
01:37:42 <Fiora> ...? why would I be...
01:38:21 <oerjan> shachaf: https://addons.mozilla.org/en-us/firefox/addon/uggc-protocol/ hth
01:39:06 <Bike> Meet the Developer: Eli the Bearded. Learn why uggc protocol was created and find out what's next for this add-on.
01:41:06 <oerjan> i am not sure whether that lone commenter has got the point.
01:42:06 <Bike> is this bizarro shachaf
01:46:08 -!- sprocklem has quit (Remote host closed the connection).
01:47:07 -!- kgoret has quit (Quit: Lost terminal).
01:48:17 -!- aloril has quit (Ping timeout: 248 seconds).
02:01:54 -!- aloril has joined.
02:08:18 <pikhq_> shachaf: Syntactically, it *is* a valid URL.
02:08:41 <Bike> but you need like, a scheme, man.
02:08:58 <pikhq_> Looks like it matches the generic schema.
02:10:27 <Sgeo> I um, wish I knew what that commenter was trying to say
02:10:32 <Sgeo> Almost wrote commentor. Thagora
02:17:04 <pikhq_> Opus audio on a video file in the wild.
02:19:38 -!- sprocklem has joined.
02:21:21 <pikhq_> Also fun, Ubuntu's shipped version of mplayer does not support Opus in mkv.
02:21:33 <ion> How about mplayer2?
02:21:56 <pikhq_> I just know mpv works just fine.
02:24:39 -!- Koen_ has quit (Quit: The struct held his beloved integer in his strong, protecting arms, his eyes like sapphire orbs staring into her own. "W-will you... Will you union me?").
02:28:40 -!- lexande has left.
02:35:13 -!- Bike has quit (Ping timeout: 248 seconds).
02:37:15 -!- Bike has joined.
03:06:24 -!- oerjan has quit (Quit: Gnat).
03:38:24 <Bike> http://retractionwatch.wordpress.com/2013/06/27/come-again-penile-strangulation-by-metallic-rings-retracted-for-duplication/
03:51:50 -!- NihilistDandy has quit (Quit: NihilistDandy).
03:54:25 <Bike> kmc: http://en.wikipedia.org/wiki/Rozellida pseudofungi!!
04:01:11 <shachaf> ion: little-known fact: that's how kmc got into haskell
04:54:37 <HackEgo> smlist: shachaf monqy elliott mnoqy
04:55:03 <shachaf> mnoqy did you see the top of the page
04:57:00 <mnoqy> very exciting and good
05:02:18 <shachaf> mnoqy: also this is a good comic
05:09:11 <shachaf> oerjan: Wait, did you @quit kappabot?
05:09:27 <shachaf> oerjan: That bot is in more channels than just this one, you know! @part is there for a reason!
05:14:36 <mnoqy> shachaf: yes it is a good comic
05:15:44 <shachaf> mnoqy: hey what's the cps-encoding of newtype Fix f = Fix (f (Fix f))
05:15:52 <shachaf> is it just newtype Fox f = Fox (forall r. f r -> r)............. that doesn't really sound right
05:16:38 <mnoqy> depenmds on what you mean by cps-encoding & how faithful you want to be to that newtype
05:16:54 <shachaf> i want the boehm-berarducci-church-etc thing
05:17:04 <shachaf> which turns lists into foldr and all that
05:18:12 <mnoqy> thhen thats it yes
05:18:20 <mnoqy> you might want to read http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt if you havent
05:18:43 <shachaf> ok but that's kind of weird because isn't Fix f isomorphic to (forall a. (f a -> a) -> a)
05:20:02 <mnoqy> i forget the name for that other thing youre saying woops
05:20:12 <mnoqy> i dont have "too much exposure" to it but ive seen it around
05:20:18 <shachaf> well that thing is just the type of fold
05:20:27 <shachaf> fol d:: Fix f -> (f a -> a) -> a
05:20:40 <shachaf> and you can fold with the "initial algebra" or whatever it is to get Fix back
05:20:56 <mnoqy> thats what that paper is about :-)
05:21:07 <mnoqy> its a tutorial on helping peopel get an understanding of that
05:21:20 <mnoqy> or rather a draft draft draft draft draft thereof
05:21:29 <elliott> is (forall r. f r -> r) really ~ Fix f
05:21:32 <elliott> like for instance consider f = Const Void
05:21:49 <elliott> but (forall r. Const Void r -> r) ~ (forall r. Void -> r)
05:21:54 <elliott> Fix (Const Void) is uninhabited
05:21:55 <mnoqy> i i may have oopsed BUT ALSO
05:21:59 <mnoqy> theres the thing where
05:22:03 <elliott> but (forall r. Void -> r) is inhabited
05:22:24 <mnoqy> ill just pull up the actuall thing and well settile it once and for all
05:22:35 <mnoqy> Lfix X. F X = All X. (F X -> X) -> X.
05:22:41 <mnoqy> "th re r you have it"
05:22:50 <elliott> 06:18:44 <shachaf> ok but that's kind of weird because isn't Fix f isomorphic to (forall a. (f a -> a) -> a)
05:22:57 <elliott> looks like the truth was with us all along....
05:23:07 <shachaf> elliott: p. sure edwardk said it was once
05:23:12 <shachaf> but he also said "in haskell"
05:23:23 <shachaf> and there's def. a data/codata thing going on here so maybe that's related??
05:23:48 <shachaf> because for codata you have (exists a. (a, a -> f a)) ~ Fix f "or something like that"
05:24:02 <mnoqy> you can find the eqn for that in the .txt too :) :)
05:24:03 <shachaf> i think that's the least/greatest fixed point thing
05:24:11 <shachaf> mnoqy: HEY I'M GETTING TO THE TXT OK
05:25:12 <shachaf> mnoqy: sorry for yelling :'(
05:25:44 <mnoqy> i just dont want to make the mistake again of seeing something that looks sort of like the right thing and saiyng "yes thats the right thing" when really its not
05:26:12 <shachaf> wait which thing are you talking about
05:28:22 <shachaf> 21:26:10 <edwardk> newtype Mu f = Mu (forall a. (f a -> a) -> a); data Nu f = forall a. Nu a (a -> f a) -- build mappings from Mu f -> Nu f and vice versa given Functor f
05:28:44 <shachaf> elliott: Nu (Const Void) also has exactly one inhabitant
05:29:11 <lambdabot> Not in scope: data constructor `Void'
05:29:25 <shachaf> (I.e. a type with no inhabitants.)
05:29:35 <Bike> just wondering how it like looks
05:29:38 <lambdabot> Not in scope: type constructor or class `Void'
05:30:11 <elliott> Void can be of any kind with PolyKinds on I think
05:30:14 <mnoqy> Gfix X. F X = Exists X. (X -> F X) * X,
05:30:20 <mnoqy> whats up with edwardk's Nu
05:30:39 <shachaf> mnoqy: he got it backwards
05:31:00 <mnoqy> ah that makes sense
05:31:02 <shachaf> oh that explains why my file says
05:31:03 <shachaf> data Nu f = forall a. Nu a (a -> f a)
05:31:09 <mnoqy> the Nu in his recschemes package is
05:31:12 <mnoqy> data Nu f whereSource
05:31:13 <mnoqy> Nu :: (a -> f a) -> a -> Nu f
05:31:20 <mnoqy> ^^good copy paste ^^
05:31:22 <shachaf> maybe he didn't get it backwards
05:31:28 <shachaf> no i'm the one who got it backwards just now
05:31:35 <shachaf> but it got it correct earlier
05:31:41 <shachaf> when i said (exists a. (a, a -> f a))
05:32:33 <shachaf> anyway it makes perfect sense
05:32:38 <shachaf> it's just building up a tree and all that
05:33:25 <shachaf> elliott: i misunderstood again!
05:33:35 <shachaf> (forall r. f r -> r) isn't (forall r. (f r -> r) -> r) at all
05:33:47 <shachaf> I really do doubt that (forall r. f r -> r) is right.
05:36:32 <shachaf> data Foo a = Foo a ---> newtype Foo a = Foo (forall r. (a -> r) -> r)
05:36:56 <shachaf> data Foo f a = Foo (f (Foo a)) ---> newtype Foo f a = Foo (forall r. (f r -> r) -> r)
05:37:01 <shachaf> Obviously it needs to be an argument.
05:37:21 <shachaf> elliott: OK, so "church"(/boehm-berarducci) encoding of Fix gives you Mu.
05:37:59 <shachaf> Is there a cochurch encoding that gives you Nu?
05:38:38 <shachaf> data Hi a = Hi a ----> data Ho a = forall x. Ho x (x -> a) -- totally making things up right now
05:39:47 <shachaf> OK, I guess there's no point to this encoding.
05:40:18 -!- sebbu2 has joined.
05:43:14 -!- sebbu has quit (Ping timeout: 246 seconds).
05:55:47 <Bike> http://en.wikipedia.org/wiki/Wikipedia:Department_of_Fun
05:56:28 <Bike> https://en.wikipedia.org/wiki/Wikipedia:Department_of_Https
05:56:39 <shachaf> Wikipedia does not have a project page with this exact name.
05:58:37 <shachaf> ok mnoqy i'm going to read that txt file now
05:59:17 <shachaf> mnoqy: what does 'only allowing recursion in positive position' translate to in logic
05:59:58 <shachaf> i can't say anything but nonsense ;'"
06:01:40 <mnoqy> as far as the category theory goes youre just dealing with endofunctors...recursion in the negative position translates to a contravatiant position and you cant do stuff there
06:02:33 <shachaf> you get all kinds of paradoxes when you have self reference things
06:02:36 <mnoqy> that's what i'd like to know
06:02:55 <shachaf> and curry's paradox is the kind of thing that you get with negative position recursion right
06:03:06 <shachaf> and that sort of type lets you do r. evil things if you allow it
06:03:17 <shachaf> but the types with plain old positive recursion don't
06:03:29 <shachaf> does that mean you can allow "certain kinds of self reference" or something
06:23:16 -!- FreeFull has quit (Quit: Gotta go).
06:31:45 -!- sacje has quit (Quit: sacje).
06:41:10 -!- sprocklem has quit (Remote host closed the connection).
07:25:27 -!- Phantom_Hoover has joined.
07:32:49 -!- Bike has quit (Ping timeout: 246 seconds).
08:28:44 -!- conehead has quit (Quit: Textual IRC Client: www.textualapp.com).
08:38:12 <kmc> welp i tried to write some rust code
08:38:17 <kmc> and got my brain twisted in I think a good way?
08:38:19 <kmc> time will tell
08:38:32 <elliott> I was hoping the second line would be "this is not the job for me"
08:38:38 <elliott> first line had that kinda resignation to it that suggested the possibility
08:39:06 <kmc> one cool thing is, the type of a reference includes the region over which it's valid, and you can actually name and bind these regions
08:39:26 <kmc> so a function can return a reference which is valid as long as a particular reference argument is
08:39:58 <kmc> it's the 'r here: fn get_x<'r>(p: &'r Point) -> &'r float { &p.x }
08:41:22 <kmc> I tried to implement a lambda calculus interpreter without using any managed boxes but I think that's impossible
08:41:45 <kmc> without writing your own GC i mean
08:42:36 <shachaf> have you been to a california welcome center yet
08:42:48 <shachaf> elliott: "had that kinda resignation to it that suggested that kinda resignation" hth
08:44:00 <kmc> oh also in rust the sugar for (*x).y is x.y not x->y
08:44:02 <kmc> "its weird"
08:44:28 <shachaf> yes that's "the cool thing to do"
08:45:01 <kmc> well I suppose C doesn't do that because a C compiler is allowed to be dumb as rocks
08:45:02 <elliott> just like python...............
08:45:24 <kmc> but more modern languages might want to avoid it because more overloaded syntax => more bad programs typecheck
08:45:29 <kmc> but maybe there isn't much risk of that in this case
08:46:06 <kmc> my bag came off the carousel so afk again
09:05:50 -!- epicmonkey has joined.
09:22:53 <kmc> I guess I officially live in San Francisco now :)
09:23:37 <HackEgo> kmc: 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.)
09:23:46 <shachaf> finally a proper use of `relcome
09:23:56 <shachaf> wow myndzi doesn't account for voice
09:24:02 <kmc> viz. https://sphotos-a.xx.fbcdn.net/hphotos-prn1/1011817_10100526803867865_340272139_n.jpg
09:24:13 <kmc> shachaf: that's what you get for setting empty nick whatever
09:26:45 <kmc> rust won't let me make a thing like an orphaned instance :(
09:27:09 <shachaf> Well, orphaned instances are evil.
09:27:14 <kmc> might relate to the fact that its polymorphism is accomplished through recompiling for each type (a la C++) rather than runtime parametric erasure whatever
09:27:35 <kmc> but maybe not
09:28:42 <shachaf> kmc: you should join #rust on irc.mozilla.org
09:29:00 <kmc> i just might do that
09:29:19 <shachaf> you p. know a lot of the p. there anyway
09:31:24 <kmc> https://www.imperialviolet.org/2013/06/27/botchingpfs.html
09:31:36 -!- mnoqy has quit (Quit: hello).
09:43:39 <shachaf> so you're working in sf, right? not coming down to mv?
09:43:52 <kmc> right, except for the first day
09:44:07 <kmc> and maybe others from time to time? dunno
10:25:51 <Phantom_Hoover> Wow, the Mongol conquests killed like 17% of the world population at the time.
11:02:26 -!- dessos has left.
11:16:54 -!- sebbu has joined.
11:20:18 -!- sebbu2 has quit (Ping timeout: 256 seconds).
11:25:47 -!- sacje has joined.
11:40:08 -!- Nisstyre-laptop has quit (Ping timeout: 256 seconds).
12:12:25 -!- nooodl has joined.
12:42:43 <Phantom_Hoover> thought experiment: would agda still be cool if it used pascal-style syntax?
12:54:58 -!- sacje has quit (Quit: sacje).
13:05:43 <HackEgo> olist 896: shachaf oerjan Sgeo FireFly
13:12:57 -!- MindlessDrone has joined.
13:25:59 -!- oerjan has joined.
13:37:42 -!- oerjan has quit (Quit: leaving).
13:38:11 -!- oerjan has joined.
13:39:12 -!- oerjan has quit (Client Quit).
13:39:29 -!- oerjan has joined.
13:40:52 <oerjan> there we are, back to leguin
13:41:15 <oerjan> (the norwegian server seems to be permanently refusing me)
13:41:36 <oerjan> and the rotation keeps stupidly sending me across the atlantic
13:42:35 <elliott> you could just specify a server...
13:42:50 <oerjan> elliott: um i just did
13:43:14 <oerjan> i had gibson in norwegian before, which has refused connections for weeks.
13:46:42 <shachaf> oerjan: did you see the olist
14:04:20 -!- olsner has quit (Quit: Leaving).
14:07:01 -!- sacje has joined.
14:07:23 <oerjan> <shachaf> oerjan: That bot is in more channels than just this one, you know! @part is there for a reason!
14:07:52 <oerjan> <shachaf> oerjan: That bot is in more channels than just this one, you know! @part is there for a reason! <-- oops sorry :P
14:12:25 <fizzie> oerjan: I interpreted "i had gibson in norwegian" to mean that you had a collection of Norwegian translations of Gibson's novels, and it puzzled me a whole lot as to how exactly were they "refusing connections".
14:12:43 <fizzie> "I'd really like to read this book, but it's refusing connections."
14:12:51 <fizzie> I guess in this e-age of e-books that might happen.
14:16:33 <shachaf> oerjan: exercise: write a function to convert Mu f to Nu f
14:21:59 -!- Nisstyre-laptop has joined.
14:24:36 <oerjan> shachaf: i don't even remember what those are hth
14:25:07 <shachaf> newtype Mu f = Mu { runMu :: forall a. (f a -> a) -> a }
14:25:16 <shachaf> data Nu f = forall a. Nu a (a -> f a)
14:39:47 <tswett> ACCORDING TO WIKIPEDIA, TODAY IS AN INTERNATIONAL CAPS LOCK DAY.
14:40:32 <shachaf> every day is an international caps lock day
14:41:00 <tswett> SO, UH, WHAT'S MU SUPPOSED TO BE?
14:42:02 <tswett> LIKE, UH, IT TAKES A FUNCTOR ALGEBRA THINGY AND THEN RETURNS THE UNDERLYING THING.
14:42:39 <oerjan> also it's my birthday hth
14:42:49 <tswett> LIKE, WHY DON'T WE TAKE [] AS AN EXAMPLE. Mu [] IS forall a. ([a] -> a) -> a, RIGHT?
14:42:52 <shachaf> are you a billion years old now
14:43:44 <shachaf> tswett: [] is a complicated example.............
14:44:05 <tswett> ALL RIGHT, HOW ABOUT Maybe?
14:44:27 <tswett> Mu Maybe, THEN, WOULD BE forall a. (Maybe a -> a) -> a.
14:44:42 <tswett> OF COURSE, A (Maybe a -> a) COULD BE PRETTY WEIRD.
14:45:11 <tswett> ANYWAY, I GUESS THE ONLY THING YOU CAN DO, IF YOU'RE THIS MU VALUE THING, IS PASS Nothing INTO THAT FUNCTION.
14:45:11 -!- NihilistDandy has joined.
14:45:26 <shachaf> that's the only thing you can do *at first*
14:45:34 <tswett> THEN YOU'LL GET AN a, WHICH YOU CAN RETURN, OR YOU CAN PUT IT INTO Just AND RETURN THE RESULT...
14:45:37 <shachaf> but after you do that you get an a value
14:45:44 <tswett> OR YOU CAN PUT *THAT* INTO Just AND RETURN THAT RESULT, AND SO ON.
14:46:10 <tswett> EFFECTIVELY THE NATURAL NUMBERS.
14:46:35 <shachaf> exists x. (x, x -> Maybe x)
14:47:50 <shachaf> what can you do with that?
14:48:11 <tswett> YEAH, THAT LOOKS LIKE THE NATURAL NUMBERS AS WELL. TAKE THE x, PASS IT INTO THAT FUNCTION, EITHER YOU GET Nothing OR YOU GET Just SOMETHING.
14:48:27 <shachaf> or............................................you never get Nothing!!
14:48:27 <tswett> IF IT'S THE LATTER, YOU CAN PUT IT INTO THE FUNCTION AGAIN, MAYBE YOU'LL GET Nothing THIS TIME, MAYBE YOU'LL GET Just AGAIN...
14:48:46 <tswett> RIGHT. IT'S THE-NATURAL-NUMBERS-PLUS-INFINITY.
14:48:52 <tswett> THE CO-NATURAL NUMBERS, AMIRITE?
14:49:07 <tswett> SINCE, LIKE, ISN'T THIS EFFECTIVELY A COINDUCTIVE DATA TYPE?
14:49:39 <shachaf> so now write a function to turn Mu into Nu
14:49:41 <tswett> WHAT ABOUT MU, CAN THAT ALSO BE INFINITY?
14:49:52 <shachaf> in haskell it can.....since haskell is ""confused"""
14:50:34 <tswett> HM. TO ME IT ALMOST KIND OF SEEMS LIKE A COINCIDENCE THAT THOSE THINGS ARE THE SAME THING.
14:51:47 <tswett> MU IS A FUNCTION TAKING THE ALGEBRA THINGY AND PLAYING WITH IT AND RETURNING THE ONE WHATEVER THING.
14:52:10 <tswett> WHEREAS NU IS JUST THE PART THAT GOES IN BETWEEN OR WHATEVER.
14:52:37 <oerjan> shachaf: elliott: thanks
14:53:57 <elliott> oerjan: in return you can outlaw international caps lock day in the channel
14:54:59 <tswett> ONE THING THAT THE MU COULD BE, I GUESS, IS \f -> f . Just . f . Just . f . Just . f . Just . f $ Nothing, AYE?
14:55:22 <shachaf> tswett: International Caps Lock Day has been outlawed in #esoteric
14:55:33 <shachaf> Now it's time For international shubshub Day.
14:56:06 <shachaf> you know, we Never Figured it out
14:56:26 <tswett> Is It All Right If I Just Capitalize Every Word?
14:56:46 <tswett> I dunnO, I don'T thinK thaT woulD bE thE besT ideA pragmaticallY speakinG.
14:57:00 <tswett> Anyway, what could the Nu be.
14:57:27 <shachaf> Anyway, yes, sure, That's a Good Mu value.
14:57:33 <shachaf> :t \f -> f . Just . f . Just . f . Just . f . Just . f $ Nothing
14:57:49 <tswett> Going backwards... taking a layer off each time... why would you go backwards, why would that be the same thing...
14:58:04 <tswett> Is it really possible to convert Mu into Nu or is this just an Elaborate practical joke...
14:58:11 <shachaf> > (\f -> f . Just . f . Just . f . Just . f . Just . f $ Nothing) (maybe 0 (+1))
14:58:31 <shachaf> It's really Possible to do it.
14:59:20 <tswett> I mean, if you have the fixed Point of a Type, like, a Data Constructor representing that, then it seems like you can do it.
14:59:41 <tswett> Like, define data Fix f = F (f (F f)).
14:59:45 <shachaf> well You can Make Whatever data Constructors you Want
15:00:01 <tswett> Then, uh, the Nu is...
15:00:03 <shachaf> (but Say No To negative Recursion)
15:00:32 <elliott> that shachaf is always so positive all the time.
15:00:35 <tswett> (F . Just . F . Just . F . Just . F . Just . F $ Nothing, \(F x) -> x)?
15:01:07 <tswett> In which Case it seems pretty clear how to convert the Mu into the Nu. Just pass F in and then the other Thing is always that Thing.
15:01:21 <tswett> (themu F, \(F x) -> x)
15:01:34 <tswett> If my Syntax is correct; I'm not sure you can put the Lambda Symbol directly after a Comma like that.
15:02:00 <shachaf> The syntax Is Correct but haskell Doesn't Have first-Class Existentials
15:02:11 <shachaf> So You Would instead make a Data Constructor In ghc
15:02:23 <shachaf> data Nu f = forall a. Nu a (a -> f a)
15:03:10 <tswett> Right, it's \themu -> Nu (themu F) (\(F x) -> x).
15:03:29 <tswett> So right. A Mu is effectively a forall a. (f a -> a) -> a, aye?
15:04:07 <shachaf> newtype Fix f = Fix { unFix :: f (Fix f) }
15:04:18 <shachaf> unFix :: Fix f -> f (Fix f)
15:04:24 <tswett> SO YOU'VE GOT THIS THING, YOU DOn't know what it is, and you have to, like, effectively use it to guide your Behavior.
15:05:06 <tswett> The first Argument to the Nu Constructor.
15:05:14 <shachaf> also If you Want A Bonus exercise try Turning Nu Into Mu
15:05:19 <HackEgo> 750) <Lumpio-> STOP CAPITALIZING <Lumpio-> It's making me feel weird <shubshub> the I has to be capitilized its proper grammer
15:05:37 <tswett> And then the other Thing is, of course, the second Argument to the Nu Constructor.
15:06:13 <tswett> shachaf: happy Birthday to you. Happy Birthday to you. It is likely that quoting any more of the Song would be an Infringement of Copyright.
15:06:30 <shachaf> i Heard That was Just A rumour
15:06:47 <shachaf> Oops That was improper Grammer
15:07:30 <nooodl> is shubshub the batch script esolang guy
15:07:37 <tswett> I guess it's essentially, like, you have an a, and an (a -> f a), and an (f b -> b), and you have to appropriately produce a b.
15:08:03 <tswett> Oh, and you know that the f is Maybe, of Course.
15:08:59 <nooodl> i googled his name and found http://www.youtube.com/watch?v=WOUKwJYhdss wow
15:10:16 <shachaf> esoteric/2012-04-28.txt:10:24:19: <shubshub> I Just added capital lettering to !Py!Batch
15:10:26 <tswett> So, keep operating on the a until you've gotten rid of all of the, like, a, and then do the same thing in reverse.
15:11:36 <tswett> So the first Thing we need is (a -> (a -> Maybe a) -> Fix Maybe).
15:11:56 <tswett> And that's just, uh, what should I call it. How about shake.
15:13:18 <tswett> Lemme interchange the arguments, so it's ((a -> Maybe a) -> a -> Fix Maybe).
15:13:24 <tswett> shake f x = fmap (shake f) (f x)?
15:13:38 <tswett> No, we need more constructors.
15:13:48 <tswett> shake f x = Fix (fmap (shake f) (f x))?
15:14:31 <tswett> Looks right as far as I can tell.
15:14:37 -!- Koen_ has joined.
15:14:53 <tswett> Then you just need to do the reverse. Let's call that one scrunch.
15:15:46 <tswett> With a Type along the Lines of (Fix Maybe -> (Maybe b -> b) -> b). Yeah, that sounds easy.
15:16:24 <tswett> I think we should interchange the Arguments again. ((Maybe b -> b) -> Fix Maybe -> b).
15:16:49 <shachaf> by the way you can do hylo :: Functor f => (f b -> b) -> (a -> f a) -> (a -> b) if you prefer
15:17:38 <shachaf> (Which is the same thing, of course.)
15:18:33 <tswett> scrunch f t = f (fmap (scrunch f) (unFix t))
15:18:54 <tswett> So you just need to shake and then scrunch.
15:23:17 <Koen_> he wanted to shake my hand but then I scrunched his fingers so hard there was blood everywhere
15:23:47 <tswett> The metaphor is... a T-shirt or something.
15:23:57 <tswett> If you want to turn a T-shirt into a hockey puck, what do you do?
15:24:18 <tswett> All right, I mUST LEAVE YOU GUYS FOR THE TIME BEING.
15:56:12 <oerjan> itt t-shirts, hockey pucks and burritos
15:57:29 <shachaf> kmc: your job is to find the best place in sf for a vegetarian burrito btw
16:10:24 <oerjan> it sounds like the kid in the apartment above has recently acquired a marble or something similar.
16:10:47 <oerjan> so, after all, that is what will finally be the end of me.
16:11:37 <oerjan> it has to be the ones making the noise, Phantom_Hoover
16:18:34 -!- Gracenotes has quit (Ping timeout: 256 seconds).
16:21:29 -!- mnoqy has joined.
16:38:30 -!- FreeFull has joined.
16:49:38 -!- Bike has joined.
16:54:23 -!- impomatic has quit (Read error: Connection reset by peer).
17:01:16 -!- itsy has quit (Read error: Connection reset by peer).
17:06:41 -!- impomatic has quit (Read error: Connection reset by peer).
17:08:00 -!- impomatic has quit (Read error: Connection reset by peer).
17:49:48 -!- Gracenotes has joined.
17:54:55 -!- Gracenotes has quit (Remote host closed the connection).
17:55:14 -!- Gracenotes has joined.
18:00:33 -!- epicmonkey has quit (Ping timeout: 248 seconds).
18:13:13 -!- conehead has joined.
18:18:37 <kmc> shachaf is no-meat-food-seeky
18:37:47 -!- Gracenotes has quit (Remote host closed the connection).
19:00:33 -!- olsner has joined.
19:05:53 -!- mnoqy has quit (Quit: hello).
19:07:30 <ion> I had to stop being vegetarian recently. I feel bad about it, but i have to prioritize my health over the wellbeing of production animals. As a health issue i have (had for years before i even began vegetarianism) i have real trouble getting things done. Due to that i just didn’t manage to take care of the increased effort to get all the nutrition i need.
19:08:23 -!- epicmonkey has joined.
19:52:34 -!- Nisstyre-laptop has quit (Quit: Leaving).
20:05:37 <Koen_> being vegetarian was fun
20:05:43 <Koen_> but meat is SO GOOD
20:07:02 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds).
20:29:47 <ion> I haven’t really got used to the taste of meat yet, it still feels subjectively disgusting. But that’s just a matter of getting used to it again. OTOH, i don’t think the bad conscience is going to go away. :-P
20:34:37 -!- epicmonkey has quit (Ping timeout: 276 seconds).
20:38:09 <Bike> just start with something easy, like drinking chilled pig blood, and then slowly move up to hunting squirrels and such
20:41:37 -!- sivoais has quit (Ping timeout: 248 seconds).
20:55:48 <Koen_> ion: wait... are you saying you've NEVER eaten meat before?
20:57:17 <ion> koen: I have.
20:57:44 <ion> I stopped around 13 years ago.
20:59:43 <Koen_> oh okay that's a long time
21:02:50 <ion> Enough for the desire to turn to disgust.
21:22:43 <tswett> Do the Component Object Model and the Common Language Infrastructure have anything to do with each other?
21:26:51 <coppro> i would like to purchase an internet
21:26:55 <coppro> do you have any available?
21:27:20 <tswett> I don't have any internets here at the moment, but I could create one given... let's say about three to six months.
21:28:28 <coppro> unfortunately, that timeline is unacceptable to me
21:41:45 -!- MindlessDrone has quit (Quit: MindlessDrone).
21:45:19 -!- tertu has joined.
21:45:47 -!- Bike has quit (Ping timeout: 246 seconds).
21:47:54 -!- Bike has joined.
21:48:12 -!- TeruFSX2 has quit (Ping timeout: 246 seconds).
22:05:16 <oerjan> i suggest going for an intern e.t. instead hth
22:21:44 <FreeFull> What does hth stand for again?
22:22:04 <HackEgo> hth is help received from a hairy toe. It is not at all hambiguitous.
22:27:34 <kmc> shachaf: i will let you know
22:29:04 -!- zzo38 has joined.
22:31:26 -!- Gracenotes has joined.
22:39:06 -!- Bike has quit (Ping timeout: 252 seconds).
22:39:54 -!- Bike has joined.
22:44:13 -!- Gracenotes has quit (Ping timeout: 246 seconds).
22:44:39 -!- Gracenotes has joined.
22:52:08 -!- Gracenotes has quit (Ping timeout: 256 seconds).
23:05:52 -!- TeruFSX2 has joined.
23:09:08 -!- tertu has quit (Ping timeout: 256 seconds).
23:17:57 <tswett> coppro: I recommend taking your business elsewhere, hth.
23:18:05 <tswett> elliott: I'm so glad you're not a baby any more.
23:20:14 <tswett> Nope. He's two years old now.
23:20:22 -!- sebbu2 has joined.
23:22:43 -!- sebbu has quit (Ping timeout: 264 seconds).
23:40:27 -!- Koen_ has quit (Quit: Koen_).
23:44:23 -!- Sgeo has quit (Ping timeout: 240 seconds).
23:45:57 -!- Sgeo has joined.
23:49:44 -!- sarasic has joined.
23:50:14 -!- Gracenotes has joined.
23:50:20 <lambdabot> DavidJacobs says: Code is like poetry; most of it shouldn't have been written.
23:51:01 <oerjan> (belatedly reading HWN)
23:54:59 -!- sarasic has left.
23:58:44 -!- Gracenotes has quit (Ping timeout: 246 seconds).