00:18:09 -!- edwardk has joined.
00:21:33 <oklokok> doing some work on my language
00:22:16 <edwardk> i'm sitting here doing basically the same with a stripped down version of mine as well =)
00:23:09 <edwardk> which i guess could basically be described as a haskell without types at this point
00:23:13 <oklokok> oklotalk, my everlasting project
00:23:49 <oklokok> that's what happens when you don't think of a name for your language and someone asks what the name is...
00:24:24 <edwardk> mine has gone through a few names, so i typically just refer to it as 'my toy language' =)
00:24:55 <edwardk> nuel, kata, catalan, opt, and spec have all be the name at some point
00:25:09 <oklokok> http://www.vjn.fi/pb/p454332531.txt <<< it's heavily based on finite state machines that are introduced via a regex-like syntax
00:25:19 <edwardk> i dropped nuel coz its no longer a curry howard correspondence of the display logic
00:25:23 <edwardk> kata is still in the running
00:25:27 <edwardk> catalan is an actual language ;)
00:25:36 <edwardk> opt and spec are still open
00:25:42 <edwardk> just need to pick something ;)
00:25:45 <oklokok> "opt" and "spec" are kinda reserved for other usage
00:25:57 <oklokok> not that that has ever stopped anyone :)
00:26:08 <edwardk> they acronymed nicely into what i was doing
00:26:31 <edwardk> and the running joke of my friends is that my language name is 'x, where x is a variable to be determined later'
00:27:26 <edwardk> however, the acronym's for those describe the full language design and not the kinda fun stripped down version that i'm playing with now
00:29:34 <edwardk> so what is the premise of oklotalk? =)
00:30:31 <edwardk> its a language where i was exploring substructural type systems to start with, thats where the humor lies
00:30:43 <edwardk> since its all about type safety =)
00:31:06 <RodgerTheGreat> my main "pet" languages have been "Synthesys", "Lojo" and "Sprocket", the third of which was actually fully implemented.
00:31:29 <RodgerTheGreat> and Sprocket incorporates the best ideas from Synthesys in a more usable fashion, so no loss there
00:31:33 <oklokok> yeah, i've read every conversation you've had about your language on this channel, edwardk, though i haven't understood more than a third :)
00:31:50 <edwardk> basically at this point in time i'm trying to see if i can rederive most of the power of a traditional type theory through flow analysis and a simplist theorem prover over a basic universal type
00:32:47 <RodgerTheGreat> I started out with imperative designs, drifted into stack-based variants, and am now finding myself designing increasingly functional-style languages
00:32:53 <edwardk> i had started building up over a pretty powerful base type system, which didn't leave the theorem prover much to do, so i figured it was a more interesting result to see not if i could augment the power of a type system, but instead how much of it i could supplant
00:32:59 <oklokok> i'm trying to find a way to check for straights in tic-tac-toe using my language...
00:33:23 <RodgerTheGreat> oklokok: I've never seen a particularly elegant algo for that in any language
00:33:25 <edwardk> i went sort of the same path, i went imperative, drifted into computer algebra system designs, and now i'm functional with lazy semantics and optimistic evaluation
00:33:42 <RodgerTheGreat> the board is too small to really optimize the problem for without increasing overhead
00:38:42 -!- ehird` has quit.
00:39:34 <edwardk> oklo: in any event i've currently got none of the type features enabled including the substructural things, so its not that hard to understand its current behavior its more or less haskell and erlang's bastard child.
00:39:52 <oklokok> i'm doing it the brute force way first, since the technique i'm using is still under constructino
00:40:12 <RodgerTheGreat> edwardk: my language "Sprocket" is the bastard child of LISP and PostScript. :D
00:40:27 <oklokok> RodgerTheGreat: as you prolly guessed, i read that without the "never"
00:40:39 <oklokok> "any" sounded kinda weird there indeed :)
00:41:11 <oklokok> have you done any implementing?
00:41:42 <edwardk> what i have right now is that anything starting in upper case is a 'constructor' ala haskell's data constructors, and you can specify an arity for them, and use pattern matching primitives, and a trick to make monads work without types.
00:42:51 <edwardk> yeah quite a bit. i had an interpreter and theorem prover for the full language working, now i have an interpreter i've been toying with for the stripped down language that i figure i'll sit down and finish up this weekend since i want to rewrite the parser completely to strip out the remnants of the old logic
00:44:00 <edwardk> what i need to get right is the pattern matcher since i use a strange rule when compared to haskell or language's like that, because my rule lets me work around my lack of typeclasses
00:44:16 <edwardk> and still provide haskell like 'magic ints' and 'overloaded' operators, etc.
00:44:50 <RodgerTheGreat> how much of the language is intended to be primitive, versus synthetic?
00:44:54 <oklokok> http://www.vjn.fi/pb/p645463521.txt <<< checking for lines is currently done in an ugly prolog way :)
00:45:02 <edwardk> in this version? not much =)
00:45:02 <oklokok> hopefully i'll find a better way tomorrow.
00:45:33 <oklokok> i'm fairly sure you can't decipher that, but it's a graphical tic-tac-toe with 3x3 array
00:46:03 <oklokok> "end" is pretty cluttered.
00:46:18 <oklokok> i'm gonna enhance the list regex syntax a *lot*
00:46:26 <edwardk> its got a pattern match dispatcher, and primitive bigint support through GMP. assignment is primitive, beyond that most traditional language features, if, booleans, etc. are built up in the language
00:46:38 <oklokok> it's just i invented that feature this morning, so it's a bit undeveloped yet :PO
00:46:56 <edwardk> heh at one point in time i had a typecheck operator and subtyping operator defined in the language in two lines of code =)
00:47:41 <oklokok> you do almost everything synthetically
00:47:43 <RodgerTheGreat> the following is a fairly unreadable but completely valid fibonacci sequence generator in Sprocket: [clear 1 disp 0 1 !fibo ] :run [copy rollup add copy disp copy 144 nequ [!fibo] if ] :fibo
00:47:45 <edwardk> i guess the code that was there wont make a lot of sense unless you know and love monads
00:48:20 <RodgerTheGreat> this is a bit easier to understand: http://www.nonlogic.org/dump/text/1190418036.html
00:49:36 <oklokok> edwardk: that was a slow continuation to "(oklokok) you do almost everything synthetically", not to monads, i'm pretty neutral about those ;)
00:50:12 <edwardk> the monad stuff is just so that i can evaluate lazily and not get tripped up
00:50:34 <oklokok> RodgerTheGreat: in oklotalk, [\1 1 {!-_+!--_}] is a fib generator :)
00:51:12 <oklokok> [\1 1{!-_+!--_}] if that space seemed like too much :P
00:52:06 <RodgerTheGreat> oklokok: the Sprocket version is still quite efficient.
00:52:38 <RodgerTheGreat> I've considered adding single-character versions of all the basic keywords, which ought to make some simple things a lot more compact
00:53:10 <edwardk> fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
00:53:30 <edwardk> in my setting those colons become semicolons but otherwise its the same
00:54:02 <oklokok> oklotalk will own pretty much any language in that exact sequence since i designed iterators to fit that purpose ;)
00:54:10 <edwardk> well, that is an infinite list so access any portion of it as needed
00:54:40 <oklokok> i did that for fun, then realized that's nice for many other uses too
00:54:43 <edwardk> main = putStrLn (take 20 fibs) would show the first few in haskell
00:54:50 <RodgerTheGreat> edwardk: hm. I'm thinking it'd be a little hard to directly compare that with another language.
00:55:09 <oklokok> edwardk: my code was also an infinite list, though codata has to be done in an explicit way in oklotalk
00:55:09 <edwardk> well if you just want a fib function rather than a generator list
00:55:56 <edwardk> fib 0 = 1;; fib 1 = 1;; fib n = fib (n - 1) + fib (n -2)
00:56:25 <oklokok> and you'd do (out ([\1 1{!-_+!--_}] ! (0..10))) for the first 11 numbers
00:56:28 <edwardk> the one above memoized that naive definition doesn't
00:56:40 <RodgerTheGreat> I'm thinking my creation is the closest to a normal language of the bunch
00:57:03 <edwardk> so a memoized functional version in my setting would be
00:57:23 <edwardk> nevermind i forgot i was overloading list accesses
00:57:29 <edwardk> so fibs 12 should just work above
00:57:51 <edwardk> since a list used as a 'function' is a function taking a number and returning its nth element
00:58:01 <oklokok> in oklotalk, there's no difference
00:58:43 <oklokok> ΄[1 2 3 4](3) means you're interpreting the list as a function, and taking 4th element
00:59:17 <oklokok> (1;2;3;Nil) 1 = 2 <<< this is your language, not haskell, right?
00:59:19 <edwardk> in my case use of any type as the function in an application can be allowed
00:59:39 <edwardk> i can overload application
00:59:54 <edwardk> so arrays and lists take positions to dereference
01:00:34 <edwardk> also means you can pass in lists or arrays directly when something expects a function from nats (or in the array case anything indexable) to values.
01:01:51 -!- ihope has joined.
01:04:08 <oklokok> my bad, should know everything.
01:04:20 <oklokok> even the contents of your head
01:04:26 <edwardk> arity 1 Succ;; type Zero = Nat;; type (Succ n) | type n == Nat = Nat
01:04:34 <oklokok> hmm... that tic-tac-toe bugs me...
01:04:47 <oklokok> i don't want prolog, i want something beautiful
01:04:58 <oklokok> something fucking clever :P
01:05:09 <oklokok> i guess i'm onmy own there
01:05:17 <ihope> An arity keyword? What a travesty.
01:05:32 <edwardk> its a constructor based language without types
01:05:41 <edwardk> thats the only way i can tell you how many arguments that constructor takes
01:05:47 <edwardk> goes alongside infixl and infixr
01:06:50 <edwardk> any constructor without a specified arity has arity 0, so now anything that starts with an upper case letter is a constructor even with nothing else said
01:07:39 <edwardk> monads without types, its fun =)
01:07:52 <ihope> So what's the "type" keyword do if there are no types?
01:07:58 <edwardk> type there is a function =)
01:08:32 <edwardk> which takes the value Zero and returns the value Nat, and returns Nat when the condition is met in the second case above
01:09:35 <edwardk> you can do pretty much everything you want without adding 'type' to the language its just kinda useful for getting haskell-like typeclasses to work
01:09:50 <oklokok> it's useful for optimization too, i guess
01:09:59 <edwardk> coz how to overload + * /, etc?
01:10:12 <ihope> What's type Nat? :-)
01:10:27 <edwardk> a pattern match failure unless you specify =)
01:10:38 <edwardk> type Nat = Type;; type Type = Type
01:10:48 <edwardk> there now it has an impredicative type tower
01:11:00 <ihope> Impredicative type power?
01:11:21 <edwardk> arity 1 Type;; type Nat = Type 0;; type (Type n) = Type (n + 1)
01:11:24 <ihope> s/what I said/what I meant/
01:11:30 <edwardk> that would make it predicative
01:11:52 <ihope> Is this language lazy?
01:11:54 <edwardk> basically there are two ways to define a type system with multiple layers
01:13:28 <edwardk> one way you can define it has the sorts of types being types, and the other has them being kinds, and its whether the sort of kind is kind or superkind, and if that hierarchy keeps going up that tells you if you are predicative or impredicative.
01:14:26 <edwardk> in this setting i don't care about type systems, since they aren't needed to make monads work =)
01:14:56 <edwardk> arity 1 Ok;; return = Ok; Ok x >>= f = f x gives us an identity monad
01:15:22 <edwardk> mzero = Nil;; Nil >>= f = Nil together with the above gives us maybe
01:16:25 <edwardk> and rely on the monad laws to make 'Ok' work
01:20:13 <edwardk> is that an actual section marker symbol i see in that oklotalk code as part of the language?
01:21:00 <oklokok> currently using it for atoms
01:21:23 <oklokok> might change in case it's hard to access in non-finnish keyboards
01:21:29 <edwardk> so you don't have to deal with something like my upper case first letter rule
01:21:45 <edwardk> i used to use ' marks to note the beginning of an atom
01:21:50 <oklokok> lower-case first letter = parsed as a function
01:21:59 <oklokok> upper-case = parsed as a value
01:22:10 <oklokok> § in the beginning = parsed as an atom
01:22:46 <oklokok> i don't see how that has anything to do with it
01:22:48 <edwardk> the need to have separate value and function roles
01:23:05 <oklokok> i just need to know what is a function and what is a value because everything is infix/prefix parsed
01:23:06 <edwardk> same reason that ML has val and fun or whatever
01:23:26 <oklokok> any sequence of "funcokens" and "objokens" is valid
01:23:51 <oklokok> 5+3+4 == 5p3p4 if you do p=+ first.
01:24:40 <oklokok> or then i'm misunderstanding something.
01:25:00 <oklokok> it's just there's no difference between operators, functions and lambdas
01:25:36 <oklokok> so you can do infix and prefix with lambdas as well as with operators
01:25:45 <edwardk> well, the issue as i'm thinking of it is why c has to have separate functions and value types. you need to distinguish between int foo() { ... } and int foo
01:26:10 <edwardk> whereas in a lazy language you don't have a need for a value/function distinction
01:26:43 <oklokok> you need to know whether "A B" means a list of A and B or "apply A to B"
01:26:55 <oklokok> a B means a (B), whereas A B means [A, B]
01:27:07 <oklokok> adjacent objokens mean an implicit list.
01:27:37 <oklokok> but indeed, it is strict, although you can't see it from that.
01:27:50 <edwardk> i inferred strict from the { ; ; ; } blocks ;)
01:28:26 <oklokok> i'm only making it strict because i'm not confident enough in my implementation skills
01:28:47 <oklokok> it will be lazy in version 2 :P
01:29:04 <oklokok> since i don't see why not be lazy
01:29:11 <edwardk> i'm currently lazy and side effect free, but i may revert to a pathological reduction rule i used to use that i like which is worst-case lazy or strict. whatever it wants to do. so you have to make sure all of your reductions are confluent.
01:29:37 <edwardk> and the only promise i make is i won't strictly reduce anything wrapped in a 'lazy' keyword
01:30:20 <oklokok> oklotalk has special syntax for introducing generators, those can be used for pretty much anything laziness can, though admittedly it's not as pretty
01:30:48 <edwardk> the basic issue is that you need to guarantee that your code would work no matter how it was evaluated strictly or lazily, but in exchange the compiler can partially evaluate a larger class of things and take optimization steps that are unsound in EITHER a lazy or a strict language
01:32:06 <oklokok> not specifying stuff is the key to efficient optimization
01:32:09 <edwardk> on the other hand you have the burden of both disciplines, you have the space reasoning issues of a lazy language and the need for explicit 'lazy' annotations of a strict language, though you don't have an explicit 'force', so you get a small win there. and you still have to reason about side effects via a monad or CPS or other trick like a lazy language
01:33:04 <oklokok> hmm, i don't see how laziness and side-effects relate
01:33:36 <edwardk> currently i'm using an 'optimistic with lazy semantics' rule which says it can waste work on things eagerly but it has to bound the amount of speculation and if it encounters an error while speculating it has to pretend it didn't happen and turn that speculation into a lazy thunk to be forced on demand.
01:34:11 <edwardk> so that you can encounter bottoms and not 'bottom' out, but you don't have to build as many thunks
01:34:47 <edwardk> but the antagonistic compiler is somewhat more amusing of a rule, since it hasn't been used as far as i can tell ;)
01:34:51 <oklokok> not sure what that means :P
01:35:31 <edwardk> a thunk is the unevaluated computation that when forced will give you the answer and overwrite it self with the answer, so that call-by-name evaluation works
01:36:26 <edwardk> call-by-name has thunks, call-by-need makes the thunk remember the answer it gave by self-modifying
01:36:37 <oklokok> now that i come to think of it, lazy evaluation is pretty trivial to implement.
01:37:21 <edwardk> pattern matching just checks to see if what you have is a thunk if so it tells the thunk to evaluate which makes sure the outermost constructor is a value, then you can inspect it
01:37:40 -!- ihope_ has joined.
01:37:51 <edwardk> in the ghc haskell compiler it does so by making everything into a 'thunk' with a function for the constructed values that just returns itself
01:39:29 <oklokok> 1½ minutes of lag in my head
01:39:46 <edwardk> so basically a list 'cons' cell is a [Cons, x, xs] where cons is a pointer to a function that happens to just return the 'thunk' [Cons, x, xs] that it was given, so to force it you call the function at the start of the thunk and you inspect the value of the tag that it returns in the first position.
01:40:04 <edwardk> that way if you had a function like
01:40:12 <edwardk> repeat n = Cons n (repeat n)
01:40:20 <edwardk> then you'd encounter a thunk like
01:41:04 <edwardk> [Repeat, n] where Repeat was a function that takes that and constructs [Cons, n, [Repeat, n ]]
01:41:19 <edwardk> and hands it back for inspection
01:41:56 <edwardk> its the simplest model for compiled lazy evaluation i know
01:42:01 <oklokok> and when pattern matching occurs, it evaluates until there's an actual constructor as outermost
01:42:16 <oklokok> becoming [Cons, n, [Repeat, n ]], where repeat is [Cons, n, [Repeat, n ]]
01:42:54 <edwardk> yeah although that pattern matching routine doesn't have to loop explicitly because by calling that function which calls whatever other functions it has to call to reduce to 'weak head normal form' the recursion is implicit.
01:43:14 <edwardk> it just calls the one function and that thing takes care of all the details, but you have the right idea
01:43:41 <oklokok> you mean the actual caller will not have to care about the fact it has lazied out?
01:44:01 <oklokok> i mean, it doesn' have to know the object it's matching is actually a thunk
01:44:18 <edwardk> more or less, it knows it has to call the function that is in the first slot of the value it was given no matter what, then it can safely inspect the first value in the result that returns.
01:45:04 <edwardk> and laziness proceeds like that, outside-in.
01:46:05 <oklokok> i guess you can do the tree rewriting in any order as long as the result is as value-like as necessary
01:46:14 <edwardk> adding speculation muddies the waters a bit, you track a speculation depth cap, and rather than generate a thunk in the first place you try to run through it eagerly, but if you hit the cap you abort and return the thunk.
01:46:38 <oklokok> well yeah, but isn't that just optimization?
01:46:47 <edwardk> if you hit the cap too many times in the same place, then for performance reasons you disable speculation on that code point.
01:47:08 <edwardk> the semantics remain lazy, but evaluation can proceed eagerly in a lot of cases
01:47:52 <oklokok> if there are no infinite sequences and no side-effects, lazy evaluation and strict evaluation have no difference, am i right?
01:48:07 <oklokok> prolly not, but i don't know the difference.
01:48:10 <edwardk> the 'evil compiler' version of it, just allows me to reduce outside-in or inside-out as i choose
01:48:17 <oklokok> i mean, as far as the programmer is concerned..
01:48:37 <edwardk> they only have space and time efficiency tradeoffs in that case
01:48:47 <edwardk> which i think is perfectly reasonable to give the compiler more control over
01:49:03 <edwardk> no infinite loops and no side effects
01:49:42 <oklokok> sorry, i'm very slow right now
01:49:42 <edwardk> if you ever evaluate infinity you never stop
01:49:52 <oklokok> yes, indeed, i failed a bit there
01:49:58 <oklokok> i blame the wine and the time.
01:50:33 <edwardk> but in the absence of general recursion and general corecursion you can't tell the two apart without side effects
01:52:02 <oklokok> did you understand the oklotalk code btw?
01:52:04 <edwardk> productive corecursion is valid in a lazy setting, but not a strict-setting though, so the "devil's advocate" compiler design above might make productive corecursion into something that bottoms out and never returns
01:52:31 <edwardk> more or less, modulo the builtins
01:53:08 <oklokok> a few built-ins there indeed
01:53:34 <edwardk> productive corecursion being anything that you know returns an outermost constructor in a finite amount of time, the lazy counterpart to well-founded recursion which says your functions return
01:54:22 <oklokok> (i learned the term earlier today, but anyway :P)
01:55:01 <oklokok> hmm... don't know what that is :)
01:55:02 -!- ihope has quit (Read error: 110 (Connection timed out)).
01:55:24 <edwardk> ah he's a guy over on #haskell who is fond of that terminology
01:55:46 <oklokok> read an article @ neighborhood of infinity
01:56:20 <edwardk> ok, dan piponi, yeah he's fond of that stuff too
01:57:01 <oklokok> oerjan also once mentioned corecursion some months ago
01:57:10 <oklokok> i didn't bother to check then
01:57:40 <edwardk> i've been obsessed with comonads and codata for a while, so corecursion naturally follows ;)
01:57:57 <oklokok> hmm... comonads sounds dangerous.
01:59:10 <edwardk> comonads aren't that weird. monads are easy to put things into but hard to deconstruct, they are like a container that won't let you in to get at the value you injected unless you follow some rigorous protocol.
01:59:43 <edwardk> on the other hand comonads are easy to deconstruct, fragile even, you can always remove a comonad from the value it contains, but they may be harder to put things in.
01:59:49 <oklokok> "they" there, which does it refer to?
02:00:05 <edwardk> how well do you know monads?
02:00:30 <oklokok> i guess i know what they are, but their usage is just too complicated
02:01:14 <ihope_> I think they're like any other tricky concept, really.
02:01:45 <edwardk> a monad just basically says that i can take a value of some basic type and always transform that value into a more complicated type. i.e. if i have a value of type a. i can always transform that into a function of type e -> a by just returning a constant function that ignores its argument
02:01:48 <ihope_> Look at it for a while, ask to see it in different directions, and either it suddenly clicks or slowly falls into place.
02:02:16 <ihope_> Say that you don't understand something, and someone will declare that it's easy to understand and give you one way to understand it :-)
02:02:17 <edwardk> or, if i have a value of type a, i can always generate a function of type s -> (a,s) which just copies the argument through to the second position of the result
02:03:01 <edwardk> and then there are rules for taking functions that worked on your previous 'a' and getting a function that works on e -> a or s -> (a,s)
02:03:36 <edwardk> so it was 'easy' to inject a value into it, but we have to follow some protocol to get the value out, we have to supply an e or an s in either case, and in the second case we had to strip off the superfluous (,s) term, etc.
02:03:46 <oklokok> ihope_: i don't have to say that, the explanation follows anyway ;)
02:03:54 <edwardk> some monads you may not be able to 'strip off' at all
02:04:49 <edwardk> on the other hand a monad is something that if given you could discard the candy wrapper if you wanted to and always extract the value without any work, but which still provide that framework of how to extend a function for the basic value to handle a comonadically wrapped value.
02:05:06 <edwardk> so i could always treat the pair (e,a) as a by just ignoring the (e,) part
02:05:43 <edwardk> so i can always rip off that 'context' comonad as that is called, i don't have to supply additional information like i did with the reader monad e -> a or the state monad s -> (a,s) above
02:06:35 <oklokok> i guess i have to admit i ain't exactly following :)
02:06:54 * edwardk stops his 'easy to understand and giving you one way to understand it' explanation =)
02:07:52 <oklokok> i think i lack the part of the brain that manages monads
02:07:56 <edwardk> i think of monads as a container you can put something in, and a way to take a container of containers and flatten it out to get a container. so for lists you can always take a value and make a singleton list out of it, and you can always take a list of lists and concatenate them to get a single list
02:08:45 <oklokok> the problem is i know that much, but monads seem to have something much deeper in them.
02:09:14 <edwardk> you can always take a value and transform it into a function that ignores its argument, turning a into e -> a, and you can take an e -> (e -> a) and transform that into a function of type e -> a by using your argument twice
02:09:37 <edwardk> whereas a comonad goes the other way
02:09:45 <ihope_> Oh, monads are really no harder than, um...
02:10:01 <ihope_> ...I can't think of anything I'm trying to understand but can't.
02:10:04 <oklokok> "you can take an e -> (e -> a) and transform that into a function of type e -> a by using your argument twice" << sure about this?
02:10:10 <edwardk> you can always extract an a from (e,a) and you can duplicate the context, you can always generate (e,(e,a) given (e,a) but with just an a you cant generate (e,a) for an arbitrary e.
02:10:29 <ihope_> join :: (e -> (e -> a)) -> e -> a
02:10:52 <oklokok> "by using your argument twice"
02:12:19 <edwardk> the monads as containers analogy leads to a sort of 'comonads as candy wrappers with a possible valuable prize' analogy, you can get rid of the comonad, but it might have value if you kept it around, it may provide you with something you can't do without it.
02:13:20 <edwardk> in that case it provides you with the ability to access the value of e. discarding the comonadic wrapper discards that value.
02:14:22 <edwardk> and if you want to bake your brain you can analyze the fact that (e,a) and e -> a provide the same functionality and go off into category theory and make grandiose statements about how 'Hom and Prod' are adjoint functors so those two things do the same thing monadically and comonadically, etc. and then you can go get a job on the mathematics faculty somewhere ;)
02:15:59 <edwardk> actually that notion comes probably a bit easier through the concept of currying
02:16:32 <edwardk> (a,b) -> c can always be rewritten as a -> (b -> c) sort of witnesses the connection between , and ->
02:17:03 <oklokok> hmm, (a,b) is not a tuple then?
02:17:20 <edwardk> that connection implies the existence of the (,)e comonad given the (->)e monad and vice versa
02:18:05 <edwardk> you can always rewrite a function that takes a pair of values as a function that takes one of them and returns a function that takes the other and returns the result of calling the function on the pair of the values it now holds
02:18:38 <oklokok> but different call syntax in haskell
02:19:15 <edwardk> though technically the haskell version lazily handles the latter pattern
02:19:34 <edwardk> uncurry f xy = f (fst xy) (snd xy)
03:00:55 -!- ihope_ has quit (Read error: 110 (Connection timed out)).
03:19:56 -!- navaburo has left (?).
03:36:09 <Sgeo> Any thoughts on PSOX </normal-mindless-drivvel>
03:51:16 -!- hieronymus310 has joined.
03:52:48 <Sgeo> Is '$ yes no | rm -r /tmp' a safe thing to do?
03:53:14 <Sgeo> hieronymus310, LOCATION_ERROR: IRP_NOT_SUPPORTED_IN_THIS_CHANNEL__SEE_TOPIC
03:53:38 <edwardk> sgeo: well, you don't usually want to remove the /tmp folder entirely
03:53:56 * Sgeo already did it :/
03:54:08 <Sgeo> Imean, not everything was deleted..
03:54:28 <Sgeo> OSHI--12.5MB from right after, down to 4.6MB
03:54:53 <Sgeo> of total freespace
03:55:17 <edwardk> the worry would be if it succeeded entirely and /tmp was gone (which probably wouldn't work on most unix implementations since it usually is mounted) then mktmp and those calls don't know where to dump their files
03:55:41 <Sgeo> It didn't succeed entirely
03:55:44 <edwardk> but the contents of /tmp you can blow away until your heart is content ;)
03:55:57 <edwardk> that was why i was qualifying my response =)
03:56:24 * Sgeo desperately needs the space
03:56:25 -!- hieronymus310 has left (?).
03:56:56 <Sgeo> WTF 4.0KB free?
03:57:52 <Sgeo> Make that 0bytes
03:58:17 * Sgeo has exactly 0bytes free on /
03:58:43 <edwardk> thats generally a bad place to be
03:58:50 <edwardk> is /var in your / partition?
03:59:15 <Sgeo> Probably, why?
03:59:27 <edwardk> if so you might be able to get some room by nuking stuff out of /var/log
03:59:45 <Sgeo> 9.1MB of stuff in /var/log
04:00:04 <edwardk> how much room is on this machine in total anyways?
04:01:07 <Sgeo> Um, howdoItell?
04:01:41 <edwardk> that'll tell you what partitions you have how full they are and how big they are
04:01:52 <Sgeo> /dev/sda7 136188044 130653632 24 100% /
04:02:17 <Sgeo> oh, 24KB freew
04:02:35 <Sgeo> I think all I did was close a text editor
04:02:49 <edwardk> and you have no separate user partition or anything?
04:03:02 <Sgeo> And decreasing?
04:03:03 <edwardk> just like linux installed on a workstation in one big fat partition?
04:03:40 <edwardk> do you know where the space went or is that just a black box at this point?
04:04:19 <Sgeo> A dir with MIDIs converted to OGGs, all Futurama seasons, a bunch of SWFs, a bunch of ISOs, and more stuff probabky
04:05:10 <edwardk> was worried it was just some process filling your drive with drek, now i realize the user is the process in question ;)
04:06:24 <Sgeo> ~/music/midi/all is 2.5GB
04:06:31 <Sgeo> Not a lot, in relation to, say, ISOs
04:06:59 <edwardk> heh my solution is usually to run down and buy another 500 gig drive and add it to the machine =)
04:08:09 * edwardk is pushing about 2.5TB on his desktop machine these days and just realized it.
04:08:50 <edwardk> mostly virtual pc images, etc.
04:15:18 <Sgeo> Down to 0b again
04:15:31 <Sgeo> /dev/sda7 136188044 130653656 0 100% /
04:15:41 <Sgeo> Why are the numbers different?
04:15:54 * edwardk watches sgeo find space episode by precious episode...
04:16:14 <edwardk> because some percentage of the drive space is reserve for root
04:16:25 * Sgeo will probably delete some ISOs
04:16:53 <edwardk> the justification is that if you have NO drivespace left on the root partition then root can't shuffle things around to fix a problem
04:17:46 <Sgeo> How much is reserved (too lazy to do simpleish math right now)
04:18:21 <edwardk> its like 10% traditionally, but the numbers are probably changed by now, and remember root has some files on the drive so some of that reserve is used
04:19:04 <Sgeo> But I can store more stuff by becoming root? Yipee!
04:19:49 <Sgeo> Buh-bye openSUSE-10.2
04:20:02 <edwardk> yeah, though if you get to the point you are currently at you risk not being able to mount the drive in the event that you have to fsck it or lack the room to record the transaction log, etc.
04:20:34 <Sgeo> You mean, if I use up root's space?
04:20:57 <Sgeo> What about LiveCDs?
04:21:09 <edwardk> on a drive that big you should be able to lower the reserve some though
04:21:28 <edwardk> they don't risk corruption on themselves because they are an iso image, they don't write back to themselves
04:21:44 <edwardk> they make a ramdisk or whatever and load up in that if it corrupts there is nothing to fsck-up =)
04:21:46 <Sgeo> Incidentally, I wouldn't have been able to use the openSUSE LiveDVD anyway.. can't burn DVDs, and only have 512MB so can't emulate..
04:22:08 <Sgeo> woohoo 1.7GB freed
04:22:23 <Sgeo> Um, how do I peek into a tgz file?
04:22:38 <Sgeo> I have 10GB locked up in a file called someisos.tgz
04:22:53 <Sgeo> I made that file after running out of space before
04:23:47 <Sgeo> This is taking a while
04:23:53 <Sgeo> There's Linux XP, which I remember hating
04:24:16 * Sgeo likes linux mint, although I should delete the 3.0 iso
04:24:45 <edwardk> you might consider just tunefs'ing to lower the reserve to like 5-6%
04:25:05 <edwardk> or whatever it is in your distro
04:25:50 * Sgeo decides he will delete the file after recording the filenames
04:25:57 <Sgeo> Thank you so very much BTW
04:26:15 <edwardk> sitting here trying to get something to compile anyways ;)
04:26:15 <Sgeo> hmm Xandros 302-OCE is in there..
04:26:31 <Sgeo> And a Linspire ISO
04:27:37 -!- edwardk has quit (Read error: 104 (Connection reset by peer)).
04:27:55 -!- edwardk has joined.
04:28:02 -!- kwertii has quit (Client Quit).
04:28:22 <edwardk> try: tune2fs -m 5 /dev/sda1 (or whatever drive it was)
04:28:28 <edwardk> and see what that does for you
04:28:38 * Sgeo isn;t sure he wants to adjust that.. he's reclaiming space..
04:28:46 <Sgeo> I now have 3.1GB free
04:29:13 <edwardk> 5% is safe, the traditional 10% threshold was set back in the 10mb harddrive era ;)
04:30:04 -!- oerjan has joined.
04:32:56 * edwardk notes that apparently linux distros switched to 5% a while back.
04:52:04 * oerjan notes the discussion about a=b=c in plof
04:52:47 <oerjan> it would have been interestingly weird if a=b was equal to b as lvalue
04:54:01 <oerjan> unfortunately plof is not esoteric ;)
04:54:36 * oerjan mentions GregorR, just in case he didn't see that.
05:06:28 -!- wooby has joined.
05:07:06 * Sgeo deletes a 10GB file
05:07:38 <oerjan> was there a *slurp* sound?
05:08:55 <Sgeo> My comp seemed to freeze for two seconds, though
05:09:23 <oerjan> probably /dev/null has some indigestion problem.
05:47:06 * Sgeo will probably add some stuff to seek through File Descriptors next time he works on PSOX
06:02:56 -!- Sgeo has quit ("Ex-Chat").
06:56:24 -!- edwardk has left (?).
07:13:50 -!- puzzlet_ has quit (Read error: 104 (Connection reset by peer)).
07:25:41 -!- oerjan has quit ("leaving").
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
09:22:47 -!- wooby has quit.
10:02:30 -!- SEO_DUDE85 has quit (Remote closed the connection).
11:34:19 -!- SEO_DUDE85 has joined.
11:54:50 -!- jix has joined.
12:23:43 -!- ihope_ has joined.
12:23:49 -!- ihope_ has changed nick to ihope.
14:20:02 -!- Tritonio has quit (Remote closed the connection).
14:45:42 -!- sebbu2 has changed nick to sebbu.
15:02:21 -!- jix has quit (Nick collision from services.).
15:02:31 -!- jix has joined.
15:04:40 -!- UnrelatedToQaz has joined.
15:18:19 -!- UnrelatedToQaz has quit ("ChatZilla 0.9.78.1 [Firefox 2.0.0.7/2007091417]").
15:38:04 -!- UnrelatedToQaz has joined.
16:20:19 -!- edwardk has joined.
16:36:26 <ihope> It's another one of those greetings-only conversations.
16:36:39 <ihope> Hey all, ello, hi, hey, waves hello, hi, heya, ello.
16:49:26 <ihope> I think we can manage.
16:49:32 <ihope> Esoteric programming language discussion | FORUM AND WIKI: esolangs.org | CHANNEL LOGS: http://ircbrowse.com/cdates.html?channel=esoteric | IRP in #irp
16:49:55 <ihope> All aspects of mathematics | www.freenode-math.com/ | Don't ask to ask. Ask. | Guidelines: www.freenode-math.com/index.php/Guidelines | Writing maths on IRC: http://xrl.us/ubdh | LaTeX paste: http://mathbin.net | Using mbot: www.freenode-math.com/index.php/Mbot | Off-topic? #not-math (this is not a joke)
16:50:07 <ihope> And I think we have some room for actual content, too.
16:50:08 <UnrelatedToQaz> Did you know you can construct logic gates using dominoes?
16:50:22 <ihope> I've been trying to do that for a while, actually.
16:51:22 <UnrelatedToQaz> For some, though, you have to have an input and a process channel.
16:51:35 <ihope> Though my logic gates would be more like "holes" that can be filled with dominoes if and only if a certain thing is true.
16:52:02 <UnrelatedToQaz> That's a curious way of doing it. What do you mean, exactly?
16:52:57 <ihope> I'll pastebin a diagram sort of thing.
16:55:49 <oklokok> heh dominoes, gotta get some of those
16:55:50 <ihope> http://pastebin.ca/707096
16:56:07 <oklokok> i've been thinking of making a computer using water and pipes
16:56:49 <ihope> Each hole is really a logic gate of its own, and putting two holes next to each other connects them. Each connection can be either filled or empty, and each hole must have exactly one filled connection.
16:57:17 <ihope> oklokok: haven't we all? :-)
16:57:53 <oklokok> i'm sure we have, it's just my current dream :)
16:58:34 <UnrelatedToQaz> No wonder I'm so confused. That diagram refers to dominoes laying down; my logic gates use dominoes standing up.
16:59:02 <UnrelatedToQaz> I'll append something to yours to show you what I mean.
16:59:41 <oklokok> i don't know much about physics, but you'd think water would work almost the same in a circuit as electricity
16:59:55 <oklokok> it doesn't have the magnetism stuff electricity does, obviously
17:00:09 <oklokok> i don't exactly know how important that is in a computer
17:00:52 <oklokok> computers are dc internally, right?
17:01:11 <oklokok> then there shouldn't be much magnetism involved
17:01:39 <oklokok> i should start reading about this stuff... school hasn't taught me shit :<
17:04:00 <oklokok> i don't get the # notation
17:04:52 <ihope> oklokok: each # represents a hole the size of half a domino.
17:05:19 * ihope attempts to build a stick bomb out of pencils: http://en.wikipedia.org/wiki/Stick_bomb
17:05:35 <ihope> I expect that pencils are much too stiff to actually do this.
17:07:45 <oklokok> http://www.lunatim.com/kinart/videos/videos.htm omg
17:08:17 <ihope> Mm, testing a pencil shows that it's impossible to do a certain simple weave.
17:12:08 <SimonRC> http://www.rebelscience.org/Crackpots/notorious.htm
17:12:33 <SimonRC> I would laugh more, but he goes on too much abt why i am wrong and won't admit it.
17:18:10 -!- Tritonio has joined.
17:24:14 <oklokok> "First of all, dt/dt does not equal 1 second per second. The units cancel out."
17:31:34 <ihope> It can't be said that it doesn't equal 1 second per second, but "1" is indeed probably a better way of putting it...
17:42:48 <SimonRC> a more interesting vector is found if you multiply that one by the mass
17:43:01 <SimonRC> you get a mass-and-momentum vector
17:45:06 -!- Arrogant has joined.
17:53:15 <bsmntbombdood> http://abacus.kwzs.be/~bsmntbombdood/drains/il-7.jpg <--- me
17:57:24 -!- ehird` has joined.
18:13:41 -!- UnrelatedToQaz has left (?).
18:14:57 -!- Arrogant has quit ("Leaving").
19:28:40 -!- UnrelatedToQaz has joined.
19:30:24 <UnrelatedToQaz> Wow. I can't believe that all that's happened since I've been gone is that SimonRC has had dinner.
19:38:25 <oklokok> cool, i now have proof for something i claimed to my german teacher in the 5th grade
19:38:41 <oklokok> she would be so embarrassed if i showed this to her
19:39:55 <oklokok> (because who wouldn't remember a 7-year-old conversation vividly.)
19:45:47 -!- sebbu2 has joined.
20:04:55 -!- sebbu has quit (Connection timed out).
20:15:42 -!- UnrelatedToQaz has quit ("ChatZilla 0.9.78.1 [Firefox 2.0.0.7/2007091417]").
20:45:44 -!- oblivion2k has joined.
20:46:15 -!- oblivion2k has quit (Client Quit).
20:46:25 -!- oblivion2k has joined.
20:57:26 <oklokok> that germans occasionally way "zwo" for 2.
21:19:08 -!- ihope_ has joined.
21:36:12 -!- ihope has quit (Read error: 110 (Connection timed out)).
23:10:02 -!- edwardk has quit (Read error: 110 (Connection timed out)).
23:13:21 -!- bsmntbombdood has quit (Read error: 104 (Connection reset by peer)).
23:35:44 -!- bsmntbombdood has joined.
23:48:20 -!- ihope_ has quit (Connection timed out).
23:49:21 -!- bsmntbombdood has quit (Read error: 104 (Connection reset by peer)).