00:00:45 -!- mach has joined.
00:14:15 -!- mach has quit (Quit: Saindo).
00:19:02 -!- daef has quit (Ping timeout: 265 seconds).
00:32:09 -!- Asztal has quit (Ping timeout: 260 seconds).
01:26:28 -!- BeholdMyGlory has quit (Remote host closed the connection).
03:22:17 -!- adu has quit (Quit: adu).
03:54:20 -!- Sgeo_ has changed nick to Sgeo.
05:07:00 -!- oerjan has quit (Quit: Good night).
05:16:30 -!- bsmntbombdood_ has joined.
05:17:49 -!- bsmntbombdood has quit (Ping timeout: 268 seconds).
05:26:20 -!- HackEgo has quit (Remote host closed the connection).
05:26:20 -!- EgoBot has quit (Remote host closed the connection).
05:28:36 -!- HackEgo has joined.
05:28:37 -!- EgoBot has joined.
05:31:59 -!- bsmntbombdood_ has quit (Ping timeout: 265 seconds).
05:34:42 -!- gm|lap has quit (Quit: HydraIRC is a child molester -> http://silverex.net/news <- i couldn't change my quit message).
05:47:00 -!- bsmntbombdood_ has joined.
05:57:58 -!- MizardX has quit (Ping timeout: 260 seconds).
06:12:22 -!- Oranjer has left (?).
06:15:08 <augur> http://www.youtube.com/watch?v=iHlHitIc7pY
06:31:54 -!- bsmntbombdood_ has changed nick to bsmntbombdood.
06:33:21 -!- cheater2 has quit (Ping timeout: 260 seconds).
06:34:10 <augur> its awesome is why!
06:35:27 <MissPiggy> is stuff like qualia just bullshit in the same bag as astrology, reincarnation and e-meters?
06:37:00 <augur> it depends on what you mean by qualia.
06:37:16 <augur> THIS ARE PHILOLSOPHY
06:37:19 <augur> IS NO ILLEGAL MOVES
06:37:29 <pikhq> Qualia are somewhat less bullshit, in that it *can* be used sanely in philosophical discussions.
06:37:35 <MissPiggy> I mean "subjective experience of redness" might as well mean "mantra stones which you place on your body which magically heal you using the secrets of crystals"
06:37:46 <pikhq> However, they are (inherently) inobservable.
06:38:14 <MissPiggy> pikhq, all the arguments that try to argue qualia exist make me think of that 'invisible dragon in my garage' story
06:38:42 <augur> well its true, right
06:38:52 <augur> there is nothing to qualia, really
06:39:25 <augur> qualia is what an intelligent system does when it does with its senses.
06:39:37 <augur> but theres nothing more to them than that
06:39:38 <pikhq> MissPiggy: Except that the subjective experience of redness most certainly does exist in some sense.
06:39:53 <pikhq> The brain processes input and produces this experience.
06:40:06 <augur> what is the difference between experiencing and believing you're experiencing
06:40:10 <augur> thats the question i think
06:40:39 <pikhq> It's pretty near impossible to discuss scientifically, though.
06:40:59 <pikhq> (mostly because we don't have sufficient access to the workings of the human brain)
06:41:21 <pikhq> (... I should also note: nearly impossible *at the moment*. Technology could change that, in principle.0
06:44:22 <MissPiggy> it just seems like a made up thing to make people feel better, like reincarnation and free will
06:45:27 <MissPiggy> what's bugging me is that some of this stuff just seems like totally trivial concepts unrelated to consciousness -- but it _can't_ be that because then it wouldn't have all these references to consciousness
06:47:18 <pikhq> ... All it is is the interpretation of input by our brains. *That's all*.
06:47:43 <pikhq> It's about as real as gravity, but much harder to *do* anything with.
06:48:15 <pikhq> (which is why it's entirely in the realm of philosophy: they're willing to discuss "maybe"s for ages.)
06:49:09 <MissPiggy> I am experience the subjective experience of what the hell does any of this mean
06:49:21 <uorygl> So, alise is still MIA?
06:50:07 <pikhq> MissPiggy: You see something that is red. It goes to your brain. It gets processed into a qualia. You perceive the qualia, not the red thing.
06:51:29 <MissPiggy> so a qualia means some kind of neuron-state (like neuron 35252 on between 0.3 and 0.34 %, neuron 4543 on 1.1% etc...)
06:51:53 <pikhq> Very roughly, yes.
06:52:22 <pikhq> (well, some might say "the neuron state is the representation of the qualia", but whatever.)
06:52:28 <MissPiggy> but there was a discussion about being pricked by a pin it woul cause a pain qualia.. and so would a neuron controlling device that directly stimulated the neurons
06:53:13 <pikhq> Decent interpretation.
06:53:55 <MissPiggy> I suppose the semantics are just a matter of the brain interepreting its own state
06:54:17 <MissPiggy> and there is no some kind of mystical dual universe where souls exist and they 'feel' things
06:55:26 <pikhq> Just your brain doing stuff.
06:59:14 <uorygl> Kinda funny how the only way thoughts are perceived is by producing more thoughts.
06:59:29 <uorygl> Except when they produce action that produces perception. But that's not really perception of thought.
07:10:32 -!- bsmntbombdood has quit (Remote host closed the connection).
07:13:22 <augur> MissPiggy, whats your OS
07:14:31 <augur> wanna collaborate on a videogame?
07:14:44 <augur> a first-person space adventury game
07:15:06 <MissPiggy> but what would I do ? I am not good with computer
07:15:55 <augur> im gonna probably use the unity engine
07:30:48 -!- bsmntbombdood has joined.
07:30:54 -!- asiekierka has joined.
07:31:00 -!- asiekierka has changed nick to alise.
07:31:03 -!- alise has changed nick to asiekierka.
07:32:29 <asiekierka> should i change the topic to reflect the latest alise sighting
07:38:15 <augur> noooo uorygl you ruined it D:
07:38:27 <MissPiggy> and I have been worrying about this today
07:39:47 <asiekierka> I wish i hadn't done that now that I impersonated the last person I would
07:43:32 -!- asiekierka has set topic: 0 days since last topic change | 1 week since last alise sighting | <dtsund> For those who don't know: INTERCAL is basically the I Wanna Be The Guy of programming languages. Not useful for anything serious, but pretty funny when viewed from the outside. | http://tunes.org/~nef/logs/esoteric/?C=M;O=D | * MissPiggy also wished you hadn't.
07:58:44 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
07:59:47 -!- cheater2 has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:24:28 -!- coppro has joined.
08:48:58 -!- asiekierka has quit (Ping timeout: 248 seconds).
09:04:41 -!- Gracenotes has quit (Quit: Leaving).
09:28:15 -!- kar8nga has joined.
10:09:54 -!- KingOfKarlsruhe has joined.
10:13:56 -!- coppro has quit (Remote host closed the connection).
10:18:11 -!- sebbu2 has joined.
10:18:55 -!- sebbu has quit (Ping timeout: 245 seconds).
10:22:58 -!- sebbu2 has quit (Ping timeout: 264 seconds).
10:28:30 <AnMaster> Deewiant, there? I found another issue with implementing SOCK: in the fingerprint and in the BSD-style API you first create a socket, then bind it to a port and so on
10:28:38 <AnMaster> Deewiant, in the erlang api this is one single call
10:28:56 <Deewiant> So don't do anything until you need to bind...
10:28:59 <AnMaster> like you just call listen(), instead of socket(), bind(), listen(), ...
10:30:05 <AnMaster> Deewiant, yep, I just find it somewhat annoying to emulate API A on top of API B, where API B is an abstraction for API A basically
10:30:30 <AnMaster> Deewiant, also this means reflecting may happen later than expected
10:30:35 <Deewiant> AnMaster: Hey, you know CMake, right? If I have set(ARGS "foo bar") how can I execute_process(COMMAND blah "${ARGS}") so that each arg in ARGS is passed separately instead of as a single argument "foo bar"
10:31:00 <AnMaster> Deewiant, hm. I haven't tried that. What about dropping the quotes?
10:31:49 <AnMaster> Deewiant, I think I saw something to do that some time ago
10:31:58 <Deewiant> But you don't remember what or where ;-P
10:32:13 <Deewiant> I've been googling for it for a while now with no luck
10:33:13 <Deewiant> Every use case I can find seems to have hard-coded args, nothing like this
10:33:34 <Deewiant> (Typically running ${PROG} --version or suchlike)
10:33:48 <AnMaster> Deewiant, tried shell syntax for it?
10:34:00 <AnMaster> Deewiant, I mean, "${ARGS[@]}"
10:34:28 <AnMaster> Deewiant, hm isn't there a list type thingy?
10:34:52 <Deewiant> Yeah, if I drop the quotes from the earlier and do set(ARGS foo bar) it makes a semicolon-separated list automatically ;-P
10:35:20 <AnMaster> Deewiant, no I mean as in list()
10:35:38 <AnMaster> oh maybe it maps to the same below
10:35:44 <Deewiant> NOTES: A list in cmake is a ; separated group of strings.
10:35:56 <AnMaster> Deewiant, but what about extracting from that?
10:36:15 <AnMaster> well, I haven't really used lists in cmake
10:37:01 <AnMaster> Deewiant, try the cmake mailing list?
10:37:03 <Deewiant> Of course I can do list(GET "${ARGS}" 0 ARG_0) list(GET "${ARGS} 1 ARG_1) and then COMMAND blah ${ARG_0} ${ARG_1} but eh... no
10:37:33 <Deewiant> It's the only option I can think of
10:37:56 <AnMaster> Deewiant, what about list and not using quotes when using it?
10:38:42 <Deewiant> Amazing, I'd somehow not tried that pair
10:38:54 <Deewiant> I wonder if this breaks if one of the arguments contains a semicolon
10:39:31 <AnMaster> Deewiant, did it work if the arguments did not contain semi-colons?
10:39:35 <Deewiant> Well I don't think I'll be needing semicolons so I guess I'm good
10:39:50 <AnMaster> quite odd really when you think about it
10:39:59 <Deewiant> I guess if the user has a directory containing semicolons in its name that's their fault :-P
10:40:00 <AnMaster> Deewiant, what are you using cmake for btw?
10:41:51 <AnMaster> Deewiant, so you are making progress with it? All D bugs blocking it fixed?
10:42:15 <Deewiant> No, I just decided to not implement the thing which requires those bugs to be fixed
10:42:28 <AnMaster> Deewiant, and what was that thing?
10:42:32 <Deewiant> At least not yet; maybe when it's the only thing left I'll come up with something better
10:42:41 <Deewiant> Per-IP fingerprint constructors
10:42:50 <AnMaster> Deewiant, errr what would they do?
10:43:19 <AnMaster> don't you load the fingerprint per-ip anyway?
10:43:25 <Deewiant> E.g. MODE's constructor and destructor switches stack<->deque
10:43:50 <Deewiant> And yes, but the constructors/destructors are currently called only when the global loaded count is/becomes 0
10:44:16 <Deewiant> I can't remember off the top of my head but there are some cases where this is actually a correctness issue as well as a pessimization
10:44:19 <AnMaster> Deewiant, but isn't that controlled by one of the instructions of MODE rather than by loading/unloading the fingerprint?
10:45:10 <Deewiant> Flipping the mode would be too extensive if it had to copy the stack every time
10:45:41 <AnMaster> Deewiant, but if you are aiming for high speed here, why are you implementing that stuff at all? :P
10:46:09 <Deewiant> Because as I said a few days ago: CCBI aims for correctness > fingerprint support > speed
10:46:20 <Deewiant> TRDS comes first, then speed :-P
10:46:29 <AnMaster> Deewiant, and I'm quite confident you can't beat cfunge then at speed
10:46:43 <AnMaster> unless you do JIT-ing suddently
10:46:57 <AnMaster> but JIT doesn't really work if you support t
10:47:21 <AnMaster> Deewiant, with a single IP you can do it like fizzie was doing.
10:47:34 <Deewiant> Yes, but we need the TRDS support and everything ;-P
10:47:38 <AnMaster> with multiple IPs... well I doubt it is possible to gain anything with it
10:48:05 <Deewiant> I guess one could JIT while only one IP exists
10:48:18 <AnMaster> Deewiant, also, how abstracted is your stack?
10:48:39 <Deewiant> But that's a bit tricky anyways, and I'm not in the mood for making it x86-only like jitfunge :-P
10:49:11 <AnMaster> still what about your stack abstraction
10:49:12 <Deewiant> Last I checked my stack was fully abstracted
10:49:35 <AnMaster> Deewiant, so, { and } aren't implemented as using memcpy() or similar?
10:49:57 <Deewiant> That might change if it seems problematic
10:50:28 <AnMaster> Deewiant, well, cfunge's stack is quite well optimised in most parts
10:51:09 <AnMaster> abstracted yes, but the abstraction contains lots of befunge-specific functions
10:51:27 <Deewiant> AnMaster: Do you know if CMake supports some kinda categories for options? So it's not all flat at the top level in ccmake for example
10:51:40 -!- FireFly has joined.
10:51:43 <AnMaster> Deewiant, advanced/non-advanced is all afaik
10:52:03 <AnMaster> Deewiant, write a patch! file a feature request!
10:52:31 -!- sebbu has joined.
10:53:02 <Deewiant> Is it summarized somewhere what exactly happens in the configure/build steps respectively?
10:53:32 <Deewiant> Configure runs the CMakeLists, build does what?
10:53:36 <AnMaster> you could set the verbose flag in the advanced config section to make it output what commands are executed
10:53:45 <Deewiant> I mean semantically what does it do
10:53:57 <Deewiant> If I put a command foo in CMakeLists, is it always run at configure time
10:54:07 <Deewiant> If so, what exactly is run at build time
10:54:16 <AnMaster> Deewiant, I guess it says in the docs? Like "execute_process runs the thingy during configuration" or such
10:54:37 <AnMaster> to run at build time you would use a custom target
10:55:25 <AnMaster> for generating man page using help2man
10:55:29 <Deewiant> So essentially build time is what's defined in add_executable / add_library / add_custom_*?
10:55:54 <AnMaster> Deewiant, there is the install() one that maps to make install of course
10:56:12 <Deewiant> Yeah, there's install time separately, true
10:56:24 <Deewiant> And I think there was some post-install thing in one of the add_custom_* too
10:56:42 <AnMaster> possibly, when i use those I check the docs
10:57:55 <AnMaster> Deewiant, now rewrite the last one using / as the separator instead of # :P
10:58:23 -!- tombom has joined.
10:59:43 <AnMaster> Deewiant, it results in "poss I bly"
11:00:00 <Deewiant> It modifies your s/i/I/ command
11:00:00 <AnMaster> what does the i modifier do now again?
11:00:47 <AnMaster> Deewiant, well, you need g to make that work then
11:01:49 <Deewiant> Alternatively s/([iI])/ \1 /g of course
11:02:02 <Deewiant> But, I'm leaving for a few hours now ->
11:02:59 * AnMaster tries to figure out in which order the BSD style socket API functions are called
11:03:47 <AnMaster> is it socket -> bind -> (connect|listen) ?
11:04:06 -!- BeholdMyGlory has joined.
11:06:54 <fizzie> Yes, though you don't necessarily need to bind before connecting, IIRC.
11:33:25 <AnMaster> fizzie, ah, but is it allowed?
11:33:49 <AnMaster> fizzie, also, can you call setsockopt() both before and after listen()/connect()?
11:34:28 <AnMaster> fizzie, and further: how does it work for UDP sockets? I have no clue really :/
11:41:48 -!- MissPiggy has quit (Quit: Lost terminal).
11:49:57 <fizzie> It's allowed, it's just that if you connect an unbound socket, it's going to get bound to a random local port.
11:50:15 <AnMaster> fizzie, and what about udp. How is it done
11:50:26 <AnMaster> again, erlang offers a very high level API for it only
11:51:12 <fizzie> Well. For UDP sockets connect means just "set the default address for which packets will be sent if you don't use sendto."
11:51:53 <AnMaster> fizzie, and what about bind() on them?
11:52:44 <AnMaster> I mean, how do you listen to an UDP socket with the BSD API
11:53:13 <fizzie> bind assings the local address. You don't need to (and can't) call listen/accept.
11:53:45 <fizzie> But specifying the remote address with connect makes the socket only receive packets from that address.
11:53:46 <AnMaster> so you do socket() -> bind() -> recv() ?
11:54:15 <fizzie> Yes, or socket-bind-connect-recv if you want to talk with only one host.
11:55:10 <fizzie> If you don't specify the remote side with connect, you'll recv all packets targeting the address you bound to.
11:55:17 <AnMaster> sigh... erlang doesn't have that in it's udp API. it has open(Port, Options), recv(Socket, Length, Timeout) and send(Scoket, Address, Port, Packet)
11:55:40 <fizzie> You can do that manually if you want, though.
11:55:45 <AnMaster> oh wait, I think open() has it
11:55:58 <AnMaster> ah no, it is what local IP to bind to
11:56:23 <fizzie> And I think connecting an unbound UDP socket also does the "bind to random local port" thing.
11:56:49 <AnMaster> for open(): "If Port == 0, the underlying OS assigns a free UDP port, use inet:port/1 to retrieve it."
11:58:01 <AnMaster> fizzie, even more confusing is the "active" mode sockets of erlang, where arriving tcp/udp data is transformed into erlang messages sent to the process in question
11:58:21 <AnMaster> and that would have been a pain to emulate with, there are luckily passive sockets too
11:58:35 -!- cheater2 has quit (Ping timeout: 256 seconds).
11:58:38 -!- cheater3 has joined.
11:59:11 <fizzie> man 7 udp's second description paragraph (at least in my man pages) is reasonably complete.
11:59:56 <AnMaster> fizzie, oh and you can get erlang to automatically group tcp streams into various packet formats for you, like "line-based", "<n-bytes length prefix><data>" "asn1" "fcgi" "sunrm" "tpkt" and a few other ones
12:00:34 <fizzie> I suppose it's logical that Erlang makes communications easy.
12:01:08 <AnMaster> fizzie, well, it just makes emulating the low level stuff in efunge hard
12:01:16 <fizzie> I guess with SOCK you need to always use connect even with udp sockets, since you can't otherwise specify the address to send to.
12:01:17 <AnMaster> for most apps I guess this higher level API is nicer
12:01:55 <AnMaster> fizzie, yes and the whole thing maps badly onto erlang's API. Especially for UDP it will be tricky. Plus mycology only tests TCP
12:02:27 -!- lament has quit (Ping timeout: 252 seconds).
12:02:48 <fizzie> That's a bit shame in the sense that you can't as easily use a single UDP socket to serve a large number of clients.
12:03:12 <AnMaster> I think broadcast is supported by erlang
12:03:23 <AnMaster> at least there is an option for it, with the note that it only applies to UDP
12:03:44 <AnMaster> (or maybe to SCTP, let me check gen_sctp manual)
12:03:50 <fizzie> Yes, but I mean serving many unicast clients with one socket using the SOCK fingerprint.
12:04:35 <fizzie> After you C the socket to one client to send data, you can't un-C it to receive packets from others.
12:04:39 <AnMaster> like socket() -> bind() -> recev() ?
12:05:03 <fizzie> That helps only if you never need to send anything.
12:06:13 <AnMaster> fizzie, well, I don't have connect() for UDP in erlang, so I will have to emulate that...
12:06:34 <fizzie> Yes, even the undesired aspects of it.
12:07:13 -!- lament has joined.
12:07:16 <fizzie> With real connect(2), you can "disassociate" the remote-endpoint address for a UDP socket by connect(2)ing to an AF_UNSPEC address family address, but I don't suppose that's possible with SOCK?
12:07:24 <AnMaster> fizzie, if I actually ever make NSCK, I will make it closer to the erlang API, because it is easier to emulate that from C than the reverse way around
12:07:57 <AnMaster> C(s ct prt addr -- )Open a connection
12:08:10 <AnMaster> where ct is 1=AF_UNIX, 2=AF_INET
12:08:27 <AnMaster> since we can't know length of addr
12:08:32 <AnMaster> without knowing what family we have
12:08:50 <fizzie> Right. I guess you could extend that by defining 0=AF_UNSPEC, but it might not be worth it.
12:08:54 <AnMaster> as the note says on the rc page:
12:08:58 <AnMaster> "ct=1 and pf=1 are a broken spec and should not be implemented. Usage of either of these should reflect."
12:09:19 <fizzie> There aren't very many UDP servers written with Funge-98 anyway.
12:09:23 <AnMaster> fizzie, it would be better to just design a high level API that also could support unix socket and inet6
12:09:58 <AnMaster> not that anyone uses it, which is a shame
12:11:06 <fizzie> If you wish, though you could do a far better low-level API than SOCK is too.
12:11:24 <AnMaster> fizzie, but then I would have to write a test suite
12:11:53 <AnMaster> plus you would need to rewrite fungot to make use of it
12:11:54 <fungot> AnMaster: they say that it's a blast when you are boring, not knowing who he would have known it, " hey guys, *wield* a lizard corpse is guaranteed to be quite popular. there aren't any penguins this far inland. there's nothing to take on the helmet, the first time to save your game is now before it's too late.
12:11:59 <AnMaster> and I would have to implement it in cfunge
12:12:25 <AnMaster> I don't really feel like dealing with C currently
12:13:30 <AnMaster> fizzie, why did the bot put * around "wield"?
12:13:44 <fizzie> I'm going to have to rewrite fungot to use NSCK anyway, if you do that. I don't suppose those will be such large changes, though; there's only one place where it establishes a connection, after that it's just read/write (or recv/send, though the SOCK R/W map more closely to read/write).
12:13:45 <fungot> fizzie: dark one:... it came! one, single, savage thrust of her lover. if she kills the lynx, she was as a distress signal, and the four men, bending eagerly forward, saw the occupant a huddled, withered, wizened shape, very magic ( in a glittering cascade, they prayed at the goldsmith's store. there aren't any skua gulls to imitate, except that the thing about genocide is that it is food and clothing for their relentless perse
12:13:51 <fungot> Available: agora alice c64 ct darwin discworld europarl ff7 fisher ic irc jargon lovecraft nethack* pa speeches ss wp youtube
12:14:10 <AnMaster> save game before it is too late?
12:14:50 <fizzie> rumors.fal:They say that the best time to save your game is now before it's too late.
12:14:57 <fizzie> It's classified as "false", too.
12:15:56 <AnMaster> fizzie, actually I would probably make separate TCP and UDP fingerprints, since if you go for a high level API they are rather different
12:16:01 <AnMaster> and I refuse to go for a low level API
12:16:34 <AnMaster> plus TCP and UDP would be a nice way to check how much various interpreters depend on fingerprints being 4 letters
12:17:38 <AnMaster> cfunge and efunge themselves should handle it. I'm not so sure about the maintenance scripts for the fingerprint system.
12:20:02 <AnMaster> fizzie, do you need to call shutdown() before you call close()?
12:20:25 <AnMaster> since erlang API does have shutdown() and close() for TCP
12:21:03 <AnMaster> and cfunge seems to first use shutdown() with SHUT_RDWR, then close()
12:24:03 <fizzie> I'm not sure either. I think the main benefit of shutdown() is that you can half-close the connection.
12:24:33 <fizzie> But I think just close() without a shutdown will do the clean TCP connection tear-down.
12:28:40 <AnMaster> huh, erlang doesn't provide a poll() interface? I'm 100% sure it uses epoll and kqueue internally if available
12:28:57 <AnMaster> but it seems it abstracts such things away from the high level API?
12:32:33 -!- MizardX has joined.
12:33:59 <AnMaster> I think you are supposed to use multiple threads or some such instead
12:34:12 <AnMaster> fizzie, that would make it hard to provide a nice interface for polling sadly
12:34:38 <AnMaster> unless you could use the {active,once} mode that sends messages for one message then switches to passive
12:36:40 -!- kar8nga has quit (Remote host closed the connection).
12:53:59 <AnMaster> fizzie, there still? How does this sound http://sprunge.us/cBWI
12:54:16 <AnMaster> with just the overall layout specified yet
13:32:17 -!- MizardX has quit (Read error: Connection reset by peer).
13:32:39 -!- MizardX has joined.
13:47:55 -!- kar8nga has joined.
14:24:22 -!- oerjan has joined.
14:42:36 -!- KingOfKarlsruhe has quit (Remote host closed the connection).
14:45:49 -!- MizardX has quit (Read error: Connection reset by peer).
14:45:59 -!- MizardX has joined.
14:47:27 -!- happyKoalla has joined.
14:53:58 -!- adam_d has joined.
14:57:00 -!- scarf has joined.
15:43:44 -!- Asztal has joined.
15:47:25 -!- Azstal has joined.
15:48:57 -!- Asztal has quit (Ping timeout: 265 seconds).
16:01:56 -!- lament has quit (Ping timeout: 240 seconds).
16:02:06 -!- lament has joined.
16:20:40 -!- kar8nga has quit (Remote host closed the connection).
16:39:01 -!- oerjan has quit (Quit: leaving).
16:44:11 -!- MissPiggy has joined.
17:07:14 -!- cheater3 has quit (Ping timeout: 246 seconds).
17:32:22 -!- MizardX- has joined.
17:32:23 -!- MizardX has quit (Read error: Connection reset by peer).
17:32:50 -!- MizardX- has changed nick to MizardX.
17:43:13 -!- happyKoalla has quit (Quit: Leaving.).
17:57:37 -!- ehird has joined.
17:59:07 -!- ehird has quit (Client Quit).
18:07:00 <scarf> happy australian mailing list reminders day?
18:07:02 <scarf> also, that was ehird
18:07:07 <scarf> yay, at least he's still alive
18:08:17 -!- ehird has joined.
18:08:22 -!- ehird has changed nick to alise.
18:08:35 <alise> #esoteric-priv, stat.
18:10:10 -!- cheater2 has joined.
18:11:09 -!- Deewiant has set topic: 0 days since last topic change | 0 days since last alise sighting | <dtsund> For those who don't know: INTERCAL is basically the I Wanna Be The Guy of programming languages. Not useful for anything serious, but pretty funny when viewed from the outside. | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
18:20:35 -!- asiekierka has joined.
18:22:59 -!- MigoMipo has joined.
18:46:35 -!- kar8nga has joined.
18:56:30 -!- bsmntbombdood has quit (Remote host closed the connection).
18:59:21 <pikhq> alise: In #esoteric?
19:00:12 <pikhq> "M' sxat' vid' l' lingv'.", I say in horrifically butchered Esperanto.
19:00:37 <alise> Lovely! Now translate.
19:00:46 <pikhq> I'd like to see the language.
19:01:28 <alise> Well, it's not /intentionally/ esoteric, but it does require a Ph.D. to understand...
19:02:01 <alise> Hey, Epigram's mailing list is hosted in the university of the county I am in!
19:02:32 <alise> DEPENDENTLY-TYPED BUDDIES
19:02:54 <alise> pikhq: Anyway, it's the same dependently-typed fuddlepip I've been on about for ages.
19:05:21 <alise> pikhq: Recent developments... uh, I realised a few days ago that the way it defines equality means that function1 === function2 means "function1 gives the same results as function2 for all inputs".
19:05:25 <alise> My language can do the freaking impossible!
19:05:53 <alise> pikhq: But it can actually compute it!
19:06:01 <alise> Admittedly for /tricky/ things you need to give it some proof mon.
19:06:07 <pikhq> alise: So, your language is total?
19:06:08 <alise> But still, coooool.
19:06:27 <alise> pikhq: Yes - but it doesn't check all inputs, total languages can still have infinite input and output sets, lilke Nat.
19:06:33 <alise> Also, with the partiality monad it's turing-complete.
19:06:45 <alise> Here's the definition of equalilty:
19:07:09 <alise> data _===_ : {a:*} -> (x:a) -> a -> * where
19:07:15 <alise> ===-refl : x === x
19:07:31 <alise> i.e., (a === b), where a and b are values of any type, is a type.
19:07:45 <alise> If a and b are the same, then there is a value of that type (===-refl).
19:07:47 <alise> Otherwise, the type is empty.
19:07:59 <alise> Since types = statements and values = proofs...
19:08:15 <alise> "The same" means "indistinguishable", btw, i.e. the normal forms are the same.
19:08:37 <alise> Setoids/quotient types let you define your own equality relation, basically by making two "equal" elements indistinguishable even if they wouldn't normally be with Fancy Stuff.
19:08:50 <alise> pikhq: So, uh, how much of that did you understand?
19:09:22 <pikhq> Uh. I'm not sure I grok the definition.
19:10:59 <alise> * is the type of types
19:11:28 <alise> (foo : t) -> is the same as t -> but we bind the /value/ of the argument to foo in the type
19:11:32 <alise> (not at runtime, it's the dependent magic)
19:12:11 <alise> {x} is just like x except the argument is inferred, i.e. the compiler works out the value
19:12:18 <alise> we don't need to specify it
19:12:27 <alise> the data clause is just like haskell's gadt
19:12:49 <alise> so === takes, inferred, a type "a" (this is like forall a.), a value x of that type, another value of that type, and results in a type.
19:12:59 <alise> so within the constructors we have x bound to the first value
19:13:03 <alise> so we do, basically
19:13:08 <alise> YepIndeed :: Equal x x
19:13:19 <alise> i.e. ===-refl is a value of type x === x, and there are no other constructors
19:13:27 <alise> so we cannot construct a value of type x === y unless x and y are the same
19:18:36 <alise> pikhq: Am I to take that as a no? :P
19:19:18 <MissPiggy> alise in Coq you can use ifte on anything with two constructors
19:19:39 <alise> So you couldn't ifte an x === y by my definition?
19:19:39 <MissPiggy> so bool {true,false} and P + Q {inl pPrf, inr qPrf} etc
19:20:17 <alise> My definition is better because it uses the proper curry-howard view of types anyway :|.
19:22:38 <alise> pikhq: you displease me
19:22:42 <alise> anyone else want to hear me blab?
19:23:41 -!- impomatic has joined.
19:25:22 <MissPiggy> because I tried to talk about my own stuff
19:25:25 <alise> i'm not I just already
19:25:31 <alise> explained everything I was gonna :)
19:25:34 <alise> also ifte is yours you mmean?
19:25:39 <alise> as opposed to Coq's
19:25:42 <alise> SO THE LAMENESS IS ON YOUR PART
19:25:42 <MissPiggy> I just already the whole thing I was gonna
19:26:03 <MissPiggy> ifte is from coq and it's not lame ! it's good
19:26:22 <MissPiggy> say f :: Either a b, if f then p else q
19:27:26 <alise> mine is the /real/ meaning of if then else, i.e. if /true/
19:27:39 <alise> and truth in such a lang is presence-of-value
19:27:51 <alise> the construct you mention may be more useful
19:28:02 <alise> but mine lets you write things like "if x < y" with < : a -> a -> * and have it work coherently
19:28:15 <alise> i think that op would be useful that you mention under a different name
19:29:31 <MissPiggy> the true meaning if IF HYP THEN CONS ELSE ALT is HYP /\ CONS \/ ~HYP /\ ALT
19:30:01 -!- asiekierka has quit (Ping timeout: 276 seconds).
19:34:09 -!- MizardX has quit (Ping timeout: 260 seconds).
19:34:34 <alise> MissPiggy: right but we're trying to import type-level truths into value-level conditionals
19:34:49 <alise> fact is this is a useful operation I'm sure you can't deny that branching on (x < y) is common
19:34:52 <alise> ifte looks like a good op too though
19:34:59 <MissPiggy> what's your take on typeclasses, in a dependently typed setting anyway?
19:35:16 <alise> typeclasses suck anywhere :/
19:35:34 <MissPiggy> to me they seem very useful (I am using them a bit actually), but it's quite complicated and magic which I don't like
19:36:22 <alise> They are useful but they have such complications, even functional dependencies result in lots of ambiguity.
19:36:32 <alise> Has anyone actually formalised them, I wonder?
19:36:57 <alise> hmm mixfix operators could do with a character signifying whitespace
19:43:15 <pikhq> alise: Sorry, doing a kanji review.
19:44:28 <pikhq> Not all that Jewish.
19:45:08 <alise> So I'm using the Unicode minus sign β instead of - for subtraction.
19:45:13 <alise> I may or may not be Unicode-mad.
19:46:45 <alise> pikhq: That definition of _===_ I gave you? That's not the /real/ definition.
19:46:52 <alise> Wanna see the /real/ definition?
19:47:04 <Gregor> ΧΧΧΧΧ ΧΧΧΧ¨ ΧΧ€Χ ΧΧͺ
19:47:35 <pikhq> Gregor: How Jewish of you.
19:47:58 <alise> data _β‘_ : {a:β} β (x:a) β a β β where
19:48:04 <alise> pikhq: Behold the Unicode, bitch.
19:48:10 <alise> I got it slightly wrong
19:48:16 <pikhq> alise: Mmm, Unicode.
19:48:24 <alise> data _β‘_ : {a:β} β (x:a) β a β β where
19:48:24 <alise> β‘-refl : x β‘ x
19:48:31 <Gregor> ΧΧ Χ ΧΧΧ©ΧΧͺ Χ©ΧΧ Χ ΧΧ€Χ Χ ΧΧΧ©Χ¨ΧΧΧ, ΧΧ Χ ΧΧΧ©Χ Χ©ΧΧ Χ ΧΧ€Χ Χ ΧΧΧ©Χ¨ΧΧΧ, ΧΧ Χ ΧΧΧΧͺ ΧΧΧ©Χ ΧΧ
19:49:24 <pikhq> alise: So. data === with a being a type, x being the same type as a, mapping from a to a type, where the property "x === x" is true?
19:49:37 <alise> Let me rewrite it in Haskell + some notation.
19:49:43 <alise> pikhq: You know GADTs, right?
19:49:48 <pikhq> That'd help -- your notation is dense.
19:51:06 <alise> data Eq :: forall a. (x:a) -> a -> * where
19:51:06 <alise> Constructor :: Eq x x
19:51:07 <alise> The only additional notation you need here is (x:a) -> ... means a -> ..., except at the type-level (at compile-time, not run-time; it's complicated), we bind the run-time value of the argument to the name x.
19:51:28 <alise> Oh, and we can give value arguments to types.
19:51:46 <alise> So: "Constructor :: Eq 2 2", and "Constructor :: Eq (2+2) (3+1)" but not "Constructor :: Eq 1 2".
19:51:53 <pikhq> That's fairly straightforward.
19:52:01 <alise> Since values = proofs and types = logical statements, voila!
19:52:08 -!- scarf has quit (Remote host closed the connection).
19:52:26 <alise> pikhq: Oh, you want me to BLOW YOUR FREAKIN' MIND?
19:52:30 <alise> Do you know what Leibniz's law is?
19:53:00 <pikhq> I do, but please inform this gentleman, as he is a Mongolian. He doesn't even have a cow!
19:53:37 <alise> http://en.wikipedia.org/wiki/Identity_of_indiscernibles
19:53:42 <alise> your fucking Mongolian can read WP bitch :|
19:54:39 <alise> leibniz : {a:β} β {P : a β a} β {x:a} β {y:a} β {x β‘ y} β P x β P y
19:55:13 <pikhq> You just did Leibniz's law in your language.
19:55:15 <alise> "For a given type a, and a given function from a to a (P), and two values x and y of type a, and given x === y, then P x implies P y.@
19:55:56 <alise> "Give me (implicitly): a type a, a function (a -> a) P, an a x, an a y, an x === y. Then give me a value of type (P x). I'll give you a value of type (P y)."
19:56:05 <alise> pikhq: The best part? Here's the definition (proof).
19:56:12 <alise> The compiler can PROVE IT AUTOMATICALLY.
19:56:18 <alise> This isn't just theory; Agda does it.
19:56:30 <pikhq> This might be a pain to implement.
19:56:55 <alise> It's exactly the same as writing a constructivist proof system, which is exactly the same as writing a dependently-typed, total programming language.
19:57:09 <pikhq> (... In the sense that Haskell is a pain to implement well.)
19:57:14 <alise> MissPiggy: yeah it does
19:57:17 <alise> I've seen the definition
19:57:43 -!- MigoMipo has quit (Read error: Connection reset by peer).
19:58:51 <alise> http://www.cs.nott.ac.uk/~nad/repos/lib/src/Relation/Binary/PropositionalEquality/Core.agda
19:58:58 <alise> it's either sym, trans or subst; I forget whicch
19:59:21 <alise> http://www.cs.nott.ac.uk/~nad/repos/lib/src/Relation/Binary/PropositionalEquality.agda some more properties including subst_2
19:59:26 <alise> (subst on 2-adic functions)
20:00:13 <alise> one of those IS leibniz just named funny and under a wall of types
20:00:19 <alise> if you expand all the types it does come out to the type I showed
20:01:03 -!- lament has quit (Ping timeout: 240 seconds).
20:01:37 -!- lament has joined.
20:05:29 <alise> {a:β} β {x:a} β {y:a} β ({P : a β a} β P x β P y) β x β‘ y
20:05:32 <alise> is more interesting
20:12:05 <uorygl> alise: does your language have * : *?
20:12:36 <uorygl> Also, did I miss the #esoteric-priv stuff?
20:19:08 <alise> The other way around.
20:19:21 <alise> It has β : βn 1
20:19:50 <alise> I'm not sure how to split Set/Prop though, what symbols, whether to have a supertype etc
20:19:53 <uorygl> I wonder if I can get my hands on the #esoteric-priv stuff somehow.
20:21:36 <alise> Ask MissPiggy for the complete log.
20:22:05 <uorygl> MissPiggy, may I please have the complete log?
20:33:13 -!- impomatic has quit (Ping timeout: 264 seconds).
20:46:31 <alise> MissPiggy: did you give it to uorygl?
20:46:46 <uorygl> I don't seem to have received it.
20:48:12 -!- MigoMipo has joined.
20:48:16 <alise> bad MissPiggy, bad! :P
20:55:53 <alise> foo : {a:*} -> {x:a} -> {y:a} -> ({P : a -> a} -> P x -> P y) -> x === y
20:55:54 <alise> foo {_} {x} f = f {x ===} _
20:56:18 <alise> I guess letting P involve === is kinda cheating though.
21:01:30 -!- lament has quit (Ping timeout: 258 seconds).
21:02:25 -!- lament has joined.
21:06:53 <Sgeo> http://igoro.com/archive/human-heart-is-a-turing-machine-research-on-xbox-360-shows-wait-what/
21:10:22 * Sgeo goes to play a bit of RoboZZle
21:15:31 * Sgeo goes to try asikierka's tree
21:17:59 <Sgeo> That was too easy, and didn't feel treelike
21:20:29 -!- MizardX has joined.
21:28:35 -!- zzo38 has joined.
21:31:13 <zzo38> I wrote on 10.02.26 that (fork\I) is "the set of all single element sets of single element sets". But now I think that's wrong. It is (I) itself that is "the set of all single element sets of single element sets".
21:32:37 <zzo38> (fork\I) is simply "the set of all single element sets".
21:34:07 <zzo38> I also want to know if you know any other set paradoxes.
21:34:16 <zzo38> (Other than Russell paradox)
21:38:09 <zzo38> OK, I found it, and I found out its similarity
21:41:39 <zzo38> I want to figure out how to represent it in Hyper Set Language. I noticed that the set of all natural numbers is naturals=successor%0;
21:41:57 <zzo38> But you can get the successor of that, too (successor/naturals)
21:42:22 <zzo38> And even (successor%naturals)
21:45:44 <zzo38> I prefer the "Nostalgia" skin in Wikipedia but esolang wiki doesn't have that one
21:51:05 <alise> set of all natural numbers:
21:52:58 <alise> data β : β
where
21:53:22 <alise> for the unicode challenged
21:53:26 <AnMaster> fizzie, Deewiant: http://sprunge.us/cjVA <-- early draft for that
21:53:32 <augur> imma make a video game :D
21:53:38 <AnMaster> alise, you weren't here the last few days
21:53:49 <alise> AnMaster: I wasn't, and I'd rather not talk about it.
21:56:12 <pikhq> AnMaster: Nothing much to worry about, though.
21:56:47 <augur> some sort of space piloting game that puts you in a situation like Farscape
21:57:44 <augur> zzo38: basically you're stuck in a far off part of the universe having to escape some crazy super powerful dudes
21:57:53 <augur> and your ship is all fucked up so it doesnt do quite what you want it to do
21:57:53 <AnMaster> pikhq, any opinion on http://sprunge.us/cjVA ?
21:58:11 <augur> but you dont have money, you have to work using your only resource: your ship
21:58:12 <AnMaster> it is a rather early draft of course
21:58:18 <AnMaster> no details about most commands yet
21:58:23 <augur> and you can do various things to that end
21:58:41 <zzo38> I made some games on computer a lot, including one game where you have to make rectangle to catch colored balls and make a hole. You have to prevent the white ball from falling into a hole or from colliding with colored balls. And the rectangle has to be moving the white ball and has to have the corners on tiles all of the same color. Each ball of the correct color 2 points, each other 1 point. You need 2 points to be valid, and then the points
21:58:51 <pikhq> AnMaster: Looks less painful than BSD sockets.
21:59:24 <AnMaster> pikhq, and actually usable, SOCK has many parts that aren't actually accessible due to stupid design
21:59:35 <zzo38> alise: I have not seem the notation "data N : *" before
21:59:48 <pikhq> zzo38: It's an ehird-ism.
21:59:56 <AnMaster> pikhq, like UNIX sockets. the specification for if it is an unix or an inet socket comes below the address on the stack. And you need to know which type it is to know what format the address is in!
22:00:11 <alise> zzo38: It's dependent type theory, which is isomorphic to intuistionistic logic.
22:00:25 <alise> Basically, it's computable logic.
22:00:46 <alise> Dependently-typed programming language <=> intuitionistic computer proof system
22:01:15 <alise> "data N : * where" just defines the set N (* is read as "set", : is read as "is a").
22:01:16 <pikhq> AnMaster: Wait, there was already a sockets API for Befunge that did that?
22:01:24 <pikhq> AnMaster: *Eeeeew*.
22:01:28 <alise> It's just defining the set N inductively, pretty much.
22:01:50 <AnMaster> pikhq, yes, the one fungot uses
22:01:50 <fungot> AnMaster: they say that shopkeepers don't read, so that his mouth as a cloud, by samuel taylor coleridge)
22:01:56 <fungot> http://git.zem.fi/fungot/blob/HEAD:/fungot.b98
22:02:15 <fizzie> "They say that shopkeepers don't read, so that his mouth as a cloud."
22:02:30 <AnMaster> fizzie, mixed up ones I guess?
22:02:47 <alise> Wondered lonely as a cloud will be the last bit.
22:03:29 <alise> A shopkeeper, his mouth as a cloud: creating only obscurity, not one wit of understanding; for that that travels through his ears finds no passage to the outward path.
22:03:34 <AnMaster> pikhq, anyway look at SOCK: http://rcfunge98.com/rcsfingers.html#SOCK
22:03:41 <AnMaster> pikhq, spot the multiple issues
22:03:47 <alise> There, I made it make sense. POETICALLY
22:05:36 <AnMaster> pikhq, so yes I'm aiming for a somewhat higher level and more advanced API than that
22:05:52 <AnMaster> I do need some help with figuring out the best interface for SCTP however
22:06:01 <fizzie> "Shopkeepers don't read, so what use is engraving in a shop?" (rumors.tru) + "-- so that his mouth and jaws were completely hidden --" (from "mummy wrapping" entry) + "-- until they laid Tyr's hand into his mouth as a pledge." (from "tyr) + what alise said for the last bit.
22:06:07 <AnMaster> I have only used SCTP a tiny bit
22:07:01 <AnMaster> fizzie, what? it added cloud to make it poetical?
22:07:19 <AnMaster> or is this some famous poetical work?
22:08:24 -!- jcp has joined.
22:08:39 <AnMaster> (yes I'm aware of prose poetry)
22:08:54 <AnMaster> (it is a border case, some instances are okay, some are not IMO)
22:09:59 <alise> You don't know "I wonder lonely as a cloud"?
22:10:13 <alise> Also, /me slaps AnMaster about a bit with the Rime of the Ancient Mariner.
22:10:21 <AnMaster> alise, can't say it is familiar. Remember I'm from a different culture
22:10:54 -!- kar8nga has quit (Remote host closed the connection).
22:12:50 <alise> MissPiggy: is there any actual problem with supertypes?
22:12:58 <alise> after all (exists e. e) ...
22:13:13 <alise> so why can't we say N = N* intersect {0}?
22:13:21 <alise> no dependent lang seems to allow such constructions
22:15:28 <alise> Union, not intersect.
22:20:03 <Sgeo> "A website designer created a script that would create a webpage comparing every possible text color to every possible background color (16,777,216 colors each). The page that would have resulted was calculated to be more than 19 Peta Bytes in size using the system of 1 KB = 1024 Bytes, 1 MB = 1024 KB, etc. The script was never run."
22:23:13 <alise> MissPiggy: Howso, in Coq or Agda or similar?
22:24:41 <alise> http://upperandlowercase.com/musicvariant2/ _what-
22:25:01 <alise> MissPiggy: but do agda and coq allow you to make such a subtyping?
22:31:18 -!- oerjan has joined.
22:31:49 <alise> MissPiggy: Please give oerjan the complete -priv log, if that's okay.
22:36:31 <zzo38> A spider-web in dark is a good way to stop the war
22:36:50 <oerjan> <pikhq> "M' sxat' vid' l' lingv'.", I say in horrifically butchered Esperanto.
22:37:11 <oerjan> is ' legal not-before vowels?
22:37:25 <zzo38> I don't know Esperanto language very well what does that mean please?
22:37:45 <oerjan> <pikhq> I'd like to see the language.
22:37:47 <pikhq> oerjan: Actually, you're not supposed to omit the ending of every word. :P
22:39:00 -!- tombom has quit (Quit: Leaving).
22:39:27 <zzo38> A spider-web in dark is a good way to stop the war. (It was a D&D game we played on Thursday, and, this idea did work, very well actually)
22:44:31 <zzo38> The war does not know how to think ahead. And that's why they didn't win the war.
22:44:52 -!- Timoriensis has joined.
22:46:58 -!- Timoriensis has left (?).
22:47:19 <alise> X* is X-without-0; is there similar notation for X-without-negatives?
22:48:12 <alise> that's X-without-0, i.e. X*
22:48:17 <alise> I'm wondering about X-without-negatives
22:48:21 <oerjan> in math? R^+ is R without either negatives or 0, afair
22:48:24 <alise> pretty sure it's X^+ yeah
22:48:54 <alise> oerjan: so clearly R^{+{-*}} is what I need
22:49:06 <alise> where -* means "with 0", being the inverse of *
22:49:08 <zzo38> Naturals without zero: naturals_without_zero=naturals!1;
22:49:56 <alise> oh wait I want Q+ not Q+ with 0
22:50:35 <alise> I find it aesthetically pleasing.
22:50:42 <oerjan> especially since X* has other meanings, especially if X is a vector space
22:50:50 <MissPiggy> that has nothing to do with the set being zeroless
22:51:06 <alise> oerjan: yeah but i don't care about that :)
22:51:11 <alise> MissPiggy: it's just notation
22:51:18 <alise> notation is inherently arbitrary
22:51:28 <alise> "nothing to do" doesn't matter is what I mean
22:51:36 <alise> no notation has anything to do with what it represents
22:51:43 <alise> we pick aesthetically pleasing, memorable notation, and that's it
22:51:53 <MissPiggy> you could equally argue that no word means anything
22:52:05 <alise> no word has any relation to its meaning
22:53:14 <alise> well let's consider "not black"
22:53:18 <alise> we think this has a relation to "black"
22:53:28 <alise> but the concept being expressed is /everything/ just to the exclusion of black
22:53:45 <alise> i.e. in the "true meaning", without any level of abstraction or function, just value, so to speak, there is no "black"
22:53:48 -!- Oranjer has joined.
22:54:00 <alise> so "not black" relates to the word "black" but its meaning does not relate to the meaning of "black"
22:55:15 <alise> i guess i just stepped into the lovely deep-end of things i don't really know shit about
22:55:53 <MissPiggy> alise you read On Denoting by Russle
22:56:13 <augur> what are you kids talking about
22:59:02 <alise> /what/, I don't have \top and \bot in emacs
23:00:50 -!- MigoMipo has quit (Quit: When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net).
23:02:21 * oerjan read \bot as lambdabot, and wondered why you'd expect it in emacs
23:05:32 -!- ehird has joined.
23:05:35 -!- alise has quit (Ping timeout: 245 seconds).
23:05:47 <ehird> what did i miss since migomipo left?
23:07:25 <oerjan> * oerjan read \bot as lambdabot, and wondered why you'd expect it in emacs
23:12:08 <MissPiggy> http://2.bp.blogspot.com/_mmBw3uzPnJI/S2Ltvwxm04I/AAAAAAABAQU/qcggMUcrims/s1600-h/ipad_12.jpg
23:16:24 <ehird> MissPiggy: i thought of some two-dimensional notation for dependent types
23:17:35 <ehird> the regular type, with more spacing between the function arrows, but with (x:T) replaced with T. Above, a line along the whole thing. Above, in the middle of the T without the x, "x", for each such argument.
23:17:43 <ehird> the f : goes on the dividing line
23:20:44 * Sgeo can't seem to copy from a PDF
23:21:03 <ehird> MissPiggy: do you like the notation though?
23:22:42 <ehird> basically there's a line, and above is the dependent section; below, the normal section
23:22:55 <ehird> normal section is all the types, none of the names, connected by arrows; drab and usual
23:23:04 <ehird> above, in the locations of dependent arguments, the names we bind them two
23:24:24 <MissPiggy> ehird are you likey to be on tommorow if not when
23:25:08 <ehird> if not tomorrow, then say before the end of next week
23:25:26 <ehird> one final thing before you go :|
23:26:26 <ehird> === : ---------------------------
23:26:27 <ehird> Set -> A -> A -> Set
23:26:29 <ehird> IT IS GOOD NOTATION LOVE IT
23:27:01 -!- zzo38 has quit (Remote host closed the connection).
23:27:01 <MissPiggy> one thing which is good is implicit binding
23:27:11 <ehird> what do you mean by that?
23:28:10 <ehird> Oranjer: it says things
23:28:13 <ehird> MissPiggy: don't want to :D
23:28:17 <ehird> but what do you mean by implicit binding
23:28:19 <ehird> oerjan: things. complicated
23:29:11 -!- MissPiggy has quit (Quit: Lost terminal).
23:29:16 <Oranjer> but what does it say, ehird?
23:31:21 <Oranjer> delightful my existence must be
23:32:06 <ehird> Eb tsum ecnetsixe ym lufthgiled
23:32:08 <ehird> Nope, not an anagram
23:33:59 <ehird> I'm becoming dissatisfied, I think, with the usual GADT method of defining inductive types.
23:34:02 <ehird> It feels to specialised.
23:36:15 <ehird> I guess I see the definition of the set, i.e. the T in data X : T where ..., and the definition of the constructors, i.e. the ... in the same, as being separate.
23:36:44 <ehird> Nat = data zero : Nat
23:36:45 <ehird> succ : Nat β Nat
23:36:45 <ehird> however, leans too much to the right for my liking; and besides, does this even make sense?
23:36:54 <ehird> Doesn't Nat expand indefinitely? If not, what does "data" actually mean?
23:38:17 -!- Gracenotes has joined.
23:42:24 <ehird> It's complicated. You wouldn't understand.
23:42:34 <ehird> Oranjer: Okay, let me rephrase.
23:42:58 <ehird> I don't have the hours or the high-level understanding necessary to eloquently explain the theory behind it all to you.
23:43:23 -!- Azstal has quit (Ping timeout: 245 seconds).
23:43:24 <Oranjer> is there a place that does?
23:43:49 <oerjan> Nat = Fix (\t -> data Zero | Succ t)
23:43:55 -!- Asztal has joined.
23:44:32 <ehird> Oranjer: Well... it's dependent type theory.
23:44:47 <ehird> But good luck. You need a strong backing in functional programming and some backing in logic.
23:44:59 <ehird> oerjan: I have this slight feeling that that is not well-defined. :P
23:45:08 <ehird> Also, bah; I despise non-G ADT syntax.
23:45:24 <ehird> At the very least, "Nat = Fix (\t -> data Zero : t; Succ : t -> t)".
23:45:31 <ehird> But yes, I considered "data a where ...".
23:45:38 <ehird> I dislike it; we shouldn't need such arbitrary binding of names.
23:45:46 <oerjan> um the whole point is you _don't_ have t as the result before using Fix
23:46:35 <oerjan> \t -> data Zero | Succ t would be something like an anonymous type constructor
23:46:44 <ehird> right but remember all this must be total
23:47:00 <ehird> regular function-level "fix : (a -> a) -> a", at least, is totally verboten
23:47:03 <oerjan> that's total enough, you could name it
23:47:20 <ehird> Fix : (Set -> Set) -> Set
23:47:21 <oerjan> fix here means smallest fixpoint of types
23:47:29 <ehird> prove it; Fix f = ...?
23:47:35 <ehird> I'm not doubting, I'm just curious
23:48:08 <oerjan> well it's just what i _think_ inductive data types are defined as in denotational semantics
23:48:19 <oerjan> while codata uses largest fixpoint
23:48:32 -!- coppro has joined.
23:50:06 <oerjan> i don't know what restrictions there are on the Set -> Set, like you say, to make it work
23:51:47 <oerjan> oh i _think_ it would be isomorphic to having a single inductive data type data Fix t = Fix (t (Fix t)), and using it to construct everything else?
23:52:01 <oerjan> or i could be horribly wrong :)
23:54:48 <ehird> oerjan: if so that would be nice
23:54:52 <ehird> as a theoretical underpinning
23:54:56 <ehird> data β : Set where
23:54:56 <ehird> β : (f : ββΊ β β)
23:54:56 <ehird> β {{Ξ΅β:ββΊ} β {Ξ΅β:ββΊ} β abs (f Ξ΅β - f Ξ΅β) β€ Ξ΅β + Ξ΅β}
23:54:58 <ehird> I think I have that rigght
23:55:13 <ehird> Fuck yeah, definin' the computable reals 'n shit
23:57:55 <ehird> yeah - long story.
23:58:07 <ehird> suffice to say there are now _two_ crises in my life.
23:58:29 <coppro> being replaced by your female alter ego isn't one of them, I presume
23:58:54 <ehird> oops, my name changed back.
23:58:57 -!- ehird has changed nick to alise.
23:59:04 <alise> --no, that would merely be interesting
23:59:16 <alise> are we talking full sex change here or just ephemeral gender switch?
23:59:58 <pikhq> I'd hesitate to call either one a crises -- though sometimes it can be a *pain in the ass*. ;)