00:01:12 -!- Patashu has joined.
00:17:56 <Gregor> In Catholicism, the halting problem is believed to be unsolvable for infants who die before baptism.
00:19:00 <ais523> well, it's unsolvable for most other TC systems...
00:22:06 <Gregor> Well, this is quite the opposite of atheinformatic common wisdom, which is that the halting problem is solvable for all humans. (doesHalt (x:human) -> true)
00:22:34 <ais523> ah, I see
00:22:44 <zzo38> I read about Curry-Howard and how you can use it to make intuitionistic logic with Haskell. But how can you make Typographical Number Theory with Curry-Howard?
00:24:22 <zzo38> But still, even if you write the program in Haskell using intuitionistic logic, you still need to ensure all outputs are defined if the input is defined. Sometimes is difficult due to halting problem but you can make a subset that halts. It is still not complete, they could make up a PROVE pragma to do it?
00:25:23 <zzo38> And if there is no proof, use the ASSUME pragma.
00:29:55 -!- copumpkin has quit (Ping timeout: 260 seconds).
00:30:19 -!- copumpkin has joined.
00:48:24 -!- ive has quit (Ping timeout: 252 seconds).
00:52:37 -!- kmc_ has joined.
00:52:48 -!- nooga has quit (Ping timeout: 252 seconds).
00:54:27 -!- kmc has quit (Ping timeout: 252 seconds).
00:55:53 -!- kmc__ has joined.
00:59:30 -!- kmc_ has quit (Ping timeout: 250 seconds).
00:59:55 -!- zzo38 has quit (Remote host closed the connection).
01:02:17 -!- kmc_ has joined.
01:05:19 -!- kmc__ has quit (Ping timeout: 252 seconds).
01:06:52 -!- kmc_ has changed nick to kmc.
01:13:49 <quintopia> sam hughes is a bastard :(
01:21:42 <Sgeo> quintopia, hmm?
01:25:57 <quintopia> the yawning tweet. elliott made me yawn over irc last night and i had to fight not to yawn reading that tweet
01:36:34 -!- cheater has quit (Ping timeout: 260 seconds).
01:41:40 -!- DH____ has quit (Remote host closed the connection).
02:15:32 -!- DH____ has joined.
02:22:22 <CakeProphet> honestly I've been using try almost as much as if
02:22:30 <CakeProphet> WHY PYTHON.
02:22:35 <ais523> try's a better control construct all round
02:23:03 <ais523> in fact, is try+recursion TC? my guess is yes
02:23:07 <CakeProphet> I guess it's just that exception hierarchies are annoying.
02:23:14 <CakeProphet> ais523: I believe we had a discussion about this once
02:23:15 <ais523> although that's a bit wooly as it doesn't define what sort of data's allowed
02:23:25 <CakeProphet> a language that uses only exception handling with the ability for recursion.
02:24:02 <CakeProphet> also with some new constructs. Like a "lower" keyword to return to a previous exception level. :D
02:24:41 <CakeProphet> and exceptions would essentially be like ADT
02:26:48 <CakeProphet> the difficult part would be fitting IO into this model.
02:27:12 <CakeProphet> without adding something that is not strictly exception handling.
02:27:58 <ais523> clearly we need an unthrow
02:28:06 <ais523> which is a bit like RESUME NEXT from BASIC
02:28:10 <ais523> only with exceptions instead
02:28:43 <CakeProphet> well I think that would similar to what lower does.
02:28:50 <CakeProphet> returns back to the original raise.
02:29:06 <CakeProphet> so you could have an implicit try around the entire program
02:29:23 <CakeProphet> that catches IO exceptions, and then lowers something back.
02:29:29 <CakeProphet> the lower would be the return value of the raise, perhaps?
02:32:33 <olsner> sounds like coroutines
02:32:33 <CakeProphet> it would be similar to functions but backwards. :P
02:32:52 <CakeProphet> up and back down instead of down and back up.
02:34:45 -!- kmc has quit (Quit: Leaving).
02:35:56 -!- azaq23 has quit (Quit: Leaving.).
02:37:16 * CakeProphet will implement this when has a moment.
02:40:52 <CakeProphet> I think having a pattern matching construct along with recursion would allow it to be Turing complete?
02:41:55 -!- oerjan has joined.
02:42:05 <CakeProphet> otherwise I don't think you can branch.
02:42:40 <CakeProphet> oh wait nevermind you could via recursion.
02:42:57 <CakeProphet> and just a regular catch without any kind of special pattern matching.
02:45:59 -!- pikhq_ has joined.
02:46:31 <oerjan> 00:17:56: <Gregor> In Catholicism, the halting problem is believed to be unsolvable for infants who die before baptism.
02:46:35 <oerjan> 00:19:00: <ais523> well, it's unsolvable for most other TC systems...
02:46:47 <oerjan> i am not entirely sure i want a TC system based on dying infants.
02:46:54 <ais523> I don't want one either
02:47:16 <ais523> well, it's a case of "I wouldn't buy such a system if I were offered one"
02:47:27 <ais523> rather than "if such a system already existed, I wouldn't want it to be TC", which seems kind-of irrelevant
02:47:49 <oerjan> important clarification, that.
02:49:20 -!- pikhq has quit (Ping timeout: 260 seconds).
02:49:58 <oerjan> <ais523> clearly we need an unthrow
02:50:14 <oerjan> i thought common lisp conditions were supposed to support that
02:50:19 -!- copumpkin has changed nick to pirateat41.
02:50:20 <ais523> probably they do
02:50:29 <ais523> the concept is a relatively obvious one, and not even particularly eso
02:53:23 <CakeProphet> :(
02:53:32 <CakeProphet> man you guys have such high standards.
02:55:11 <ais523> now I'm trying to work out if "uncatch" is a sane and useful concept (outside the concept of Feather, where everything's sane by comparison and I have no idea what would be useful)
02:56:07 <CakeProphet> I believe an uncatch would negate a catch below it?
02:56:10 <oerjan> um isn't uncatch just rethrowing?  although if you also have unthrow you'd want a new catch to be able to unthrow all the way back
02:56:35 <ais523> I was thinking that it should work even after an unthrow
02:56:43 <ais523> as in, you do throw; uncatch;
02:56:46 <oerjan> eek
02:58:09 <oerjan> ais523: i assume that would go up the catch chain until you hit something which _doesn't_ unthrow
02:58:29 <CakeProphet> I'm so confused now.
02:58:39 <ais523> if you remembered a history of throws and catches it might not be so hard
02:58:50 <oerjan> and if there was no unthrow then it wouldn't get to run, so it would essentially be an ununthrow
02:58:54 <ais523> err, I'm confused now too, and this is much less confusing than Feather
02:59:13 <ais523> so we have rethrow = uncatch, and ununthrow which reverses an unthrow?
02:59:33 <ais523> I don't see why you couldn't keep stacking un- prefixes forever and getting meaningful operations
02:59:36 <oerjan> ais523: actually i think it's more subtle than that
02:59:40 <ais523> although whether they were /useful/ would be another matter
03:00:27 <oerjan> in a handler, when you have the option both to rethrow and to unthrow, there's the question of exactly _when_ you discard the unthrow possibility
03:00:48 <ais523> especially because you also have the option to throw an unrelated exception
03:01:06 <oerjan> oh and the option of just exiting at handler level, which probably must discard the unthrow to make sense
03:01:41 <ais523> I take it it doesn't make sense to throw one exception, throw an unrelated exception, then unthrow the first one?
03:01:48 <ais523> and if it does, can you subsequently unthrow the second?
03:01:58 <oerjan> ais523: i was just thinking about that
03:02:06 <oerjan> you'd need an unthrow stack :P
03:02:20 <ais523> so it's OK if you unthrow the second, then the first?
03:02:27 <ais523> I'm beginning to think this is a bit like setjmp in C, with all the restrictions that has
03:02:36 <ais523> and using continuations instead would be how you break the restrictions
03:02:47 <oerjan> heh
03:03:40 -!- pirateat41 has changed nick to copumpkin.
03:04:09 <CakeProphet> well
03:04:13 <CakeProphet> each exception would have its own unthrow stack
03:04:16 <CakeProphet> so, not a problem.
03:04:43 <oerjan> CakeProphet: er, it's when you mix exceptions you need an unthrow stack
03:05:14 <CakeProphet> oh, well then the exception would just have an unthrow pointer...
03:05:23 <CakeProphet> you unthrow the exception, control goes back to where it was thrown.
03:05:28 <CakeProphet> done.
03:06:01 -!- ive has joined.
03:06:12 <oerjan> CakeProphet: but we have the option of having an explicitly manipulatable unthrow stack which the other functions can be written in terms of...
03:06:28 <CakeProphet> wait, there are functions in this language?
03:06:29 <CakeProphet> :P
03:06:43 <oerjan> i didn't know we were discussing a particular language
03:06:45 <Jafet> This can probably be easily expressed with continuations.
03:07:07 <Jafet> Although, what continuation can be sensibly thrown is another question.
03:07:25 -!- Jafet has quit (Read error: Connection reset by peer).
03:08:03 -!- lambdabot has joined.
03:08:07 -!- Jafet has joined.
03:08:15 <oerjan> (1) perform a command while pushing current continuation to unthrow stack.  the command may or may not do any throwing.  (2) pop unthrow stack, discarding it.  (3) pop unthrow stack, returning to continuation.
03:08:36 <oerjan> (4) throw an exception.
03:08:46 <Jafet> ...perhaps one that takes a replacement for whatever-value-caused-the-problem as its parameter.
03:08:54 <oerjan> then the _usual_ way to throw an exception would be combining (1) and (4)
03:09:03 <Jafet> Well, the stack is an implementation detail.
03:09:12 <oerjan> oh wait.  this doesn't support uncatch.
03:09:14 <CakeProphet> not really sure it's necessary...
03:09:49 <oerjan> Jafet: actually i'm here mostly making the stack explicit in a vain hope of making the semantics understandable
03:10:15 <CakeProphet> throw/unthrow/catch is really really simple.. :P
03:10:36 <CakeProphet> uncatch I'm not too clear on.
03:10:37 <oerjan> but if there are enough options, you'd surely end up with enough power to explicitly manipulate the stack.
03:10:38 <Jafet> By "unthrow", I presume you mean "go back to where the exception occurred and continue".
03:10:43 <CakeProphet> yes.
03:10:43 <oerjan> Jafet: yeah
03:11:05 <Jafet> But how would you continue? An error just occurred.
03:11:13 <CakeProphet> ...they're not errors
03:11:22 <Jafet> Okay, which language is this
03:11:26 <CakeProphet> it isn't one.
03:11:28 <CakeProphet> not yet.
03:11:35 <oerjan> CakeProphet: IT'S NOT ENOUGH UNTIL YOU CAN DO PROLOG IN THE EXCEPTION SYSTEM
03:11:37 * CakeProphet is going to make basic implementation with throw/unthrow/catch
03:11:44 <oerjan> (including cut)
03:11:45 <CakeProphet> oerjan: UNECESSARY
03:11:49 <Jafet> But exceptions are usually used to signal errors, so you need some way to continue that doesn't cause the error again
03:11:54 <CakeProphet> I posit that  the throw/unthrow/catch is easily
03:11:57 <CakeProphet> Turing complete.
03:12:16 <copumpkin> fuck turing completeness
03:12:17 <Jafet> I suggest returning a continuation that replaces the thing that caused the error, if applicable
03:12:25 <CakeProphet> provided that catch is a recursive control flow statement.
03:12:37 <CakeProphet> Jafet: that's the idea, except it's not really a continuation.
03:12:54 <CakeProphet> just a.. value. an exception
03:13:02 <CakeProphet> you replace the throw with an exception
03:13:04 <CakeProphet> everything is exceptions.
03:13:11 <CakeProphet> which are, in my implementation, essentially ADTs
03:13:24 <CakeProphet> *future implementation
03:13:28 <oerjan> Jafet: note that common lisp actually _does_ support something like unthrow, afair
03:14:18 <oerjan> Jafet: presumably however, each type of exception would contain enough information to tell whether it could be safely continued from
03:14:38 <Jafet> I'm confused by CakeProphet already. That's good, right?
03:14:39 <oerjan> so probably fatal errors wouldn't have the option
03:14:51 <CakeProphet> well, fatal errors could just be pre-defined
03:14:59 <oerjan> Jafet: i haven't got around to reading him yet :P
03:15:01 <CakeProphet> and then if you unthrow: undefined behavior.
03:15:36 <Jafet> Just make it impossible to name the type of a fatal error, so the programmer can't ever handle one.
03:15:45 <CakeProphet> well, that's an option.
03:16:21 <oerjan> CakeProphet: note that all of this tends to be complicated if you have asynchronous exceptions and need to worry about exactly when to reinstall exception handlers
03:16:33 <oerjan> (and that's even without unthrow, i take)
03:16:42 <CakeProphet> ...asynchronous exceptions?
03:16:55 <oerjan> CakeProphet: ghc allows throwing exceptions into other threads :P
03:17:06 <CakeProphet> ah
03:17:08 <oerjan> (i don't think it allows unthrow though)
03:17:21 <CakeProphet> well, hmmm.. I'm sure something could be workd out. :P
03:17:28 <CakeProphet> that can be worried about later.
03:17:29 <Jafet> To unthrow, you'd have to wrap everything in the Cont type or something
03:17:41 <Jafet> Perhaps static typing should be left out of your project
03:17:43 <CakeProphet> ...I really don't see a need for explicit continuations.
03:17:52 <oerjan> CakeProphet: oh and the worry of when to reinstall handlers applies regardless
03:18:10 <oerjan> (what happens if your handler has an error)
03:18:35 <CakeProphet> same thing that happens in any other code
03:18:40 <CakeProphet> >_>?
03:18:45 <CakeProphet> I am not seeing the problem.
03:19:11 <oerjan> CakeProphet: um it's a common problem when actually _using_ exceptions handlers.
03:21:31 <CakeProphet> ...well when you throw an exception in a handler it would just rise up to the next handler.
03:21:47 <oerjan> <Jafet> Just make it impossible to name the type of a fatal error, so the programmer can't ever handle one. <-- erm i didn't mean fatal in the sense you couldn't handle them further up, just fatal in the sense you cannot reasonably continue from them.  actually i'm not sure there is a real difference.
03:23:30 <oerjan> CakeProphet: yes but you might want to install a temporary handler for your handler.  and then _still_ be able to unthrow the original.  but i guess that can be worked out with ordinary control flow.
03:23:34 <Jafet> Every exception should be revertable! Design the language to enforce this.
03:23:53 <Jafet> Except, maybe, really really fatal errors.
03:24:14 <CakeProphet> ProgramWasStabbedToDeathException
03:24:24 <oerjan> CPUOnFireException
03:24:54 <CakeProphet> prepareWaterBalloonCatapult
03:25:06 <CakeProphet> see, you can recover from that.
03:25:10 <oerjan> O KAY
03:27:38 <ais523> SIGKILL is really, really fatal in most Unices, as there's no way to block or handle it
03:27:57 <ais523> oerjan: Java allows throwing exceptions at other threads too
03:28:03 <ais523> but decided that was a bad idea after a while
03:28:15 <oerjan> heh
03:28:37 <CakeProphet> threads are for ninnies
03:41:28 <pikhq_> Yeah, you should only use ucontext.
03:48:01 <oerjan> APPLICATION USAGE None.
03:48:20 <oerjan> pikhq_: man page disagrees with you
03:48:21 <Patashu> forget throwing exceptions at other threads, I want to throw exceptions across the network
03:49:30 <oerjan> posix/botnet.h bn_throw_exception
03:49:45 <Patashu> \o/
03:49:45 <myndzi>   |
03:49:46 <myndzi>   |\
03:51:27 <ais523> hmm, sounds like another feature for my hypothetical INTERCAL IRC client
03:51:33 <ais523> along with CTCP SWAPNICK
03:51:46 <ais523> that basically just swaps the I/O handles so each client is now controlling the other's connection
03:53:46 <Patashu> haha
03:54:00 <CakeProphet> The "else" here seems idiotic to me. If I have statements A and B in my "try" block, and C in my "else" block, how does that differ from having A, B and C in the "try" block? —Preceding unsigned comment added by 192.91.171.42 (talk) 20:06, 16 March 2010 (UTC)
03:54:09 <CakeProphet> ...lol
03:54:25 <Patashu> how indeed
03:54:27 <CakeProphet> 192.91.171.42 is perhaps not that smart.
03:54:53 <Patashu> else is like finally except it only runs on an exception? or?
03:54:58 <ais523> does the else block, in whatever language was on that page, run if an exception isn't caught?
03:55:02 <CakeProphet> yes.
03:55:05 <ais523> also, IP addresses starting 192 confuse me
03:55:06 <CakeProphet> Ruby and Python have it.
03:55:23 <ais523> are there general-purpose 192 addresses as well as all the special-cased ones?
03:55:32 <CakeProphet> I have no idea.
03:55:50 <CakeProphet> but anyways, the difference is that the else clause does not trigger any of the exception handlers.
03:55:59 <CakeProphet> so that you don't catch anything you don't want to catch.
03:56:48 <oerjan> ah so it is run _only_ if no exception is raised
03:56:54 <CakeProphet> correct.
03:57:29 <CakeProphet> I'm actually surprised that very few languages have that.
03:57:32 <oerjan> or wait, what if there is one but no handler matches
03:57:37 <CakeProphet> though I suppose putting everything in the try block is mostly equivalent.
03:57:52 <CakeProphet> I don't believe Python allows try-else
03:58:21 <CakeProphet> the two forms are try-finally and try-except[-else-[finally]]
03:58:53 <Patashu> http://en.wikipedia.org/wiki/Exception_handling_syntax#Python
03:59:06 <CakeProphet> ...yes that's the article whose talk page I just read.
03:59:11 <Patashu> yup
04:01:34 <CakeProphet> you'll note that Perl
04:01:47 <CakeProphet> 's exception handling system is absolutely silly.
04:02:02 <oerjan> also that ' is ridiculously close to return
04:02:15 <Patashu> wow, you have to eval {} for perl exceptions
04:02:27 <CakeProphet> well eval {} is a special case.
04:02:31 <CakeProphet> it's not quite the same as eval "code"
04:02:54 <Patashu> aah
04:03:05 <CakeProphet> eval { } is basically "run this and ignore errors"
04:03:22 <CakeProphet> but everything is parsed at compiletime
04:03:26 <CakeProphet> unlike eval "code"
04:03:51 <CakeProphet> $fail = not eval {
04:03:51 <CakeProphet> lol
04:04:03 <pikhq_> So it's a syntactic oddity, not a semantic one?
04:04:13 <CakeProphet> I suppose.
04:04:26 <CakeProphet> the semantic oddity is weird scoping rules. as the article mentions.
04:04:31 <CakeProphet> you have to dynamically scope $@
04:05:21 <CakeProphet> er... well, you don't always have to.
04:05:51 <CakeProphet> in any case I never use that. :P I've used eval once to import something that was entirely optional
04:06:22 <CakeProphet> in Perl most "error handling" is to ignore the error and return undef
04:06:53 <CakeProphet> close(FILE) || die "Could not close $file"
04:07:25 <Patashu> when would you not be allowed to close a file?
04:07:32 <CakeProphet> also the Haskell example looks a little bit ugly
04:07:43 <CakeProphet> Patashu: if it had already been closed I believe.
04:07:59 <CakeProphet> I don't understand the explicit type signatures...
04:08:08 <Patashu> that's silly though, it's not like a double free, it's not dangerous
04:08:41 <CakeProphet> >>> x = open ("test", "w")
04:08:41 <CakeProphet> >>> x.close()
04:08:42 <CakeProphet> >>> x.close()
04:08:44 <pikhq_> Still an error condition.
04:08:45 <CakeProphet> Python apparently agrees.
04:08:57 <CakeProphet> and Python thinks everything is dangerous and should raise exceptions. :P
04:10:15 <CakeProphet> I have honestly never tried to close a file twice
04:10:19 <CakeProphet> so I have no idea what happens in most languages.
04:10:41 <Patashu> Double_file_closing_syntax
04:10:44 <Patashu> Gogogo
04:11:25 <CakeProphet> dClose = (>>) `on` hClose
04:11:56 <monqy> not quite
04:11:57 <Patashu> Is there a language where you can type file.close().close()
04:12:38 <CakeProphet> :t on
04:12:39 <lambdabot> forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
04:13:04 <CakeProphet> dClose = join . (>>) `on` hClose
04:13:07 <CakeProphet> :P
04:13:45 <monqy> I'm not so sure about that either
04:13:52 <monqy> :t join . (>>) `on` hClose
04:13:54 <lambdabot> Not in scope: `hClose'
04:13:56 <monqy> oops
04:14:25 <monqy> :t join . (>>) `on` (undefined :: String -> Maybe ())
04:14:27 <lambdabot>     Occurs check: cannot construct the infinite type: b = b -> a
04:14:27 <lambdabot>     Probable cause: `>>' is applied to too few arguments
04:14:27 <lambdabot>     In the second argument of `(.)', namely `(>>)'
04:14:36 <monqy> what I suspected
04:14:44 <monqy> also, two issues
04:15:15 <monqy> but I'm guessing you meant
04:15:18 <CakeProphet> :t join . ((>>) `on` (undefined :: String -> Maybe ()))
04:15:19 <lambdabot>     Couldn't match expected type `Maybe (Maybe ())'
04:15:19 <lambdabot>            against inferred type `String -> Maybe ()'
04:15:19 <lambdabot>     Probable cause: `on' is applied to too few arguments
04:15:25 <monqy> you don't want composition
04:15:29 <monqy> you want application
04:15:30 <monqy> ???
04:15:30 <CakeProphet> :t join ((>>) `on` (undefined :: String -> Maybe ()))
04:15:30 <lambdabot> String -> Maybe ()
04:15:35 <CakeProphet> ...right
04:16:35 <CakeProphet> ...well that was productive.
04:16:53 <CakeProphet> @pl test
04:16:53 <lambdabot> test
04:17:17 <CakeProphet> @pl \x -> hClose x >> hClose x
04:17:17 <lambdabot> liftM2 (>>) hClose hClose
04:17:28 <oerjan> <CakeProphet> also the Haskell example looks a little bit ugly <-- the nested catch'es because it is catching two different exception types.  there's a function catches which takes a list of handlers but it requires them to be wrapped with Handler.
04:17:43 <oerjan> *is because
04:18:11 <oerjan> and also it's making Int and Double into exception types on the fly.
04:22:39 <oerjan> <CakeProphet> I don't understand the explicit type signatures... <-- oh right haskell uses type hackery to allow _any_ type to be used as an exception if it has an Exception instance.  but this requires type signatures for catch to know which exceptions you are intending to catch.
04:23:23 <oerjan> @hoogle Control.Exception.catch
04:23:24 <lambdabot> Control.Exception catch :: Exception e => IO a -> (e -> IO a) -> IO a
04:23:24 <lambdabot> Control.Exception.Base catch :: Exception e => IO a -> (e -> IO a) -> IO a
04:23:24 <lambdabot> Control.Exception catches :: IO a -> [Handler a] -> IO a
04:26:08 <oerjan> the Exception class is quite clever, it essentially allows you to make a new type a subtype of another for exception purposes.
04:26:47 <oerjan> (http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.4.0.0/Control-Exception.html)
04:28:56 <oerjan> <monqy> oops <-- a tip when using :t with variables it doesn't know is to put ? in front of them to make them implicit parameters.
04:29:03 <oerjan> :t ?s + ?t
04:29:05 <lambdabot> forall a. (?s::a, ?t::a, Num a) => a
04:30:01 * oerjan feels monologuing
04:30:36 <oerjan> this is just about the point when there would be a netsplit
04:48:13 <CakeProphet> !perl split net
04:49:21 -!- zzo38 has joined.
04:50:07 <zzo38> They said in live theatre that still picture photography is permitted, but video camera and tape recorder is not allowed. But, is shorthand allowed?
04:51:15 <oerjan> zzo38: it probably is not a big enough problem for them to care about it
04:52:51 <zzo38> If you learn shorthand, are you going to record a live show or a movie by shorthand?
04:53:18 <zzo38> And then, you can transcribe it into the computer when you go home.
04:53:45 -!- CakeProphet has quit (Ping timeout: 252 seconds).
05:27:25 -!- tiffany has quit (Ping timeout: 246 seconds).
05:40:35 -!- DH____ has quit (Read error: Connection reset by peer).
05:40:39 -!- DHeadshot has joined.
05:41:55 -!- CakeProphet has joined.
05:41:56 -!- CakeProphet has quit (Changing host).
05:41:56 -!- CakeProphet has joined.
05:46:28 <Sgeo> http://www.barnesandnoble.com/s/Capital%20in%20Disequilibrium?store=ebook
05:46:28 -!- DHeadshot has quit (Read error: Connection reset by peer).
05:46:35 <Sgeo> Just... the price disparity
05:46:40 <Sgeo> For the same book
05:46:46 -!- DH____ has joined.
05:47:21 <Sgeo> (Warning: mises stuff)
05:48:46 -!- MDude has quit (Ping timeout: 246 seconds).
05:50:03 <CakeProphet> !wacro
05:50:04 <EgoBot> TCCDP
05:50:40 <CakeProphet> Turing-Complete Consensual Double Penetration
05:55:30 -!- Vorpal has joined.
05:59:49 <CakeProphet> > (+) <$> [1..10] <*> [1..10]
05:59:51 <lambdabot>   [2,3,4,5,6,7,8,9,10,11,3,4,5,6,7,8,9,10,11,12,4,5,6,7,8,9,10,11,12,13,5,6,7...
06:00:06 <CakeProphet> > (+) <$> [1..3] <*> [1..3]
06:00:07 <lambdabot>   [2,3,4,3,4,5,4,5,6]
06:00:46 <CakeProphet> > sort $ (+) <$> [1..3] <*> [1..3]
06:00:48 <lambdabot>   [2,3,3,4,4,4,5,5,6]
06:00:56 <CakeProphet> > sort $ (+) <$> [1..5] <*> [1..5]
06:00:58 <lambdabot>   [2,3,3,4,4,4,5,5,5,5,6,6,6,6,6,7,7,7,7,8,8,8,9,9,10]
06:01:35 <CakeProphet> oerjan: is there some sort of theoretical mathematics behind this?
06:02:45 <CakeProphet> > map length . group . sort $ (+) <$> [1..5] <*> [1..5]
06:02:47 <lambdabot>   [1,2,3,4,5,4,3,2,1]
06:02:55 <oerjan> CakeProphet: it's far too simple to be considered theoretical.
06:03:09 <CakeProphet> I mean is there some kind of property of abstract algebra.
06:03:14 <oerjan> also, anyone who has ever played a dice game with two dice should understand this...
06:03:34 <pikhq_> :t (<*>)
06:03:35 <lambdabot> forall (f :: * -> *) a b. (Applicative f) => f (a -> b) -> f a -> f b
06:03:39 <pikhq_> ^ Hint
06:03:54 <CakeProphet> pikhq_: huh?
06:04:16 <oerjan> CakeProphet: look at a 5*5 square.  consider the lengths of the diagonals.
06:04:36 <pikhq_> "That's just what the Applicative [a] instance means, silly."
06:04:57 <oerjan> (chessboard style)
06:05:06 <zzo38> If you wanted to make a Haskell program as a HTML document (although I prefer TeX instead), you could use the <XMP> command in HTML for that purpose, I think.
06:05:22 <CakeProphet> it's not [a] that's applicative here.
06:05:31 <CakeProphet> oerjan: well, right, it makes intuitive sense.
06:05:37 -!- kmc has joined.
06:05:51 <pikhq_> :t (+) <$> [1..10]
06:05:51 <lambdabot> forall a. (Num a, Enum a) => [a -> a]
06:05:53 <CakeProphet> I was hoping maybe I could learn some general abstract nonsense. I guess not. :P
06:05:54 <zzo38> oerjan: Some game with two dice, is, backgammon. But I also played a chess variant using two dice to decide which kind of pieces you are allowed to move on your turn.
06:06:00 <pikhq_> I'm saying "it is".
06:06:13 <oerjan> CakeProphet: now if you were to sum _many_ such lists, each of form [0,1] - then you would have reinvented binomial distribution.
06:06:44 <Lymee> :t <$>
06:06:46 <lambdabot> parse error on input `<$>'
06:06:56 <Lymee> :t (<$>)
06:06:56 <oerjan> > map length . group . sort $ sum <$> replicateM 6 [0,1]
06:06:57 <lambdabot> forall a b (f :: * -> *). (Functor f) => (a -> b) -> f a -> f b
06:06:58 <lambdabot>   [1,6,15,20,15,6,1]
06:07:01 <CakeProphet> pikhq_: oh right..
06:07:14 <Lymee> > (+) <$> (+)
06:07:16 <lambdabot>   Overlapping instances for GHC.Show.Show (a -> (a -> a) -> a -> a)
06:07:16 <lambdabot>    arisin...
06:07:33 <CakeProphet> Lymee: composition
06:08:00 <pikhq_> Lymee: fmap on a->b is just (.)
06:08:07 <pikhq_> (and <$> is a synonym for fmap)
06:08:13 <Lymee> Ah =p
06:08:19 <pikhq_> (and in Caleskell, (.) is a synonym for fmap)
06:09:06 <CakeProphet> > (*) <$> [1..10] <*> [1..10]
06:09:08 <lambdabot>   [1,2,3,4,5,6,7,8,9,10,2,4,6,8,10,12,14,16,18,20,3,6,9,12,15,18,21,24,27,30,...
06:09:27 <CakeProphet> oerjan: I was thinking of it as being similar to a cartesian product as that is what you would  get if you substituted (+) for (,)
06:09:48 <CakeProphet> > (*) <$> [1..4] <*> [1..4]
06:09:50 <lambdabot>   [1,2,3,4,2,4,6,8,3,6,9,12,4,8,12,16]
06:09:55 <oerjan> CakeProphet: oh, you are confused about what <*> means for lists?
06:10:04 <oerjan> i thought you were asking something beyond that.
06:10:05 <CakeProphet> no I know what it means.
06:10:07 <CakeProphet> ...I was.
06:10:12 <Patashu> once upon a time, I did a study on this pattern
06:10:17 <Patashu> it has an interesting self-similarity property
06:10:38 <oerjan> CakeProphet: well yes it is similar to a cartesian product. applying (+) to each element in it.
06:10:42 <Patashu> each extra time you're repeating the operation, it shifts an initial curve to higher derivatives
06:10:46 <CakeProphet> oerjan: something to do with properties of addition that are distinct from say, (,) or other binary operations.
06:10:48 <ais523> isn't that just a multiplication table?
06:10:54 <oerjan> (uncurry (+), technically)
06:12:24 <CakeProphet> oerjan: that give duplicate results in that way when you apply it to a cartesian product.
06:12:28 <oerjan> CakeProphet: oh, well that, (n+1) + (n-1) == n+n so the sum stays constant on each diagonal
06:12:45 <zzo38> Once I did try on paper trying to figure out (x ->) monad and it seem  fmap = (.)
06:13:17 <oerjan> and so simply when you do length . group . sort you are simply calculating the length of each diagonal in a complicated way
06:13:34 <CakeProphet> oerjan: are there other operators that have this characteristic?
06:13:56 <CakeProphet> > (-) <$> [1..4] <*> [1..4]
06:13:58 <lambdabot>   [0,-1,-2,-3,1,0,-1,-2,2,1,0,-1,3,2,1,0]
06:14:15 <CakeProphet> > sort $ (-) <$> [1..4] <*> [1..4]
06:14:16 <lambdabot>   [-3,-2,-2,-1,-1,-1,0,0,0,0,1,1,1,2,2,3]
06:14:27 <CakeProphet> that one does. :P
06:14:34 <oerjan> CakeProphet: f(n+k, n-k) == f(n,n) means f(m,n) == f(m+n,0).  so only things that are themselves functions of m+n
06:14:54 <CakeProphet> ah, okay.
06:15:00 <oerjan> CakeProphet: oh right, (-) gives the diagonals the _other_ way
06:15:27 <oerjan> (n+k)-(m+k) == n-m
06:15:29 <CakeProphet> oerjan: also it's a function of m+n
06:15:30 <CakeProphet> right
06:15:43 <oerjan> CakeProphet: um -
06:15:59 <oerjan> *um m-n isn't a function of m+n
06:16:34 <CakeProphet> m - n = m + (-n)   ?   or does that not count?
06:18:17 <Patashu> @oerjan: http://pastebin.com/D5JHEyeM
06:18:18 <lambdabot> Unknown command, try @list
06:18:23 <Patashu> thanks for helping me understand it
06:18:56 <oerjan> CakeProphet: no, that does not count.  you are essentially doing a mirror reflection of the n direction, which as i said makes the diagonals go the other direction.
06:19:11 <CakeProphet> oh okay.
06:19:15 <oerjan> there is no function f such that m-n = f(m+n).
06:19:55 <CakeProphet> > (.&.) <$> [1..4] <*> [1..4]
06:19:57 <lambdabot>   Ambiguous type variable `a' in the constraints:
06:19:57 <lambdabot>    `Data.Bits.Bits a'
06:19:57 <lambdabot>      ...
06:20:15 <CakeProphet> > (.&.) <$> ['a'..'d'] <*> ['a'..'d']
06:20:16 <lambdabot>   No instance for (Data.Bits.Bits GHC.Types.Char)
06:20:17 <lambdabot>    arising from a use of `D...
06:20:25 <CakeProphet> er.
06:20:35 <CakeProphet> Haskell isn't C?
06:20:48 <CakeProphet> what do?
06:21:12 <oerjan> add a type signature
06:21:21 <oerjan>  > (.&.) <$> [1..4] <*> [1..4] :: [Int]
06:21:53 <oerjan> er
06:21:57 <oerjan> > (.&.) <$> [1..4] <*> [1..4] :: [Int]
06:21:58 <lambdabot>   [1,0,1,0,0,2,2,0,1,2,3,0,0,0,0,4]
06:23:23 <CakeProphet> > (.|.) <$> [1..4] <*> [1..4]
06:23:25 <lambdabot>   Ambiguous type variable `a' in the constraints:
06:23:25 <lambdabot>    `Data.Bits.Bits a'
06:23:25 <lambdabot>      ...
06:23:27 <oerjan> CakeProphet: lambdabot apparently doesn't use extended defaulting, so if you include a class it doesn't know, it refuses to try.
06:23:27 <CakeProphet> oh rite
06:23:35 <CakeProphet> > (.|.) <$> [1..4] <*> [1..4] :: [Int]
06:23:36 <lambdabot>   [1,3,3,5,3,2,3,6,3,3,3,7,5,6,7,4]
06:23:53 <CakeProphet> 3 seems to be the favorite. :P
06:24:25 <oerjan> erm s/know/know from the haskell report, where for some stupid reason the Random class seems to have been excluded in ghc, i think that's a bug/
06:24:42 <fizzie> > xor <$> [1..4] <*> [1..4] :: [Int]
06:24:43 <lambdabot>   [0,3,2,5,3,0,1,6,2,1,0,7,5,6,7,0]
06:24:46 <fizzie> (Just for completeness.)
06:24:54 <zzo38> Is there a such thing as (x ->) monad?
06:25:06 <oerjan> zzo38: yes, import Control.Monad.Reader
06:25:37 <oerjan> it's isomorphic to the Reader Monad, so defined there
06:25:58 <oerjan> > join (+) 2 -- lambdabot has it automatically imported
06:25:59 <lambdabot>   4
06:26:07 <zzo38> OK.
06:26:16 <oerjan> zzo38: also lambdabot's @pl command uses it heavily
06:26:39 <zzo38> I found what I figured out the definition of unit/join/fmap that I made up are in fact the correct ones and the same ones they use.
06:27:39 <zzo38> And in fact it does make sense.
06:28:14 <oerjan> zzo38: also yes fmap = (.) for that monad/functor, lambdabot even defines (.) = fmap as one of its "caleskell" modifications
06:28:16 <zzo38> But "join" really should be a member of the "Monad" class. It is stupid that they don't do it that way!!
06:28:39 <zzo38> oerjan: Yes, that is what I came up with.
06:29:51 <oerjan> zzo38: it's probably because Functor is younger than Monad and no one has implemented the needed subclass defaulting extensions to make that combine without being annoying
06:29:54 <Patashu> Hmmm. Since doing this over and over by the central limit theorem gets you a normal distribution, the normal distribution must be infinitely differentiable
06:30:27 <oerjan> Patashu: pretty sure it is
06:31:15 <zzo38> oerjan: Yes; if they did implement the subclass extensions, it would in fact work much better because you can define a monad in terms of unit/join/fmap or return/bind.
06:31:17 <Patashu> Basically, what I wanted to come up with about a year ago were equations for step 1 towards normal distribution, step 2, step 3, step 4... with step infinity being the normal distribution
06:31:24 <Patashu> So all continuous equations
06:32:11 <zzo38> So that you can have the classes required by constraints have implementations mentioned in both class declarations and in instance declarations for a class.
06:34:25 <CakeProphet> normal distributions are hungry.
06:34:28 -!- cheater has joined.
06:34:52 <CakeProphet> they want to assimilate everything into their normalcy.
06:35:48 <oerjan> Patashu: of course that it's infinitely differentiable is rather obvious from the explicit formula for its density function
06:35:57 <pikhq_> CakeProphet: ASSIMILATE!
06:36:08 <oerjan> even analytic
06:36:27 <Patashu> oerjan: yes, but I figured it out without needing to know that \o/
06:36:31 <Patashu> math is beautiful and all that
06:36:51 <oerjan> yeah
06:39:22 <zzo38> One of my idea about Haskell, is to make ASSUME and PROVE pragma, which can be used with proofs using Curry-Howard but can have other uses, too, such as optimization or checking some properties of the program.
06:41:04 -!- clog has quit (Ping timeout: 260 seconds).
06:41:20 <CakeProphet> zzo38: such as monad laws?
06:41:58 <copumpkin> monad laws: https://github.com/copumpkin/categories/blob/master/Categories/Monad.agda
06:42:47 <zzo38> CakeProphet: Not what I meant, but it might be usable for such things possibly; I don't know. What I mean is that ASSUME means assume the property that for all defined inputs, there is a defined output, while the PROVE pragma checks this property if possible.
06:43:26 <zzo38> I don't know whether this allows checking monad laws, though.
06:44:03 <copumpkin> zzo38: checking things automatically is generally either not possible or in very restricted cases, computationally intractable
06:44:19 <copumpkin> automated theorem proving fields tend to be happy when they find "just" doubly exponential algorithms
06:44:22 <zzo38> (The other idea would be that ASSUME is completely ignored when optimization is turned off except that ASSUME is still used in checking with PROVE)
06:44:23 <CakeProphet> I'd imagine there's some kind of way to apply function definitions until you get from one end of the equality to the other, so to speak.
06:44:48 <CakeProphet> by syntax transformations, rather than explicit input checking.
06:44:49 <zzo38> copumpkin: Yes I know it is not always possible to check. But it is sometimes possible.
06:44:59 <copumpkin> how do you determine when it's possible?! :P
06:45:19 <copumpkin> but yeah, I support automated theorem proving for some things
06:45:21 <CakeProphet> copumpkin: you have a program impatiently press a button when he gets tired of waiting for the answer.
06:45:25 <copumpkin> I just don't think haskell is the place for it
06:45:28 <CakeProphet> s/program/programmer/
06:45:33 <zzo38> For example, it uses no "undefined", it uses no loops, and all functions it calls have that property.
06:45:41 <zzo38> And it has no inexhaustive patterns.
06:45:56 <Patashu> if it doesn't have any of those it's not an interesting case
06:46:15 <copumpkin> you can restrict something to only do structural recursion
06:46:21 <copumpkin> except in haskell things are a lot trickier
06:46:23 <zzo38> It it *does* have those things, then you can have something for doing metatheorems.
06:46:27 <copumpkin> because you frequently deal with infinite data
06:46:46 <zzo38> Or just ASSUME it if you have proved it yourself and do not want to put it in the program.
06:46:58 <CakeProphet> so is syntax transformations not a viable option?
06:47:05 <copumpkin> zzo38: assume = unsafeCoerce
06:47:09 <copumpkin> or undefined :)
06:47:27 <copumpkin> according to the curry-howard correspondence
06:47:30 <zzo38> But ASSUME and PROVE only apply to the functions you tell it to do, not everything.
06:47:56 <copumpkin> how are they different from undefined? and I don't get the point of prove
06:48:13 <zzo38> copumpkin: Yes I have thought of that, too. It allows you to construct proofs in that way. But it won't do with what I proposed having ASSUME and PROVE pragmas.
06:49:02 <zzo38> So that {-# PROVE f #-} checks the property of the function f, and {-# ASSUME f #-} tells it to assume that f has that property for optimization purpose and for PROVE pragmas.
06:49:28 <copumpkin> {-# PROVE f 5 == 6 #-} ?
06:49:50 <copumpkin> you might be interested in http://pauillac.inria.fr/~naxu/research/escH-hw.pdf
06:49:59 <CakeProphet> {-# ASSUME funky #-}
06:50:02 <copumpkin> which does as much checking of haskell as I think is possible
06:50:27 <zzo38> copumpkin: No, I mean check the property, if possible, that the output will always be defined for all defined inputs of the function.
06:50:54 <copumpkin> PROVE doesn't sound like the right name for it, then
06:50:56 <copumpkin> TOTAL
06:51:07 <zzo38> (If it checks successfully, it can also do the same as ASSUME for purpose of optimization.)
06:51:25 <copumpkin> I'm not sure what you mean there
06:51:34 <copumpkin> can you give an example of a case where you'd use them?
06:51:45 <copumpkin> what would the properties look like?
06:51:50 <copumpkin> according to C-H, they're just types
06:53:37 <zzo38> But for the proof to be valid, all functions must have defined outputs for all defined inputs. Otherwise you can write undefined or whatever else like that. You also need to ensure no unsafe functions being used, too.
06:53:45 <copumpkin> oh sure
06:53:48 <copumpkin> that's what TOTAL means
06:54:01 -!- augur has joined.
06:54:06 <zzo38> You could have PROVE pragma can have local assumptions in parentheses, perhaps, if you want to make those assumptions locally.
06:54:18 <copumpkin> I think you should learn agda :)
06:54:30 <copumpkin> just to see what proofs and statements in a total language look like
06:54:35 <copumpkin> if nothing else
06:55:02 <CakeProphet> @src concatMap
06:55:03 <lambdabot> concatMap f = foldr ((++) . f) []
06:55:12 <CakeProphet> @src foldr
06:55:13 <lambdabot> foldr f z []     = z
06:55:13 <lambdabot> foldr f z (x:xs) = f x (foldr f z xs)
06:56:32 <zzo38> Call it TOTAL if you do not like the name PROVE, but what name would you give ASSUME then? Would you keep it same or do differently?
06:56:51 <CakeProphet> :t ((++) . f)
06:56:52 <lambdabot> forall a (f :: * -> *). (Monoid a, SimpleReflect.FromExpr (f a), Functor f) => f (a -> a)
06:57:08 <CakeProphet> @unpl ((++) . f)
06:57:09 <lambdabot> (\ c -> (++) (f c))
06:58:01 <copumpkin> zzo38: I still don't understand the point of ASSUME. You mentioned curry-howard, and the language of propositions in curry-howard is that of types. So I don't see why you need a separate construct for ASSUME instead of just a type. Can you explain what kind of propositions you'd put in it?
06:59:26 -!- ais523 has quit (Remote host closed the connection).
06:59:58 <CakeProphet> 2src (++)
07:00:01 <CakeProphet> @src (++)
07:00:02 <lambdabot> []     ++ ys = ys
07:00:02 <lambdabot> (x:xs) ++ ys = x : (xs ++ ys)
07:00:02 <lambdabot> -- OR
07:00:02 <lambdabot> xs ++ ys = foldr (:) ys xs
07:06:17 <CakeProphet> Monad axioms:
07:06:18 <CakeProphet> Kleisli composition forms
07:06:19 <CakeProphet> a category
07:06:26 <CakeProphet> a beautiful haiku from HaskellWiki
07:06:39 <zzo38> CakeProphet: Yes, I like that.
07:08:55 -!- augur has quit (Ping timeout: 260 seconds).
07:09:12 -!- ive has quit (Quit: leaving).
07:14:07 <zzo38> copumpkin: For example, you write a function you know has the properties required but the computer cannot check. Another use is optimization. And one more use is if you write functions but you are trying to check using assumptions; although in this case you might want local assumptions.
07:15:31 <copumpkin> I keep asking, what is the language of these properties? how do you check them, and how do you incorporate knowledge about things? So far you seem to be waving your hands and saying effectively "automated theorem proving" which is a large and complicated area
07:16:40 <copumpkin> is it just something you know to be true, that can be used as a rewrite rule?
07:16:41 <zzo38> You still have to write most of it yourself, but for example, it checks that you have no inexhaustive patterns, no unsafe functions, no undefined stuff, and that all functions it calls also have that property.
07:16:47 <copumpkin> because GHC already has those
07:16:50 <copumpkin> I thought that was PROVE
07:16:52 <oerjan> copumpkin: it is a required exercise in this channel to invent your own perfect system which looks entirely plausible as long as you keep it only in your head
07:16:53 <copumpkin> or TOTAL
07:17:00 <copumpkin> oerjan: I see
07:17:08 <zzo38> If you need more complicated then you could make up a metatheorems system
07:17:28 <copumpkin> anyway, I still think that before embarking on this journey you should learn a tiny bit of what's already out there
07:17:42 <copumpkin> you mentioned C-H but I'm not getting the impression it has anything to do with it, from what you've said so far
07:17:54 <zzo38> ASSUME just causes it to *assume* these things are true without checking, both for optimization and for proof.
07:18:01 <copumpkin> zzo38: RULE
07:18:23 <copumpkin> http://www.haskell.org/ghc/docs/latest/html/users_guide/rewrite-rules.html
07:18:30 <zzo38> I know about rewrite rules pragma.
07:18:37 <copumpkin> I'm asking, how is it different?
07:20:23 <zzo38> How is it the same?
07:20:46 <copumpkin> you haven't given me any examples of what an actual ASSUME pragma would even look like, so I don't know
07:21:25 <copumpkin> you're hand-waving and saying optimization :P I'm saying it sounds like you can provide equations that your definition satisfies and ask the compiler to optimize based on them, using rules pragmas
07:21:28 <zzo38> It would look like:   {-# ASSUME f #-}   just like that, to assume it for function f.
07:21:34 <copumpkin> assume WHAT?
07:21:43 <copumpkin> that it terminates?
07:22:06 <zzo38> copumpkin: Yes, that it terminates, has no undefined or unsafe, has no inexhaustive patterns.
07:22:30 <copumpkin> does fix (1:) terminate?
07:24:04 <zzo38> That is difficult. Is fix (1:) a valid proof for Curry-Howard?
07:24:19 <copumpkin> it's a proof of [Integer] :)
07:24:29 <Patashu> how could it not terminate?
07:24:40 <copumpkin> also, how do you deal with the paradoxes in Haskell that don't arise from recursion?
07:24:46 <copumpkin> Patashu: it produces an infinite list
07:25:05 <copumpkin> fix is basically the fundamental building block for non-termination
07:25:21 <zzo38> copumpkin: Paradoxes that arise from anything have those kind of things disallowed in a PROVE and assumed that they don't have them in an ASSUME.
07:25:29 <zzo38> Probably "fix" would be disallowed in a PROVE.
07:25:36 <copumpkin> sure
07:25:37 <zzo38> But I don't know a lot about it for sure.
07:25:41 <copumpkin> but x = 1:x
07:25:45 <copumpkin> which is the same as fix (1:)
07:25:59 <copumpkin> that is allowed in agda, for example, but only if your list is codata
07:26:05 <copumpkin> it's productive corecursion
07:26:08 -!- nooga has joined.
07:26:11 <zzo38> copumpkin: That is also recursion because it refers to itself, which I think would also be disallowed
07:26:32 <copumpkin> almost all interesting programs will have some form of recursion in them
07:26:43 <copumpkin> theorem provers force you to write structural recursion usually
07:26:53 <copumpkin> because it's clear that they terminate
07:26:57 <zzo38> That is, "fix" is disallowed unless you specifically allow it with {-# ASSUME fix #-} or with a local assumption.
07:27:55 <zzo38> copumpkin: Yes, you could have some that are clear to terminate; you might also be able to have a metatheorems system to write your own proofs of termination and nonparadoxes
07:28:10 <copumpkin> why even bother doing this in haskell though?
07:28:21 <copumpkin> the language of those proofs is going to be a completely different language
07:28:27 <copumpkin> in agda, you get it as your basic language
07:28:34 <copumpkin> in haskell, also
07:28:38 <zzo38> (You cannot do this more than one level though; I think Godel's Theorem or whatever prevents it)
07:28:42 <copumpkin> what is the benefit of guaranteed terminating functions?
07:29:26 <CakeProphet> copumpkin: what makes it clear? Are they explicitly typed so that it can be determined that they terminate at compiletime?
07:29:29 <zzo38> Of course not all functions have to be; your program can contain such functions just fine. But to check them with these kind of pragmas it would not work if you have things the computer won't check
07:29:54 <copumpkin> CakeProphet: yes, but what makes it clear is that there's a (t least one) data constructor being consumed for every recursive call
07:29:56 <zzo38> That is, you only use the pragmas on some functions, not all of them.
07:30:12 <copumpkin> CakeProphet: for example f (x : xs) = blah (f xs) is fine
07:30:15 <CakeProphet> copumpkin: ah so no laziness here.
07:30:20 <copumpkin> f (x : xs) = blah (f (x : xs)) is not
07:30:25 <copumpkin> CakeProphet: no, there can be laziness
07:30:37 <copumpkin> whether it's lazy or not is an implementation detail
07:30:51 <copumpkin> zzo38: I mean, what kind of benefit does annotating functions this way give you?
07:31:38 <CakeProphet> copumpkin: ...but that wouldn't terminate for a lazy infinite list.
07:32:02 <copumpkin> CakeProphet: yes, there's an explicit separation between data (finite things) and codata (potentially infinite things)
07:32:09 <zzo38> copumpkin: In a proof program, to make the compiler check your proof. In other programs, to use with local assumptions to check certain properties locally.
07:32:15 <copumpkin> CakeProphet: and the safeness conditions are different for them
07:32:20 <CakeProphet> ah
07:32:28 <copumpkin> zzo38: but your language for writing proofs is horrible, in haskell
07:32:42 <copumpkin> I've written proofs about basic natural arithmetic in haskell and it's really painful
07:32:58 <copumpkin> proving anything remotely useful is completely out of the question
07:33:04 <copumpkin> especially since we don't have dependent types
07:33:05 <zzo38> copumpkin: Really? It seem, if you have the (x ->) monad then you can use do-notation.
07:33:21 <copumpkin> I don't follow :)
07:34:27 <CakeProphet> I do believe you could prove the monad laws through a combination of step-by-step syntactic transformations and pattern matching.
07:34:35 <CakeProphet> for an individual instance
07:34:52 <zzo38> And it automatically gives you the fantasy rule if you do that too, I think.
07:35:19 <CakeProphet> return a >>= f = concatMap f [a] = foldr ((++).f) [] [a] = ...
07:35:42 <copumpkin> zzo38: for example
07:35:44 <oerjan> do-notation in the (x ->) monad as a replacement for the decision theorem, check.
07:35:45 <copumpkin> say you just wrote addition
07:35:52 <copumpkin> oerjan??
07:36:15 <copumpkin> zzo38: so you just defined (+). Now you want to prove that it's commutative. But first you must state that it's commutative. How do you do that?
07:36:45 <oerjan> copumpkin: the (x ->) monad could sort of work as a way to hide assumptions in your proof terms...
07:36:55 <oerjan> i think.
07:36:59 <copumpkin> except your proof terms are all trivial
07:37:05 <zzo38> oerjan: What is decision theorem? Sorry I don't know what that is?
07:37:51 <oerjan> zzo38: it's a metatheorem of logic with says that if you prove B from assumptions A1,A2,... then you can prove A1 -> A2 -> ... -> B
07:38:13 <copumpkin> anyway
07:38:19 <zzo38> copumpkin: I don't know, but I do know how to write it in TNT. But how can you make TNT with Curry-Howard? I don't know that either. That is why I want to learn.
07:38:21 <copumpkin> you'd state your commutative theorem
07:38:22 <oerjan> and i think you could sort of extract one of the A's into an (x ->) monad
07:38:31 <copumpkin> forall x y. x + y == y + x
07:38:45 <copumpkin> that would be your proposition to prove
07:39:14 <CakeProphet> zzo38: I believe you need toluene, sulfuric acid, and nitric acid
07:39:20 <copumpkin> that kind of type can only be awkwardly translated to haskell
07:39:23 <copumpkin> because it's dependent
07:39:29 <CakeProphet> zzo38: I'm not sure if Curry-Howard will help you with acquiring those things though.
07:39:43 <copumpkin> and the only place you can depend on parameters in haskell is for type-level parameters
07:39:50 <copumpkin> which means your addition needs to be over type-level naturals
07:39:51 <zzo38> TNT here is short for Typographical Number Theory, though.
07:39:58 <copumpkin> and that needs to be type-level equality
07:40:02 <zzo38> copumpkin: I have done type-level natural numbers.
07:40:21 <copumpkin> zzo38: that's fine. Do you know what a proof of that would look like?
07:40:37 <copumpkin> you'd proceed by induction over one or both of the arguments
07:40:42 <copumpkin> except you can't do that in haskell
07:40:46 <copumpkin> because they're types
07:40:54 <copumpkin> so you need to hack it in with a typeclass
07:41:05 <zzo38> I do know what a proof of it looks like in TNT.
07:41:12 <copumpkin> forall x y. (Nat x, Nat y) => x :+ y :== y :+ x
07:41:21 <copumpkin> that's what the actual statement would look like
07:41:36 <copumpkin> proofs of simple things like commutativity in haskell can be done
07:41:42 <copumpkin> but they're proofs over things people don't typically work with
07:41:47 <copumpkin> type-level naturals
07:41:48 <zzo38> And I have tried using classes too. But, it seems some things it will ignore anyways
07:42:02 <copumpkin> when I write a program I'm not writing a list of type-level numbers
07:42:07 <copumpkin> I'm writing a value-level list
07:42:13 <copumpkin> and haskell gives me no way to say anything about that list
07:42:22 <copumpkin> (except very slightly with GADTs)
07:42:53 <copumpkin> the reason anyone who cares about writing proofs uses dependent types is that they let you state and prove most things you care about in your program
07:43:00 <copumpkin> since you _can_ actually make statements about values
07:43:06 <copumpkin> that's why I keep pushing you towards agda :P
07:43:17 <copumpkin> that also checks for you that all your functions terminate
07:43:21 <copumpkin> and warns you if it can't see that they do
07:43:30 <copumpkin> so you can still write functions that don't obviously terminate
07:43:45 <copumpkin> but by default it checks
07:44:29 <CakeProphet> does a brainfuck interpreter obviously terminate? :P
07:44:33 <copumpkin> no
07:44:34 <CakeProphet> that would be pretty amazing if it did.
07:44:54 <copumpkin> there's no (obvious) succinct way to state a checkable termination condition
07:45:01 <CakeProphet> copumpkin: so wait, adga /can't/ solve the halting problem?
07:45:04 <CakeProphet> why do I want it then?
07:45:10 <copumpkin> ?
07:45:14 <monqy> ?
07:45:17 <CakeProphet> :?
07:45:19 <zzo38> I did make type-level natural numbers using type families.
07:45:19 <copumpkin> terminating agda isn't turing-complete
07:45:29 <copumpkin> it's conservative
07:45:45 <copumpkin> it might warn you that a terminating function doesn't terminate because its simple condition isn't accurate
07:45:56 <copumpkin> but it won't ever decide that a non-terminating function does terminate
07:46:32 <copumpkin> but because of that, you can trust proofs in it
07:46:48 <copumpkin> it also makes you realize how overrated turing-completeness is
07:47:40 <zzo38> That is why you don't want Agda. But you might want to use some of their features in Haskell, but not always. However there are things neither of these have but then there can be other extensions, including type families and other stuff too.
07:47:56 <copumpkin> what is why you don't want it?
07:48:18 <copumpkin> I actually think agda's default is the better one
07:48:23 <zzo38> There could be some way converting between type-level programming and value-level programming, probably with some restrictions.
07:48:45 <zzo38> copumpkin: Are you sure? I don't agree but that is just my opinion.
07:49:03 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net).
07:49:06 <copumpkin> why do you disagree?
07:49:16 <copumpkin> I'm not even sure what you dislike about it? :P
07:49:30 <zzo38> In most cases you do not want such restrictions.
07:49:37 <copumpkin> as I said
07:49:44 <copumpkin> all it does is warn you if you don't meet them
07:49:51 <copumpkin> it doesn't stop you from writing such functions
07:50:31 <copumpkin> and regardless of whether you think it's practical
07:50:37 <copumpkin> if you want to talk to people about proofs
07:50:46 <copumpkin> they're not going to take you seriously if you don't understand how proofs work :)
07:50:50 <copumpkin> and what is needed to construct them
07:50:58 <zzo38> But if you have a PROVE pragma like I described, it would check other functions it calls, too, not necessarily all cases of those other functions. (And it would be error rather than warning, allowing you to speed up the compiler, as well as a few other things.)
07:51:19 <copumpkin> yes, but _what_ can you prove in haskell?
07:52:02 <zzo38> I do have a proof in a book on the table in front of me, of commutative addition, in TNT.
07:52:06 -!- oerjan has quit (Quit: Later).
07:52:10 <copumpkin> its type system isn't expressive enough to even state, let alone prove anything that might be useful to an optimizer
07:52:16 <copumpkin> TNT is not haskell
07:52:32 <zzo38> One thing I want to learn is to be able to make TNT with Curry-Howard if there is some way.
07:52:53 <copumpkin> I think you're missing a key part of this
07:53:12 <copumpkin> you can't write forall or exists in haskell
07:53:24 <copumpkin> its type system doesn't allow it
07:53:39 <copumpkin> that's in fact the main distinguishing characteristic between its type system and agda's
07:53:51 <zzo38> O, I thought you could make up some things with it somehow
07:54:14 <copumpkin> you can, but by hacking at the type level, and doing so is extremely painful and indirect
07:54:27 <copumpkin> but most things people care about aren't at the type level
07:54:38 <copumpkin> if I want to say a list is sorted
07:54:44 <copumpkin> or addition is commutative
07:54:52 <copumpkin> or anything more interesting than that
07:54:54 <copumpkin> I need to say forall
07:55:06 <copumpkin> forall numbers x and y, x + y == y + x
07:56:02 <copumpkin> that forall gives you basically boundless power to state theorems
07:56:16 <copumpkin> and makes the type system simpler in many ways
07:56:23 <copumpkin> and more complicated in many others
07:56:35 <copumpkin> anyway, gotta sleep now
07:56:47 <copumpkin> but if you want something like haskell but with more type-level goodness
07:56:59 <copumpkin> check out http://lambda-the-ultimate.org/node/4088
07:57:31 <zzo38> OK I will look
08:05:17 <zzo38> GHC has GADTs, type families, and other stuff, too. I was making preprocessor for Haskell, which does things including anonymous macros and other features, maybe I can put some of these kind of type-level stuff too. However, note this program does not accept layout mode and I do not plan to add it (although you can add it in yourself if you want to, or do whatever else you want to it)
08:06:58 <zzo38> Such as, if you write 3 in a type context it will replace it with (Succ (Succ (Succ Zero)))
08:15:42 -!- zzo38 has quit (Remote host closed the connection).
08:50:04 <CakeProphet> Python topic line says "NO LOL"
08:50:09 <CakeProphet> I wonder if they enforce that.
08:50:13 <CakeProphet> s/Python/#python/
08:51:18 <Jafet> Yes.
08:51:38 <Jafet> It raises the channel mean IQ, if only by a little.
08:52:09 <fizzie> "NO LOL | NO PROJECT EULER | ..." it said when I /list'd few weeks ago to pick some new channels.
08:52:29 -!- clog has joined.
08:52:34 <CakeProphet> Jafet: lol
08:52:44 <fizzie> Strange things to prohibit, lol.
08:53:32 <Jafet> Not really; python is full of lol.
08:53:37 <CakeProphet> More proof that pythonistas are actually jerks, lol.
08:56:19 <cheater> yes they do
08:56:33 <cheater> if you go in there and say LOL you get banned after 1 warning
08:56:43 <fizzie> http://pound-python.org/ "Our tireless moderators ensure that disruptive conversations and people are removed from the channel quickly and with a minimum of fuss. -- Most notably, we don't tolerate use of "LOL" or other forms of 'chatspeak'."
08:56:50 <Jafet> Ah, cheater would be the one to know the details.
08:57:10 <cheater> i've been around
08:57:20 <CakeProphet> wow that's hilarious
08:57:23 <cheater> yes
08:57:24 <CakeProphet> I might actually have to lol.
08:57:24 <cheater> it is
08:57:30 <CakeProphet> perhaps I will rofl
08:57:36 <cheater> and they are like very fucking adamant about it
08:57:42 <cheater> it's like LOL killed someone's parent
08:57:43 <cheater> s
08:57:44 <Patashu> oh god. not even lol?
08:57:45 * Patashu cries
08:57:47 <cheater> yes
08:58:06 <Patashu> goon project: let's all go in and say 'lol' simultaneously
08:58:12 <monqy> do they permit hehe or haha or snickers or chuckles
08:58:52 <fizzie> No forms of hilarity at all. Python is serious business.
08:59:38 <CakeProphet> I am in Python right
09:00:14 <CakeProphet> but I'd rather not get band as I have a vhost which would make it permanent on this nick.
09:00:14 <monqy> I don't think I;ve ever heard anything good about #python
09:00:27 <CakeProphet> monqy: probably because I've been bashing it nonstop for the past few days.
09:00:35 <CakeProphet> and probably because you're in #esoteric a lot
09:00:45 <fizzie> But the website says you get personalized service and everything.
09:01:05 <monqy> of course they'd praise themselves
09:01:12 <monqy> it doesn't help
09:05:19 <CakeProphet> help what help
09:05:40 <monqy> help
09:05:46 <monqy> .
09:06:42 <CakeProphet> bash: .: filename argument required
09:06:43 <CakeProphet> .: usage: . filename [arguments]
09:07:29 <monqy> .
09:07:54 <CakeProphet> irp: fatal give a shit exception
09:08:12 <monqy> oops
09:17:04 <nooga> https://gist.github.com/1205816 looks bad
09:29:41 -!- derrik has joined.
09:31:17 -!- derdon has joined.
09:40:55 -!- derrik has quit (Ping timeout: 252 seconds).
10:37:37 -!- monqy has quit (Quit: hello).
10:39:50 -!- Phantom_Hoover has joined.
11:02:51 -!- derdon has quit (Remote host closed the connection).
11:25:11 -!- sllide has joined.
11:51:59 -!- derrik has joined.
11:52:59 -!- derrik has quit (Client Quit).
11:53:10 <CakeProphet> which is what I'm currently doing.
11:53:55 -!- derrik has joined.
11:59:32 -!- derrik has quit (Ping timeout: 252 seconds).
12:01:39 -!- pikhq has joined.
12:01:59 -!- pikhq_ has quit (Ping timeout: 260 seconds).
12:16:45 <nooga> which is
12:41:01 -!- monqy has joined.
12:41:55 <nooga> aaaaaaaaaaaaaaa
12:42:39 <monqy> hi
12:53:31 -!- Patashu has quit (Quit: MSN: Patashu@hotmail.com , Gmail: Patashu0@gmail.com , AIM: Patashu0 , YIM: patashu2 .).
13:33:28 <copumpkin> wow :)
13:38:02 <monqy> hhehe that paste thing
13:42:31 -!- DH____ has quit (Remote host closed the connection).
13:43:04 <nooga> it's not hehehe, it's AAAAAAAAAAAA
13:44:13 <nooga> the worst thing is T before the Point and xx->method(xx,...
13:44:21 <nooga> otherwise it would be quite nice
13:44:59 <monqy> it almost looks like something I would do were I trying to do awful things in C to make boring things more amusing maybe
13:45:21 <monqy> almost
13:45:41 <monqy> by looks I mean "is in the style of"
13:45:48 <nooga> uhum
13:46:04 <monqy> as I would most likely go about it a bit differently
13:46:55 <nooga> then check this out: http://stackoverflow.com/questions/351733/can-you-write-object-oriented-code-in-c
13:46:58 <nooga> :D
13:48:08 <nooga> i'm coding for bare metal now and i would like to use some basic OO style
13:48:19 <monqy> naturally I'm more interested in functional c
13:48:19 <nooga> porting Objective-C runtime is not worth it
13:48:25 <nooga> and I hate C++
13:48:34 <nooga> monqy: oh, that too
13:48:41 <nooga> clang has blocks!
13:48:49 <nooga> but they need a runtime ;/
13:56:37 <fizzie> That sort of thing also hangs one function pointer/method to each object of a "class", bloating them by quite a lot, since they're going to be identical for all objects. The syntax with a separate vtbl is even uglier, though, something like "xx->vtbl->method(xx, ...)".
13:56:56 <nooga> yeah
13:57:01 <nooga> there should be vtable
13:57:17 <nooga> but then again call syntax gets uglier
13:58:22 <fizzie> You can do some sort of an equally ugly macro to rewrite CALL(obj, method, arg1, arg2, ...) into obj->vtbl->method(obj, arg1, arg2, ...). (Or just write C.)
13:58:48 <nooga> that's right
14:03:52 <nooga> another option is to take C's yacc definition and code every goddamn semantic rule + add your own few
14:04:02 <nooga> then use this as a preprocessor
14:16:42 -!- copumpkin has quit (Quit: Computer has gone to sleep.).
14:17:31 <nooga> or develop new language that compiles to C
14:26:24 -!- azaq23 has joined.
14:41:09 <nooga> sounds like fun
14:42:12 -!- copumpkin has joined.
14:42:17 <Gregor> You don't reaaaaally need to code every semantic rule, just the AST, and make them all compile down into themselves by default.
14:43:26 <Gregor> You could use Fythe :P
14:46:05 <nooga> i target bare metal since i'm writing an experimental kernel
14:47:35 <Gregor> I just meant you could use Fythe as the engine for a C+whatever->C translator
14:50:45 <nooga> I've just read the documentation
14:50:54 <nooga> but i think it's not enough ;f
14:51:03 <monqy> what documentation
14:51:51 <Gregor> Yeah, what documentation? :P
14:52:20 <nooga> the pdf file You provided on the plof.org :D
14:52:49 <Gregor> *fythe.org
14:53:05 <Gregor> Yeah, I'm not so great with documentation X-P
14:53:39 <Gregor> Anyway, one of these days I'm going to write GGGGCCCC (GGGGC-C-to-C-Compiler) in Fythe ... but until then, take my "recommendations" as mostly the blathering of a madman.
14:54:52 <nooga> GGGGC ?
14:55:17 <Gregor> Gregor's General-purpose Generational Garbage Collector
14:56:07 <Gregor> It's a precise GC for C (and because it's precise, it requires the user to do a bunch of boilerplate to make sure things never overlap improperly)
14:56:38 <Gregor> Erm, s/overlap improperly/aren't visible to the GC/, or something like that :P
14:56:42 <Gregor> Weird attempt at phrasing :P
14:57:02 <Gregor> Point is, it requires boilerplate, so I was thinking of making a C->C compiler that just injects the boilerplate for you.
15:06:31 <nooga> oh
15:06:52 <nooga> sounds really nice
15:08:02 <nooga> but I still got this : https://gist.github.com/1206470 :D
15:09:01 <monqy> yikes
15:09:05 <nooga> it parses C. The thing is i don't know yacc tricks enough to make it output the input without writing much
15:11:21 <olsner> Gregor: haha, GGGGCCCC is a very good name
15:12:07 -!- MDude has joined.
15:18:29 -!- FireFly has joined.
15:40:36 -!- tiffany has joined.
15:50:27 <Gregor> olsner: I'm pretty proud of it :P
16:27:03 -!- elliott has joined.
16:27:11 <Phantom_Hoover>  http://powdertoy.co.uk/
16:27:17 <Phantom_Hoover> help where is my life going
16:27:26 <Phantom_Hoover> i'm sure there are things that aren't this
16:27:31 <Phantom_Hoover> but i don't know what they are
16:27:43 <elliott> hi
16:27:48 <elliott> oh falling sand
16:27:52 <Phantom_Hoover> yes
16:27:55 <Phantom_Hoover> except
16:27:58 <Phantom_Hoover> with nukes
16:30:48 <Phantom_Hoover> And CAs which can be used for heat.
16:37:03 <Gregor> nooga: Incidentally, if you read the in-progress Fythe spec, can you tell me where it was most ridiculously confusing? :)
16:40:16 <elliott> 21:30:15: <Taneb> I leave you with http://esoteric.voxelperfect.net/wiki/User:Taneb/XSLT_S_and_K
16:40:23 <elliott> <s><k/><k/></s> ain't right
16:40:40 <elliott> <<s><k/></s>><k/></<s><k/></s>>
16:40:43 <elliott> MUCH BETTER
16:41:31 <elliott> `addquote <ais523> this strikes me as probably better than a singularity, because you can't trust a random AI, but you can probably trust olsner
16:41:36 <HackEgo> 642) <ais523> this strikes me as probably better than a singularity, because you can't trust a random AI, but you can probably trust olsner
16:41:44 * elliott decides to briefly worry that ais was serious.
16:46:16 <elliott> 22:29:49: <CakeProphet> you have typeclasses, and instances of such. if the type matches the instance declaration then it has an implementation of the methods.
16:46:16 <elliott> 22:30:03: <CakeProphet> there isn't any sort of re-routing or conditional logic involved.
16:46:19 <elliott> CakeProphet: You are wrong.
16:52:50 <elliott> 00:17:56: <Gregor> In Catholicism, the halting problem is believed to be unsolvable for infants who die before baptism.
16:52:50 <elliott> 00:19:00: <ais523> well, it's unsolvable for most other TC systems...
16:52:54 <elliott> ais considers humans tc?
16:53:08 <Gregor> elliott: Ridiculous, I no.
16:53:13 <Gregor> >_<
16:53:14 <elliott> I no too.
16:53:15 <Gregor> elliott: Ridiculous, I know.
16:53:17 <elliott> [asterisk]two
16:53:31 <Gregor> Since when am I so terrible at English :'(
16:54:00 <elliott> Saints wind ham eye sow terrible add English?
16:54:06 <elliott> Couldn't think of anything for terrible or English :(
16:54:28 <Deewiant> tearable
16:54:43 <elliott> Thanks
16:54:46 <Gregor> Tearable at ink-lash
16:54:48 <elliott> X-D
16:54:52 <elliott> That's not even a word.
16:55:01 <elliott> Saints wind ham eye sow tearable add ink lash?
16:55:03 <elliott> BEAUTIFUL
16:55:06 <Gregor> I will give you two lashings every time you claim that "lash" isn't a word.
16:55:16 <elliott> Lash is a word, ink is a word, I'm sceptical of ink-lash
16:55:33 <Gregor> It's hyphenated, it's referring to a lashing with ink :P
16:55:49 <Gregor> If I take a whip and dip it in ink, then lash you with it, that's an ink-lash.
16:55:59 <elliott> The worst kind of lash.
16:55:59 <pikhq> elliott: Well, the combination of humans and data storage definitely is. Without data storage, the system is comically restricted.
16:56:04 <pikhq> I mean, jeeze, human memory *sucks*.
16:56:12 <elliott> pikhq: you have infinite data storage? ok
16:56:19 <pikhq> elliott: Of course.
16:56:35 <Gregor> pikhq: We were referring to individual humans, not groups.
16:56:42 <Gregor> Individual humans are plainly not TC.
16:56:43 <elliott> 03:10:38: <Jafet> By "unthrow", I presume you mean "go back to where the exception occurred and continue".
16:56:51 <elliott> you guys realise languages already have this?
16:57:04 <Gregor> For instance, C+POSIX :P
16:57:07 <elliott> IIRC Ruby lets you "continue" from an exception handling clause, but I may be wrong
16:57:10 <pikhq> Gregor: Sure they are. They can simulate certain simple UTMs just fine if you give them an infinite paper spool and an infinite pen.
16:57:14 <elliott> Common Lisp obviously has it
16:57:24 <Gregor> pikhq: halts (x:human) -> true
16:57:25 <pikhq> elliott: What, don't you shop at the Frictionless Pully Store, fine purveyor of physical impossibilities?
16:57:33 <pikhq> Gregor: Oh, fine, *and immortality*.
16:57:39 <Gregor> pikhq: So, not human :P
16:58:14 <pikhq> Gregor: I didn't realise "mortal" was part of the definition of "human".
16:58:33 <elliott> An immortal human with infinite storage capability
16:58:41 <elliott> Find me a transhumanist who'd say "oh, well that's just a bloody HUMAN".
16:59:26 <pikhq> The infinite storage capability here is clearly external.
16:59:38 <pikhq> I'm specifying an infinite paper spool and an infinite pen.
17:00:21 <elliott> <pikhq> I have no idea what the Chinese Room argument is.
17:00:29 <elliott> <pikhq> And/or, am stupid enough to buy it.
17:01:02 <pikhq> Okay, fine, I'm just being completely and utterly silly.
17:01:24 <pikhq> And no, I don't buy the Chinese Room argument. It's a bunch of stupid wanking.
17:03:10 <nooga> Gregor: first of all I would add really simple, but complete, example of small language
17:04:13 <elliott> Specifications should not include examples.
17:04:43 <Gregor> Well, the Fythe spec is wildly incomplete anyway, I was more concerned about whether what little is already there makes any sense :P
17:05:05 <Gregor> nooga: That being said, BOOM: https://bitbucket.org/GregorR/fythe/src/tip/fythecore/fml.fythe
17:05:46 <Gregor> (Down to line 283 is the language, beyond that is a small standard library written in it)
17:06:12 <nooga> great
17:06:15 <pikhq> elliott: RFCs often do.
17:06:24 <elliott> RFCs are just requests for comment :P
17:06:32 <pikhq> Admittedly, RFCs aren't so much "formal specs" as they are "brief descriptions".
17:06:50 <Gregor> The Fythe spec is certainly not a formal spec.
17:11:50 <elliott> It certainly should be.
17:12:02 <Gregor> Hahaha no.
17:12:21 <Gregor> Eventually, it would be nice to have a formal spec.
17:12:47 <Gregor> Especially seeing as that a formal spec for Fythe plus an implementation of any language in Fythe = a formal spec for that language.
17:12:52 <Gregor> In the interim, hahaha no :P
17:13:41 <nooga> well
17:13:42 <nooga> uh
17:14:04 <elliott> Gregor: Formal specs are easy :P
17:14:52 <Gregor> nooga: Please note that for all my evangelism of Fythe (because it's awesome), at this point it's basically at the proof-of-concept phase :P
17:15:06 <nooga> i noticed ;)
17:19:41 <elliott> 04:07:32: <CakeProphet> also the Haskell example looks a little bit ugly
17:19:45 <elliott> CakeProphet: that's because it's a stupid example
17:20:20 <elliott> throw (42 :: Int)
17:20:20 <elliott>   `catches` [ \(e::Double) -> print (0,e)
17:20:20 <elliott>             , \(e::Int)    -> print (1,e) ]
17:20:25 <elliott> is a nicer way of formatting the same thing, though
17:21:19 <elliott> 04:17:28: <oerjan> <CakeProphet> also the Haskell example looks a little bit ugly <-- the nested catch'es because it is catching two different exception types. there's a function catches which takes a list of handlers but it requires them to be wrapped with Handler.
17:21:21 <elliott> oh um right
17:21:25 <elliott> need Handler <dollar sign> before those
17:21:26 <elliott> but w/e
17:22:58 <elliott> 05:47:21: <Sgeo> (Warning: mises stuff)
17:23:06 <elliott> Sgeo: too late i had a heart attack n/ died bcuz of ur ignorance fucker
17:23:11 <monqy> ;_;
17:23:21 <monqy> rip
17:23:30 <elliott> 06:00:56: <CakeProphet> > sort $ (+) <$> [1..5] <*> [1..5]
17:23:30 <elliott> 06:00:58: <lambdabot> [2,3,3,4,4,4,5,5,5,5,6,6,6,6,6,7,7,7,7,8,8,8,9,9,10]
17:23:30 <elliott> 06:01:35: <CakeProphet> oerjan: is there some sort of theoretical mathematics behind this?
17:23:31 <elliott> i...
17:23:52 <Phantom_Hoover> XD
17:23:56 <Phantom_Hoover> :t <*>
17:23:57 <lambdabot> parse error on input `<*>'
17:24:03 <Phantom_Hoover> :t (<*>)
17:24:04 <lambdabot> forall (f :: * -> *) a b. (Applicative f) => f (a -> b) -> f a -> f b
17:24:06 <elliott> rip Phantom_Hoover killed by ()
17:26:51 <elliott> 06:24:25: <oerjan> erm s/know/know from the haskell report, where for some stupid reason the Random class seems to have been excluded in ghc, i think that's a bug/
17:26:52 <elliott> huh
17:27:09 <elliott> 06:24:25: <oerjan> erm s/know/know from the haskell report, where for some stupid reason the Random class seems to have been excluded in ghc, i think that's a bug/
17:27:11 <elliott> erm
17:27:12 <elliott> 06:24:54: <zzo38> Is there a such thing as (x ->) monad?
17:27:12 <elliott> 06:25:06: <oerjan> zzo38: yes, import Control.Monad.Reader
17:27:12 <elliott> 06:25:37: <oerjan> it's isomorphic to the Reader Monad, so defined there
17:27:14 <elliott> or Control.Monad.Instances
17:28:50 -!- brisingr has joined.
17:34:03 <elliott> 07:45:19: <copumpkin> terminating agda isn't turing-complete
17:34:03 <elliott> 07:45:29: <copumpkin> it's conservative
17:34:04 <elliott> 07:45:45: <copumpkin> it might warn you that a terminating function doesn't terminate because its simple condition isn't accurate
17:34:04 <elliott> 07:45:56: <copumpkin> but it won't ever decide that a non-terminating function does terminate
17:34:04 <elliott> 07:46:32: <copumpkin> but because of that, you can trust proofs in it
17:34:11 <elliott> copumpkin: So they fixed that bug where _|_ is provable?
17:35:53 -!- sllide has quit (Ping timeout: 276 seconds).
17:38:41 <elliott> 08:50:04: <CakeProphet> Python topic line says "NO LOL"
17:38:41 <elliott> 08:50:09: <CakeProphet> I wonder if they enforce that.
17:38:41 <elliott> 08:50:13: <CakeProphet> s/Python/#python/
17:38:41 <elliott> 08:51:18: <Jafet> Yes.
17:38:41 <elliott> 08:51:38: <Jafet> It raises the channel mean IQ, if only by a little.
17:38:48 <elliott> Jafet: Nah, it just raises the channel mean pedantry level.
17:38:55 -!- brisingr has quit (Ping timeout: 260 seconds).
17:40:48 -!- brisingr has joined.
17:42:50 <copumpkin> elliott?
17:43:20 -!- brisingr has changed nick to eliottt.
17:43:26 <elliott> <elliott> copumpkin: So they fixed that bug where _|_ is provable?
17:43:26 <copumpkin> oh, you're brisingr?
17:43:27 <eliottt> copumpkin: yes?
17:43:30 <elliott> No, I'm not :P
17:43:33 <copumpkin> elliott:  just now
17:43:38 -!- eliottt has changed nick to brising.
17:43:40 <elliott> copumpkin: Convenient
17:43:41 -!- brising has changed nick to brisingr.
17:43:53 <brisingr> :)
17:44:38 <elliott> 15:08:02: <nooga> but I still got this : https://gist.github.com/1206470 :D
17:44:44 <elliott> nooga: I don't believe that works
17:44:49 <elliott> There's the typedef issue
17:46:14 <pikhq> Yeah, it doesn't seem to be handling the disambiguation.
17:56:05 -!- zzo38 has joined.
18:15:29 -!- Taneb has joined.
18:15:40 <Taneb> Hello!
18:19:21 <elliott> hi
18:19:34 <Taneb> I was thinkinh
18:19:44 <Taneb> With a g and no h on the end
18:20:04 <Taneb> Functional languages should ideally have no side effects, right?
18:20:23 <zzo38> Yes, I would think so
18:20:27 <Taneb> And an imperative language is little but side effects, right?
18:21:11 <zzo38> An imperative language is side effect per command, but you could still have things that the side effects are limited to certain areas
18:21:12 <elliott> Taneb: Not true
18:21:20 <nooga> elliott: compile and see for yourself
18:21:33 <elliott> Good code in imperative languages essentially mimics functional code :)
18:21:59 <elliott> nooga: Compiling won't tell me if it's a correct parser, but I know that C isn't context-free, and can only be parsed with yacc by using the embedded C code to sort things out
18:22:08 <Taneb> How about, a pair of a functional language and an imperative language, with the functional language in the back and an imperative language in the front
18:22:13 <elliott> I don't need to compile it to know this
18:22:22 <nooga> elliott: ah, the yacc file
18:22:37 <Taneb> So the imperative language can use functions defined in the functional language
18:22:42 <nooga> yeah guys
18:22:49 <nooga> since GHC compiles to C, AFAIR
18:22:52 <zzo38> Taneb: That is one thing that can be done, I suppose. Even, with Haskell, you can have a C program and Haskell program using FFI, where the main function is in C.
18:23:45 <elliott> nooga: No, it does not
18:23:52 <elliott> -fvia-C is deprecated and hasn't been the default ever
18:23:55 <elliott> Hmm, well
18:23:59 <elliott> I don't remember if/when itw as last the default
18:24:49 <Taneb> In some ways this is ideal; the functional language can be as pure as it likes, and the imperative language can do what it does best: filling in the bits that can't be done by a pure functional language (eg, IO)
18:25:12 <Taneb> Also, XSLT S and K is going well
18:25:28 <elliott> Taneb: That's basically what Haskell does, except that the language is one.
18:25:39 <elliott> You can model impure things in a pure language.
18:26:12 <elliott> That's more convenient than having a separate imperative language, because in a pure language you can use the pure language's functional strengths in the model of the impurity.
18:26:48 <elliott> And modelling an impure thing of course doesn't violate the purity of the rest of the language, since it's just a model.
18:29:30 <Taneb> Just a though
18:29:31 <Taneb> t
18:30:19 <elliott> Not saying it's a bad thought, I'm just saying that this is essentially what Haskell does
18:30:31 <elliott> Except that it models the imperative language inside the functional one, which is more convenient
18:31:21 <itidus20> so if monads don't have side effects
18:31:47 <itidus20> what would be the opposite thing which is crammed with side effects
18:32:02 <elliott> What
18:32:15 <itidus20> if you wanted side effects, as many side effects as possible
18:32:25 <elliott> What does "monads don't have side effects" mean
18:32:43 <itidus20> i don't know.
18:32:59 <Taneb> I think he may be referring speciffically to the IO monad, but I'm not good at Haskell enough to be sure
18:33:11 <elliott> That still doesn't make any sense
18:33:36 <itidus20> i hope i am not interrupting something valuable
18:33:41 <elliott> Probably not
18:34:24 <monqy> hi
18:34:25 <itidus20> anyway, as a self-styled game developer, every bit of code i write will necessarily trigger multimedia events
18:34:47 <elliott> It's perfectly possible to write games in a purely functional style without littering code with side-effects.
18:34:50 <itidus20> well maybe not every single bit
18:34:56 <Taneb> There are very few esolangs speciffically designed for game-making
18:35:02 <elliott> Taneb: specifically
18:35:07 <Taneb> Thank you
18:35:14 <Taneb> I knew I was getting that word wrong
18:35:22 <Taneb> Single f, double l
18:35:26 <elliott> itidus20: You probably want to read http://prog21.dadgum.com/23.html
18:35:30 <elliott> And its linked followups
18:35:53 <elliott> That's just one example, but it's very untrue to say that games are inherently side-effectful
18:36:57 <itidus20> elliott: aha.. very interesting
18:37:36 <itidus20> so one might say the game code really exists inside that "process one frame"
18:37:57 <itidus20> now... this idea sits well with me actually
18:38:05 <elliott> itidus20: Hey, I said include the follow-ups too :P
18:38:14 <itidus20> but i wanna talk about that first
18:38:36 <elliott> Have fun with that, then
18:38:38 <zzo38> Yes you could have game in no side-effect, where the code is a function taking inputs having to do with frame and outputs for their result, is one possible way to do so.
18:38:53 <itidus20> a while ago i was playing with the idea of a language where you write code which will be called once every frame
18:38:59 <zzo38> Or to process events is another way
18:39:16 <nooga> so again
18:39:30 <nooga> elliott: what's wrong with that C syntax
18:39:40 <itidus20> afk
18:39:44 <elliott> nooga: <elliott> nooga: Compiling won't tell me if it's a correct parser, but I know that C isn't context-free, and can only be parsed with yacc by using the embedded C code to sort things out
18:39:57 <elliott> By definition, it cannot parse C correctly
18:40:46 <elliott> http://calculist.blogspot.com/2009/02/c-typedef-parsing-problem.html has information on it, I can't find the better blog post I read a while ago about it
18:41:04 <elliott> aha
18:41:06 <elliott> nooga: Read these two:
18:41:09 <elliott> http://eli.thegreenplace.net/2007/11/24/the-context-sensitivity-of-cs-grammar/
18:41:10 <elliott> http://eli.thegreenplace.net/2011/05/02/the-context-sensitivity-of-c%E2%80%99s-grammar-revisited/
18:41:46 <Taneb> I may make a Feather derivative
18:41:49 <Taneb> Called McGraw
18:42:47 <monqy> what will it do
18:43:13 <Taneb> Access to alternate universes, time travelling to the future
18:44:54 <Taneb> Time police
18:46:54 <zzo38> I know about typedef parsing in C. CWEB has the same problem but it is capable to parse typedefs correctly; it doesn't parse #include files but you can use the @s and @f command to affect formatting of anything and make them parse differently.
18:48:09 <Taneb> I think I may have finished XSLT S and K
18:48:15 <Taneb> I have no idea if it would work or not
18:48:45 -!- ais523 has joined.
18:49:28 <elliott> hi ais523
18:50:43 <ais523> hi elliott
18:51:05 <elliott> hi ais523
18:51:08 <zzo38> Enhanced CWEB is completely impossible to parse unless you can read all include files and definitions of metamacros.
18:54:58 <Taneb> Just spotted a huge flaw in XSLT S and K
18:55:12 <Taneb> But I can't quite describe it
18:55:43 <elliott> "There can only be at most 256 different smob types in the system. Instead of registering a huge number of smob types (for example, one for each relevant C struct in your application), it is sometimes better to register just one and implement a second layer of type dispatching on top of it. This second layer might use the 16 extra bits to extend its type, for example."
18:55:43 <elliott> augh
18:55:51 <elliott> ais523: feel my pain k thx
18:55:55 <Taneb> It doesn't realise that <a/><b/> is equivalent to <a><b/></a> when <a> is at the start of a document
18:56:10 <ais523> hmm, wouldn't k thx mean I was thanked no matter what I did?
18:56:31 <Taneb> k thx 4 !smoking
18:56:34 <ais523> elliott: that API seems usable but far from ideal
18:57:27 <ais523> perhaps it should work along the lines of <apply><apply><s/><k/></apply><k/></apply>
18:57:52 <elliott> yeah apply is a separate node type
18:57:55 <elliott> s and k are leaves
18:58:00 <elliott> apply is a branch
18:58:13 <elliott> ais523: yeah but i guess it's designed because of the internals of the scheme implementation
18:58:15 <elliott> speeeeeeed and all that
19:01:07 <elliott> http://alan.dipert.org/ Who wants to bet on the probability that this is the Alan Dipert who owns esolangs.org?
19:01:41 <elliott> "Lisp to PHP Compiler" --https://github.com/alandipert
19:01:43 <elliott> I'm gonna say p=one
19:01:55 <elliott> (Trying to find a newer email address than that aol one.)
19:02:06 <Taneb> I'll say p=0.94
19:02:20 <Deewiant> elliott: "email" at the top of his site
19:02:26 <Taneb> Bye
19:02:27 <ais523> I always assumed Graue owned esolangs.org (the name itself, not the website there)
19:02:27 <elliott> Deewiant: Yep
19:02:29 -!- Taneb has quit (Quit: Goodbye).
19:02:34 <elliott> Deewiant: But I don't know it's the same Alan Dipert
19:02:36 <elliott> Worth an email, though
19:02:42 <ais523> elliott: just ask if it's the same Alan Dipert
19:02:52 <elliott> ais523: I'll do that, and include what I said last time :P
19:02:59 <Deewiant> Did you email the AOL address?
19:03:03 <elliott> Yeah
19:03:13 <elliott> Turns out nobody uses AOL anymore, who'da thunk it
19:03:57 <Deewiant> elliott: whois dipert.org has the same address
19:04:20 <Deewiant> (You might want to tell him to update that while you're at it)
19:04:52 <elliott> Deewiant: Too late, sent out an unsure message
19:05:02 <elliott> But thanks for the confirmation
19:05:26 <ais523> I think it's always best to be unsure even when it's obvious
19:05:54 <elliott> "Sorry, I killed + ate the old Alan Dipert two years ago to the day. I inherited his name, email address, and all property but esolangs.org. So unfortunately you have the wrong person."
19:06:09 <Deewiant> Darn
19:06:09 <elliott> It COULD happen.
19:07:04 <zzo38> I made a webpage for TeX to PNG; you could use that (source codes is available if you want to make your own copy) and cache the results by uploading files to the wiki that are named by their text and use those images in wiki
19:07:26 <elliott> Google does that too
19:07:32 <elliott> Well, probably LaTeX
19:07:35 -!- brisingr has quit (Ping timeout: 260 seconds).
19:07:38 <elliott> But only you use TeX, so :P
19:07:54 <zzo38> elliott: Why didn't they inherit esolangs.org? Did someone else take over?
19:08:08 <elliott> zzo38: No, the ghost of Alan Dipert started running it
19:08:14 <elliott> Unfortunately ghosts can have no effect on the material world whatsoever
19:09:08 -!- brisingr has joined.
19:09:25 <elliott> ais523: gah, how do you use {{unsigned}} if the comment was edited to add a bunch of stuff over numerous hours?
19:09:46 <ais523> by the same person?
19:09:52 <ais523> just give the last timestamp, I think
19:10:26 <zzo38> What seem to me, many programs try to call TeX externally from webpages and whatever are dealing with security wrongly. I use it by making the new format file this one  http://zzo38computer.cjb.net/texify/texify.php?source=3  and then adding a time limit and memory limit to the program.
19:10:31 <elliott> --(this comment by 18:35, 9 September 2011 at 121.45.148.1 UTC; please sign your comments with ~~~~)
19:10:31 <elliott> argh
19:10:35 <elliott> I hate the ordering of unsigned's arguments
19:11:04 <ais523> elliott: well, I did call it unsigned2 originally
19:11:11 <ais523> but someone went and renamed it to unsigned
19:11:18 <elliott> ais523: haha, on wikipedia or the esolang wiki?
19:11:26 <elliott> former, looks like
19:11:36 <ais523> the reversed arguments are convenient when copying time/username from the history
19:11:41 <ais523> no, it's Esolang I'm talking about
19:11:47 <ais523> I didn't invent either template on Wikipedia
19:11:52 <elliott> http://esoteric.voxelperfect.net/w/index.php?title=Template:Unsigned&action=history
19:11:54 <elliott> doesn't look renamed
19:12:04 <elliott> (cur) (last) 22:17, 20 September 2006 Ihope127 (Talk | contribs) (Template:Unsigned2 moved to Template:Unsigned)
19:12:07 <elliott> ihope ¬_¬
19:12:08 <shachaf> elliott: So you're ehird.
19:12:16 <zzo38> Some systems try to stop you from using various disallowed TeX commands in the front-end by stopping ^^ and other things, which can cause various kind of problems but I did it differently, stopping disallowed things in the format file.
19:12:21 <elliott> that's not the right way to move pages, person who isn't tswett
19:12:25 <elliott> shachaf: No, I'm shachaf.
19:12:32 -!- JuliaSH has joined.
19:12:46 <shachaf> elliott: So that would probably mean you're in BST instead of EDT.
19:13:01 <elliott> That's so geographist.
19:13:08 <elliott> Why do our timezones need to be correlated with our location?
19:13:20 <elliott> ais523: What timezone are you on these days?
19:13:22 <tswett> elliott: huh.  What did that Ihope127 guy do, and what was wrong with it?
19:13:33 <elliott> tswett: Moved something by copying, I think... I'm not atcually sure
19:13:40 <tswett> Wait, did he... move something by copying?
19:13:43 <elliott> I might be wrong though.
19:13:50 <elliott> The history doesn't make sense.
19:13:51 <tswett> Yeah, that is indeed the wrong way to do it.
19:13:55 <ais523> elliott: mostly UTC+1, but I was in something more like UTC+8 yesterday/today
19:13:56 <elliott> Maybe it was moved properly, then unsigned[two] got deleted.
19:13:58 <elliott> Then you recreated it.
19:14:07 <tswett> Then again, the wiki *is* public domain, so at least it's a *legal* way to do things...
19:14:47 <zzo38> If you copy my program for safe TeX entered remotely, please *do not* use e-TeX, pdfTeX, XeTeX, LaTeX, LuaTeX, etc, because that will result in security holes. Use it only with the One True TeX.
19:15:15 <elliott> The One True TeX doesn't have more-notation, though.
19:15:20 <elliott> Can I use it with moreTeX?
19:16:11 -!- JuliaSH has left.
19:16:16 <zzo38> elliott: I don't know moreTeX. Anyways, TeX isn't supposed to be any other programming language such as Haskell, C, or Lua (except for LuaTeX).
19:17:33 <itidus20> i think the problem with functional programming languages is that they haven't found their edsger dijkstra yet
19:17:40 <zzo38> If you write your own TeX variant, it is your job to deal with the security issues yourself if you want to use it with that.
19:17:54 <monqy> itidus20: how is this a problem with functional programming languages
19:17:55 <itidus20> howard curry is more like the charles babbage of functional programming
19:18:06 <itidus20> whatever his name is
19:18:33 <elliott> have you used any functional languages
19:19:39 <itidus20> i can't help thinking functional languages care more about being consistent than being useful
19:19:39 <zzo38> I disabled the following commands for security purpose:  \special \font \errorstopmode \input \openout \openin \closeout \closein \write \read \immediate \errmessage \jobname \fontname \mag \magnification \dump
19:20:31 <zzo38> Which things related to category theory cannot be made in Haskell?
19:20:32 <itidus20> the fact is not everything can be neatly expressed as a function
19:20:53 <monqy> itidus20 once again philosophises without knowing what he's talking about
19:21:07 <itidus20> like, could you make gimp in haskell?
19:21:18 <itidus20> when i say haskell i mean any functional programming language
19:21:29 <ais523> itidus20: well, TCness...
19:21:40 <ais523> so the only issue would be trying to get a good API to GTK or whatever
19:22:09 <zzo38> Yes, if you have a good enough event system you could probably do it.
19:22:38 <cheater> itidus20, could you make gimp in asm?
19:22:51 <itidus20> i dunno ^_^;;;
19:23:11 <cheater> i've seen GUI interactive programs of similar complexity written in asm
19:23:18 <cheater> so yes you probably could
19:23:42 <cheater> the question is whether it would be a good idea to do that
19:23:59 <cheater> no, it would not be the besti dea because of haskell's stdlib still not being the best
19:24:04 <itidus20> im just being cruel
19:24:18 <itidus20> cruel is the fitting word
19:24:25 <ais523> cheater: you could just /compile/ it into asm
19:24:36 <zzo38> It is probably not best idea writing all programs in asm because them it work only on the computers it is designed on work on.
19:24:41 <elliott> the problem, itidus20, is that you're assuming you can make judgements on what is or is not possiblew tih functional languages given only a cursory reading of functional programming materials, and never actually trying to program in one
19:24:52 <elliott> and ignoring the fact that thousands of people write useful programs in purely functional languages
19:25:26 <zzo38> But of course if you write a program that is meant only a DOS program, or only a program meant to run on NES/Famicom emulator, you can write it fine using asm
19:26:01 <ais523> elliott: quick opinion: is "common subset of OCaml and F#" a sane language? As in, only using language elements with identical syntax in the two languages?
19:26:04 <itidus20> ok ok uh.. what about game of life?
19:26:09 <zzo38> (If the emulator is accurate enough, you could even put it in a cartridge and run in real NES/Famicom hardware on television)
19:26:29 <elliott> itidus20: Are you seriously implying nobody has ever created a game of life program in haskell before?
19:26:39 <elliott> It's practically a mainstream languages. Intel uses it, for chrissakes.
19:26:40 <itidus20> well im wondering how painful it is
19:26:51 <elliott> http://hackage.haskell.org/packages/archive/pkg-list.html
19:26:52 <elliott> life program: Conway's Life cellular automaton
19:26:57 <elliott> brians-brain program: A Haskell implementation of the Brian's Brain cellular automaton
19:27:09 <elliott> And Hackage is only a small subset of all the Haskell programs written.
19:29:25 <itidus20> i could say that it may be difficult to write an OS in a functional language.. but that is probably because machine code is geared towards imperative, and that computers are not really ready yet for such things
19:29:45 <elliott> http://programatica.cs.pdx.edu/House/
19:29:59 <elliott> http://www.ninj4.net/kinetic/ (seems to be a dead link though)
19:30:07 <elliott> http://lambda-the-ultimate.org/node/299
19:30:16 <elliott> There's another Haskell OS that I don't recall the name of.
19:30:21 <itidus20> :"> ok ......... well then. i submit
19:34:27 <Phantom_Hoover> THERE WAS A VISIBLE SUPERNOVA AND NOBODY FUCKING TOLD ME??????????????????????????/
19:34:48 <itidus20> it was years ago
19:35:04 <itidus20> you're just too far away because you're on earth
19:35:25 -!- silence1 has joined.
19:35:50 <silence1> l
19:35:57 <itidus20> a race of humanoids is really scrambling to escape imminent doom after the supernova
19:36:00 -!- silence1 has left.
19:37:51 <monqy> bye
19:39:38 <Phantom_Hoover> Aw, dammit, it's brightest tonight and you need binoculars.
19:40:32 <elliott> `addquote <Phantom_Hoover> THERE WAS A VISIBLE SUPERNOVA AND NOBODY FUCKING TOLD ME??????????????????????????/
19:40:34 <HackEgo> 643) <Phantom_Hoover> THERE WAS A VISIBLE SUPERNOVA AND NOBODY FUCKING TOLD ME??????????????????????????/
19:40:43 <elliott> Phantom_Hoover: Finally we know what would warrant cursing from you.
19:40:44 <monqy> /
19:41:24 <itidus20> looking into space just makes me feel very dizzy
19:41:34 <itidus20> makes my visual field feel too "big"
19:41:55 <Phantom_Hoover> elliott, bastard smug uncle in France with binoculars dammit.
19:42:18 <elliott> thats me
19:42:36 <itidus20> headache caused by such thoughts
19:43:01 <zzo38> I do have ideas related to operating system in Haskell. A program is simply any pure value (even a function), no specific type is required. Although type is exported so that you can put programs together with correct type. There is no IO monad, but there is the operating system monad, which is exposed so that you can call a program with overriding system calls (a bit like ptrace, I suppose).
19:43:49 <zzo38> And you can make up an IO monad that can then be run in the operating system monad, to work programs written for other (imperative) operating systems.
19:43:53 <itidus20> elliott has shown me that it's been done..
19:45:37 -!- Taneb has joined.
19:45:45 <Taneb> hlep
19:45:50 <zzo38> And devices, files, etc, can also be Haskell functions accessible by querying the operating system monad.
19:45:55 <Taneb> Getting a 412 error trying to edit the wiki
19:46:08 <Taneb> That's my first 412 error
19:46:10 <Taneb> :)
19:46:20 <Taneb> But still, I kinda want to edit the wiki
19:46:33 <Taneb> It also doesn't let me preview
19:48:00 <Taneb> Any suggestions?
19:48:10 <elliott> You put a span or div in there
19:48:12 <elliott> Use the span or div templates
19:49:00 <zzo38> There are other things that can cause such errors too
19:49:00 <Taneb> No "<"s or ">"s
19:49:24 <Taneb> Lots of &lt;s and &gt;s though, could that be it?
19:49:43 <zzo38> The signature hack is another way
19:49:50 -!- tswett has quit (Changing host).
19:49:50 -!- tswett has joined.
19:50:09 <Taneb> Signature hack?
19:50:10 <elliott> Taneb: Dunno, pastebin what you were trying to save?
19:50:46 <Taneb> http://pastebin.com/P78hqgx2
19:52:14 -!- yorick has joined.
19:52:30 <zzo38> Something that has not been corrected. It should be permitted for selected confirmed users not to be blocked by this program
19:55:44 <Taneb> So, any suggestions?
19:56:09 <itidus20> is it true that functional means nothing is so-called hard-coded?
19:56:55 <Taneb> I would have thought the very opposite
19:57:14 <elliott> itidus20: what does functional have to do with hard-coded
19:57:49 <elliott> Taneb: hmm, dunno what could be triggering it, ask ais523
19:58:06 <Taneb> ais523, any ideas?
19:58:22 <ais523> what's a 412 error anyway?
19:58:32 <Taneb> Precondition Failed
19:58:36 <Taneb> The precondition on the request for the URL /w/index.php evaluated to false.
19:58:36 <ais523> Taneb: are you trying to edit via esolangs.org, or esoteric.voxelperfect.net?
19:58:38 <ais523> aha
19:58:43 <ais523> you're probably triggering the spam filter
19:58:52 <ais523> it's famous for triggering on, among other things, div and span
19:59:00 <Taneb> No divs or spans
19:59:11 <elliott> ais523: http://pastebin.com/P78hqgx2
19:59:19 <elliott> stop repeating the two seconds of conversation i had with Taneb about this :P
19:59:36 <ais523> hmm, &lt; or &gt; could well be it
19:59:46 <Taneb> They were in before
19:59:47 <elliott> he saved it with &lt;s and gts before, I believe
19:59:50 <ais523> Taneb: do you know of the <nowiki> tag?
19:59:55 <Taneb> I do not
19:59:56 <ais523> it'd make that rather easier to read
19:59:59 <elliott> but yeah nowiki would help
20:00:07 <Taneb> How does it work?
20:00:09 <itidus20> nevermind.. disregard my last post.. was a mistakle
20:00:14 <ais523> it basically means "interpret everything up to the next </nowiki> literally"
20:00:24 <Taneb> Ooh
20:00:27 <Taneb> As in, plaintext?
20:00:30 <ais523> yep
20:00:42 <elliott> <pre><nowiki>....</nowiki></pre> is useful
20:00:42 <ais523> <pre><nowiki> is a common pairing
20:00:46 <ais523> although I'm not sure if the wiki allows <pre>
20:01:04 <ais523> anyway, binary search on preview may help you work out what's offending
20:01:36 <elliott> it does allow pre
20:01:59 <ais523> I know a spambot once made a page which was incredibly hard to delete because its name tripped the spam filter
20:02:12 <ais523> and trying to follow any links from it caused the spam filter to be tripped on the /referrer/
20:02:20 <Taneb> Using nowiki and <s and >s doesn't help
20:02:31 <ais523> in the end, #esoteric figured out what was going on and I spoofed the referrer to delete it
20:02:39 <ais523> Taneb: well, it makes it more readable, at least
20:03:07 <ais523> the thing is, I have no access to the spam filter
20:03:23 <ais523> and know nothing about how it behaves, but for what we've deduced by experiment
20:03:27 <ais523> banning div and span is really obvious
20:03:36 <ais523> but there are probably other things in there that are much less obvious
20:04:26 <ais523> binary search seems to be the way to go
20:04:34 <ais523> try previewing the first half, then the first quarter, etc, until it works
20:07:18 <Taneb> The line  <xsl:copy-of  select="../*[3]"/> seems to trip it
20:07:37 <ais523> ouch, I wonder what's wrong with that line?
20:07:46 <ais523> you could try binary-searching even within the line
20:07:51 <ais523> that definitely doesn't trip any spam filters I know of
20:07:56 <ais523> but I didn't think I knew them all
20:08:33 <Taneb> It doesn't like "../*[3]"
20:08:40 <Taneb> With or without quotes
20:08:59 <Taneb> ../
20:09:24 <Taneb> That's the smallest it will go and still trip the filter
20:12:11 <ais523> a/ha/
20:12:19 <elliott> haha
20:12:20 <ais523> .</nowiki>.<nowiki>/
20:12:23 <elliott> what a terrible spam filter
20:12:24 <ais523> should avoid tripping it
20:12:38 <Taneb> I've saved it in a way that works
20:12:59 <ais523> elliott: I well know Esolang's spam filter is terrible
20:13:27 <Taneb> My way of fixing it was the slightly less readable .&#46;/
20:13:28 <elliott> I know you know
20:13:39 <ais523> &#46; works even inside nowiki?
20:13:43 <Taneb> Yeah
20:13:51 <Taneb> So does <s>...</s>
20:13:54 <Taneb> Which is annoying
20:14:02 <Taneb> As I am using <s> for something else
20:14:14 <Taneb> HTML isn't wiki
20:15:42 <Taneb> HTML character entities still work
20:19:02 -!- Taneb_ has joined.
20:20:32 <itidus20> this prog21.dadgum is quite cool
20:20:38 -!- Taneb has quit (Ping timeout: 276 seconds).
20:21:07 <itidus20> now i am very impressed to see a section beginning "I want to talk about performance coding. Not coding for speed, but coding as performance, a la live coding."
20:21:20 <itidus20> because i have actually wondered about that very same thing before
20:30:21 <itidus20> http://en.wikipedia.org/wiki/Interactive_computation
20:30:57 <itidus20> "the Turing machine model only provides an answer to the question of what computability of functions means and, with interactive tasks not always being reducible to functions, it fails to capture our broader intuition of computation and computability." -- no doubt this is controversial statement to make
20:31:04 -!- MDude has quit (Quit: later chat).
20:33:36 <elliott> looks like an advertisement article.
20:33:49 <elliott> note references being basically all the same few people.
20:34:01 <itidus20> ahhhhhhhh
20:34:26 <elliott> Can't say for sure, but...
20:34:33 <itidus20> no thats quite true
20:35:11 <itidus20> at least 3 references to the one author
20:35:15 <itidus20> and no actual references
20:35:32 <itidus20> "References and external web sources" you're right... thats not wiki style
20:35:43 <elliott> My bias against the idea is probably showing (in that I wouldn't complain much about an under-referenced article about a concept I liked).
20:36:08 <zzo38> Is there a point-free case command in Haskell?
20:36:15 <elliott> No.
20:37:54 <zzo38> Why?
20:42:09 <itidus20> elliott: i dont even know what it means. and i am sure it has nothing to do with how to code an x86
20:42:55 <zzo38> You should make the esolang wiki spam filter to be bypassed for the specified users if they are logged in. You could have it a field manually set in the user profile by administrators.
20:46:26 <nooga> elliott: isn't gcc's C parser also made in YACC?
20:47:06 <elliott> No, gcc's C parser is hand-written. I think they used to use a yacc parser. But yacc is turing-complete.
20:47:23 <elliott> The point is that you have to keep track of the typedefs by using yacc's blocks after the production
20:47:25 <elliott> i.e. foo { ... }
20:47:34 <elliott> That parser doesn't do so, so it can't possibly parse correctly.
20:48:01 <zzo38> I wrote more stuff relating to proposal of more-notation, including some possible circumstances in which it could be used.   http://www.haskell.org/haskellwiki/User:Zzo38/Proposal_for_more-notation
20:49:11 <nooga> elliott: clang's parser as well as tcc's one is also hand written
20:49:13 <nooga> this sucks
20:49:34 <zzo38> nooga: Is there anything wrong with that?
20:49:45 <elliott> ais523: there you go, http://www.haskell.org/haskellwiki/User:Zzo38/Proposal_for_more-notation
20:50:28 <ais523> oh, right
20:50:55 <ais523> wow, zzo38's writing style is instantly recognisable anywhere
20:51:36 <zzo38> ais523: That is because you have a lot of practice, because of we are all in this IRC together.
20:52:27 <ais523> perhaps
20:52:33 <zzo38> Does this document interest to you at all? Do you have any opinion/comment? You could write it on the IRC, or on the talk page of the wiki.
20:52:58 <ais523> I'll have to think about it
20:55:02 <nooga> zzo38: hard to hack in
20:56:21 -!- atrapado has joined.
20:56:34 <zzo38> nooga: Yes, that is what I thought. But I did be careful when writing that document, to make it not harder than it should be.
21:01:54 * Phantom_Hoover → looking in vain for the supernova.
21:03:55 -!- augur has joined.
21:06:36 -!- augur has quit (Remote host closed the connection).
21:07:24 <Phantom_Hoover> Hmm, I think I saw it very faintly.
21:07:41 <Phantom_Hoover> Aha, binoculars
21:07:43 <Phantom_Hoover> *!
21:08:27 <Sgeo> https://lh3.googleusercontent.com/-WLhqP3Po6hI/Tmp-VbpyS6I/AAAAAAAAAS8/UZq_G1bYfd8/s640/IMG_20110909_163314.jpg warning: dead animal
21:08:58 -!- jcp has quit (Ping timeout: 240 seconds).
21:09:03 -!- Patashu has joined.
21:10:43 <zzo38> I have no binoculars. There is also stuff in the way such as grapes and so on.
21:10:52 <elliott> Sgeo: I am unable to discern your reasons for linking to this.
21:11:35 <Sgeo> I guess I'm hoping someone could identify it
21:11:41 <monqy> oh
21:11:52 <monqy> dead
21:12:08 <elliott> its a dead animal hope this helps
21:12:10 <monqy> help i can't stop laughing
21:12:17 <Phantom_Hoover> Awww, the supernova is just a type 1a.
21:12:17 <elliott> its name was barry
21:13:04 <elliott> Phantom_Hoover: hi im dead animal
21:13:06 <monqy> it's not that dead animals are funny, it's that sgeo linking a picture of a dead animal out of nowhere is funny
21:13:24 <monqy> and then in post saying he hoped someone could identify it
21:13:38 <elliott> we will find who did this...............
21:13:43 <elliott> we will ARREST THEM FOR JUSTICE..............
21:15:11 <monqy> is there any context sgeo
21:15:17 <monqy> any at all
21:15:45 <Sgeo> I was walking to the school today, and stepped on it thinking it was a tree stump. When I walked back home, I noticed the bone
21:15:47 <Sgeo> bones
21:15:58 <monqy> poor bones
21:16:37 <zzo38> Oops you made a mistake.
21:16:42 <monqy> oops
21:16:48 <monqy> and then you took a picture of it
21:17:08 <monqy> this makes it even better
21:17:33 -!- jcp has joined.
21:19:03 -!- brisingr has quit (Read error: Connection reset by peer).
21:20:17 <Phantom_Hoover> You'd think Sgeo was 13.
21:20:45 <Phantom_Hoover> Silly Seth and the Mystery of the Dead Animal.
21:23:41 -!- Taneb_ has quit (Ping timeout: 276 seconds).
21:26:22 <elliott> `addquote <Phantom_Hoover> It is like the Holocaust but with Nazis.
21:26:25 <HackEgo> 644) <Phantom_Hoover> It is like the Holocaust but with Nazis.
21:32:08 -!- Taneb has joined.
21:46:08 <Patashu> as in the nazis are dying?
21:58:14 -!- boily has quit (Ping timeout: 252 seconds).
22:01:14 -!- augur has joined.
22:13:46 <Taneb> Goodnight
22:21:08 <elliott> ais523: the esolangs.org owner replied
22:21:17 -!- DH____ has joined.
22:21:18 <elliott> offering to point it at any dns server
22:21:31 <elliott> I doubt pointing it at voxelperfect's would work, since it doesn't know about esolangs.org
22:21:37 <ais523> ah, interesting
22:21:52 <ais523> I don't have a handy DNS server for the purpose
22:22:11 <elliott> yep, I think I'll tell him to go with the other option (investigate yi.org which I mentioned since I'd seen it used a lot)
22:22:17 <elliott> Gregor: any non-canyonthing suggestions for good free dns servers?
22:38:18 <itidus20> ok guys.. i have a new idea to drop
22:38:24 <Gregor> elliott: afraid.org
22:39:00 <itidus20> someone said "linked lists are inherently superior to arrays/arraylists when it comes to removing items from them"
22:39:18 <elliott> Gregor: Better than yi.org? :-P
22:39:44 <Gregor> elliott: Well, having not heard of yi.org, my response is "blerfmleh"
22:39:44 <Sgeo> arraylists?
22:39:45 <elliott> "Why is it free? It's quite simple. We wanted a challenge... that's it." ;; heh, such reassuring words.
22:39:45 <itidus20> so i started thinking, and i said "there could be an array traversing protocol.  2 kinds of items. 1) a number indicating how many data items follow 2) a number of which array index to jump to"
22:39:57 <itidus20> 0:[3] 1:[a] 2:[b] 3:[c] 4:[6] 5:[?] 6:[2] 7:[d] 8:[e]
22:40:06 <itidus20> 0: read 3 values. 4: jump to cell 6. 6: read 2 values.
22:40:25 <Gregor> elliott: That being said, it looks like yi.org is more focused on "dynamic DNS", whereas afraid.org is more focused on being a conventional interface with all the BINDing bells and whistles.
22:40:35 <elliott> Right.
22:40:55 <Sgeo> It's not a matter of how to do it within a language that makes linked lists better, it's the underlying structure that makes certiain operations more efficient
22:40:58 <itidus20> this idea of mine probably isn't all that wonderful.. but welll... yeah thats my latest thought
22:41:09 <Sgeo> *better for tasks which linked lists are better at
22:41:41 <Sgeo> Or I'm misunderstanding you. That's likely
22:42:01 <elliott> Aight, sent off another email to the 'pert.
22:42:07 <elliott> Also he might end up in here, I mentioned that I asked the channel.
22:43:56 <zzo38> Linked lists can be done in C, and in Haskell.
22:44:15 <itidus20> Sgeo: i'll code up my idea,, to make it more concrete
22:51:16 -!- alandipert has joined.
22:52:08 <itidus20> http://codepad.org/xWNBCwng
22:52:15 <elliott> hi alandipert
22:52:25 <alandipert> hi!
22:52:33 <ais523> hi!
22:52:38 <Gregor> lo!
22:52:38 <alandipert> it's been a few years, thought to pop in :-)
22:52:47 <itidus20> its not tested.. but it is supposed to do what i said
22:52:48 * alandipert formerly wooby, if anyone recalls
22:52:53 <Gregor> Ahhhhhhhhhhhhhhhhhhh
22:52:53 <zzo38> Can you switch text/binary I/O mode in Haskell?
22:53:10 <Gregor> alandipert: So presumably you're from a society that only gives you a non-ridiculous name when you reach a certain age? ;)
22:53:37 <elliott> I probably shouldn't have expected the domain to be owned by a completely random stranger :P
22:53:38 <itidus20> ok i can see an optimization already
22:53:51 <alandipert> lol
22:54:38 <itidus20> http://codepad.org/Yhjjp7nk
22:54:40 -!- copumpkin has quit (Quit: Computer has gone to sleep.).
22:55:02 <Sgeo> Oh, sorry, wasn't paying any attention
22:55:12 <Gregor> <elliott> I probably shouldn't have expected the domain to be owned by a completely random stranger :P // um ... so who does own it?
22:55:23 <elliott> Gregor: alandipert :P
22:55:23 <itidus20> Sgeo: ok have a look and if you're an expert code reader it might make some sense..
22:55:30 <itidus20> it wouldn't make sense to me though
22:55:40 <Gregor> alandipert: Oh! FIX FIX FIX IT NOW YOU EVIL EVIL BEING
22:55:43 <alandipert> back in a few, will toggle DNS bits shortly
22:55:58 <elliott> Forgive Gregor, he isn't accustomed to humans.
22:55:58 * alandipert writing esolang for dns manipulation
22:56:03 <elliott> oh dear
22:56:15 <elliott> Gregor: What have you _done_????
22:56:22 <ais523> I suppose esolangs.org was a great social manipulation thing
22:56:23 <Gregor> SOLVED ALL PROBLEMS?
22:56:30 <ais523> everyone just sort-of assumed that Graue owned it
22:56:31 <alandipert> Gregor: i remember from like 5 years ago a c->bf design, scanned from a napkin
22:56:32 <Sgeo> So it's an array that contains indexes into the array?
22:56:44 <Gregor> alandipert: It wasn't scanned from a napkin X-D
22:56:45 <itidus20> Sgeo: it contains 2 things
22:56:51 <Gregor> It was scanned from scribbling on normal paper :P
22:56:52 <itidus20> run lengths and indexes
22:56:59 <alandipert> oh ok :-)
22:57:03 <elliott> ais523: I found who owned it ages ago, I think
22:57:04 <elliott> I forget why
22:57:06 * alandipert thinks it would have been cooler if it was on a napkin
22:57:08 <elliott> Well, did a whois
22:57:09 <ais523> !bfjoust does_this_work_yet (>)*8(>[-])*21
22:57:17 <EgoBot> ​Score for ais523_does_this_work_yet: 18.3
22:57:17 <elliott> fungot: say hi to alandipert
22:57:18 <fungot> elliott: wait for cloud to return.
22:57:26 <elliott> ^style irc
22:57:27 <fungot> Selected style: irc (IRC logs of freenode/#esoteric, freenode/#scheme and ircnet/#douglasadams)
22:57:29 <elliott> fungot: say hi, more verbosely
22:57:30 <fungot> elliott: basically you want your function to return for the cell processor? this one is older. see http://okmij.org/ ftp/ papers/ lagarias/ paper/ html/ fnord
22:57:39 <itidus20> i will try it out :-s
22:57:55 <Sgeo> itidus20, to be clear, your structure has no random-access, which is the main benefit of arrays over linked-lists.
22:57:59 <ais523> who wrote fungot's Underload interp? fizzie?
22:57:59 <fungot> ais523: so does noone do mysql with scheme? i am sure it can be
22:58:00 <Sgeo> (iiuc)
22:58:01 <elliott> fizzie: Where'd that okmij come from? :P
22:58:09 <elliott> ais523: it's written in befunge, so yes
22:58:13 <itidus20> Sgeo: oh.... hmmm good point
22:58:14 <ais523> wow, fungot sounded surprisingly zzo38y there
22:58:15 <fungot> ais523: error in string-set!: expected type pair, got ' 65'. it was confusing since the only common language they have used until then. what were you expecting perhaps fnord discussions?
22:58:35 <Sgeo> ^style
22:58:36 <fungot> Available: agora alice c64 ct darwin discworld europarl ff7 fisher homestuck ic irc* jargon lovecraft nethack pa sms speeches ss wp youtube
22:58:36 <ais523> elliott: well, various people have written Befunge programs
22:58:39 <itidus20> Sgeo: i expect it's not every day that some fool manages to make an array not have random access
22:58:42 <ais523> I wrote a Deadfish interp in it, just because
22:58:55 <elliott> ais523: befunge isn't known for its modularity...
22:59:11 <Sgeo> itidus20, well, I think what you did is more of a linked-list, or linked-list like thing, implemented inside of an array
22:59:24 <ais523> elliott: really? it modularises pretty well
22:59:34 <itidus20> Sgeo: its sort of clever, right?
22:59:40 <elliott> ais523: I guess storage offsets are useful
23:00:08 <ais523> yep, that's all you really need to do subroutine calls
23:00:09 <Sgeo> itidus20, your code still only shows a portion of your idea
23:00:23 <ais523> together with some way to implement a return address stack
23:00:31 <ais523> (and I suppose you could use SUBR for that if you didn't want to hand-roll one)
23:00:53 <itidus20> Sgeo: well the idea is to make deletion less expensive in an array
23:02:32 <Sgeo> Store it in an array. Keep a separate record of "deleted" items, which does not require actually altering the storage array. ... actually, scrap that. What is the purpose of deleting from a random access array?
23:03:09 <itidus20> well i was responding to something someone in another channel typed
23:03:09 <Sgeo> And if you don't care about random-access, why are you using an array?
23:03:10 <itidus20> namely
23:03:22 <itidus20> "linked lists are inherently superior to arrays/arraylists when it comes to removing items from them"
23:03:58 <Sgeo> I don't know what they mean by arraylists, but... define "removing"
23:04:15 <Sgeo> Do they mean just shiftig everything else so that there's no gap in the indexing?
23:04:17 <itidus20> removing means deleting
23:04:38 <Gregor> Sgeo: An arraylist is generally a list of arrays, presenting the illusion elements of the inner arrays being a single, cohesive array. It's great for concatenating, and usually fast for indexing.
23:05:11 <Gregor> And yes, removing an element from a list is an O(1) operation, whereas removing an element from an array is an O(n) operation with n being the size.
23:05:21 <elliott> I don't really like arraylists.
23:05:33 <Gregor> elliott: And they don't like you.
23:05:45 <elliott> Gregor: It's not my fault they're not ropes.
23:06:07 <Sgeo> Gregor, why would someone want to "remove" an element from an array in that fashion?
23:06:28 <Gregor> Sgeo: Don't ask me.
23:06:49 <Sgeo> But I can think of ways using a secondary record to deal with it. Would make accessing a bit slower though
23:07:18 <Sgeo> Um, and inserting... um, ok, this is going into bad idea land
23:07:18 <itidus20> my idea might not be as hot as i expected
23:07:26 <itidus20> i didnt think it through
23:07:36 <Sgeo> Land of Bad and Ideas
23:07:55 -!- nooga has quit (Ping timeout: 252 seconds).
23:08:16 <itidus20> shit
23:08:23 <Sgeo> itidus20, I didn't mean your idea
23:08:36 <Sgeo> (which you still have not entirely expressed in code)
23:08:55 <Sgeo> Just... unneeded
23:09:17 <itidus20> i will have another crack at this
23:10:00 -!- FireFly has quit (Quit: FireFly).
23:10:41 <Sgeo> Keep in mind that memory can be described as an array. So implementing a data structure in an array does not give benefits over implementing it using pointers
23:11:31 <Sgeo> (I'm sure at some level "memory is an array" is inaccurate. Finegaling by the OS or something)
23:15:25 <CakeProphet> paging makes it less of an array.
23:16:46 -!- copumpkin has joined.
23:19:30 -!- atrapado has quit (Quit: FIN).
23:23:45 <itidus20> ok this is the actual working code: http://codepad.org/H8oSpLVR
23:23:59 <itidus20> i can't believe how difficult that proved for me
23:25:37 <itidus20> but it is occuring to me this system might not actually 'work' how its supposed to
23:25:48 <itidus20> if one actually tries to delete from the array
23:32:19 <itidus20> basically i think it will work as long as you delete more than 1 cell at a time
23:33:19 <Lymee> itidus20, what is that supposed to do?
23:33:39 <itidus20> it needs further devving >:)
23:34:26 <elliott> ais523: hey, the Java committee decided on the lambda syntax, and it features 0 octothorpes
23:34:43 <ais523> oh, what is it?
23:34:50 <elliott> http://mail.openjdk.java.net/pipermail/lambda-dev/2011-September/003936.html
23:34:51 <elliott> they stole C#'s :)
23:35:04 <Patashu> mmm, committees
23:35:53 <ais523> hmm, if that allowed a return type to be specified, as in (int x, int y) -> int {x + y;}
23:36:00 <Lymee> elliott, C++ uses that syntax too?
23:36:08 <ais523> then it would be pretty similar to C++'s in that case
23:36:14 <ais523> which is [](int x, int y) -> int {x + y;}
23:36:15 <Sgeo> itidus20, is the structure supposed to be such that the 0th slot has 0 items, 1st has 1, etc.?
23:36:26 <ais523> umm, {return x + y;} I think
23:36:30 <itidus20> ill get back to you
23:36:53 <Patashu> wait, C++ has lambda syntax?
23:36:53 <Patashu> O_O
23:37:01 <ais523> and rvalue references!
23:38:47 <Sgeo> C++ or C++0x?
23:39:09 <ais523> C++0x is C++
23:39:32 <elliott> yep, it was ratified, was it not?
23:39:57 <ais523> elliott: yes, and thus retroactively became correct
23:40:05 <elliott> haha
23:40:07 <elliott> feather-std
23:40:23 <ais523> oh no, I think we've managed to mix three metaphors in a way that actually makes sense
23:41:21 <ais523> anyway, that Java syntax seems fine to me
23:41:30 <elliott> indeed
23:41:34 <elliott> `addquote <ais523> oh no, I think we've managed to mix three metaphors in a way that actually makes sense
23:41:36 <HackEgo> 645) <ais523> oh no, I think we've managed to mix three metaphors in a way that actually makes sense
23:42:37 -!- DH____ has quit (Remote host closed the connection).
23:46:46 <Sgeo> I only see two metaphores in "feather-std"
23:46:59 <Sgeo> Or, um, is metphore the right wword?
23:47:10 -!- oerjan has joined.
23:47:41 <ais523> Sgeo: you possibly missed the Agora reference
23:48:23 <Sgeo> Oh, in retroactive correctness?
23:48:28 <ais523> yes
23:50:04 <Sgeo> I understand the eso-std reference but not entirely why it fits in
23:50:12 * Phantom_Hoover → sleep
23:50:13 -!- Phantom_Hoover has quit (Quit: Leaving).
23:56:57 -!- MSleep has joined.
23:57:03 -!- MSleep has changed nick to MDude.
23:59:53 -!- ais523 has quit (Remote host closed the connection).