00:15:20 -!- FireFly has quit ("Leaving").
00:21:28 -!- bsmntbombgirl has quit (Read error: 101 (Network is unreachable)).
00:28:37 -!- Pthing has joined.
00:28:38 -!- ehirdiphone has joined.
00:33:05 -!- oerjan has quit ("Spyong").
00:35:56 -!- MigoMipo has joined.
00:36:31 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
00:56:23 -!- ehirdiphone has joined.
00:56:51 -!- ehirdiphone has quit (Client Quit).
01:37:24 -!- |MigoMipo| has joined.
01:37:58 -!- |MigoMipo| has quit (Remote closed the connection).
01:46:06 -!- MigoMipo has quit (Read error: 110 (Connection timed out)).
01:55:05 -!- coppro has quit (Remote closed the connection).
01:59:17 -!- BeholdMyGlory has quit (Remote closed the connection).
02:23:13 -!- coppro has joined.
02:29:19 -!- anmaster_l has quit (Read error: 60 (Operation timed out)).
02:48:20 -!- Slereah_ has quit (Read error: 60 (Operation timed out)).
02:51:14 -!- Slereah has joined.
03:22:11 -!- Slereah has quit (Read error: 110 (Connection timed out)).
03:27:47 -!- Slereah has joined.
03:29:37 -!- ehirdiphone has joined.
03:30:12 <ehirdiphone> Who wants to hear about my borderline-eso lang? :P
03:30:31 <ehirdiphone> (proof of esoness: it's more CS than haskell)
03:30:57 <ehirdiphone> but I already told you the basics yesterday :P
03:31:45 <ehirdiphone> (more to the point I wouldn't know where to start elaborating)
03:32:37 <ehirdiphone> soupdragon: If you as a specific question I can prolly answer
03:34:58 <soupdragon> it is just such a contrast that I am a bit confused by it
03:35:56 <ehirdiphone> What are you referring to? his present crisislessness?
03:36:45 <ehirdiphone> he has chronic depression and saw a therapist so presumably it's not doing its chronic thing right now
03:37:55 <ais523> also, I sometimes have late Internet nights deliberately, so I can talk to americans
03:38:11 <ais523> this time it's because it's rather snowy and I didn't want to walk home in it
03:38:22 <ais523> ehirdiphone: you'd have no idea how hard it is to internationalise NetHack
03:38:32 <ais523> but mostly, it's because Germany's closer than the US
03:38:38 <ais523> and lag is pretty important when playing NetHack
03:38:42 <ais523> anyway, what language?
03:39:05 <ehirdiphone> Unnamed. Borderline eso. More CS than haskell
03:39:32 <ais523> wait, what? is that even possible?
03:40:17 <coppro> rofl Talking to Americans
03:40:28 <ais523> coppro: why is that amusing?
03:40:51 <coppro> http://en.wikipedia.org/wiki/Talking_to_Americans
03:40:56 <pikhq> ais523: IO? *IO*? How dare you suggest such a thing.
03:41:04 <ehirdiphone> GUI and web and stuff? FRP which I won't bother explaining ATM
03:41:11 <ais523> pikhq: you can only imagine how hard it is in Feather
03:41:12 <pikhq> main is a function from String to String!
03:41:21 <ehirdiphone> ais523: Ask for an overview of the cool stuff! :P
03:41:27 <ais523> ehirdiphone: you know, you could just tell me
03:42:29 -!- Slereah_ has joined.
03:43:06 <ehirdiphone> ais523: Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension.
03:43:24 <ais523> let's start with syntactic extension first
03:43:56 <soupdragon> then what's the difference between Type level metaprogramming and Dependent types?
03:44:17 <ehirdiphone> Pretty simple. Modules can add to the syntax of the language, using arbritary code to make the replacement for the syntax
03:44:51 <ehirdiphone> soupdragon: The former means inspecting types themselves
03:46:04 <ehirdiphone> ais523: Do you know what dependent types are btw?
03:46:17 <ais523> I think so, but tell me anyway, because terminology is something I easily mess up
03:46:49 <ehirdiphone> In typed lambda calculus, types index on types and values index on values
03:48:10 <ais523> basically, creating types out of other types
03:49:11 <ehirdiphone> Typeclasses create values that index on types
03:49:30 <ehirdiphone> The value of the function show depends on what type it is
03:50:31 <ais523> like overloaded functions, but much more first-class and genreal
03:50:49 <ehirdiphone> ais523: Dependent types = types indexing on values
03:51:01 <ais523> oh, aha, I did know that, just forgotten I had
03:51:26 <ais523> so you can have a function that only takes even numbers as arguments, anything else is a typing error?
03:51:41 <soupdragon> okay but (=) means something dear to me
03:51:54 <ehirdiphone> Or a vector access function that enforces bounds checking
03:52:15 <ais523> sounds like what Splint tries and fails to do
03:52:36 <ais523> incidentally, I tried and failed to get my Underlambda interp fully Splint-compliant
03:52:41 <ais523> Splint seems really buggy
03:52:49 <ais523> some code I wrote had a bare block for scoping
03:52:53 <ais523> inside a switch statement
03:52:59 <ais523> if I put the break; inside the block, no error
03:53:03 <ais523> if I put it after the block, error
03:53:16 <ais523> even though the two sets of code were completely identical to any compiler
03:53:23 <ehirdiphone> ais523: Anyway, so dependent types makes programs more type Sade
03:54:03 <ais523> ehirdiphone: incidentally, this is how I think a really good BF optimiser would work
03:54:14 <ais523> trying to calculate dependent types for tape elements at different points in a program
03:55:12 <ehirdiphone> type Vararg 0 = (); Vararg n = () -> Vararg (n-1)
03:56:28 <ais523> actually, I think that's possible in Underload too, but a completely different way
03:57:03 <ehirdiphone> ais523: And this doesn't inspect n at runtime to determine the type!
03:57:17 <ais523> it's /statically/ correct
03:57:21 <ais523> we need more static correctness in the world
03:57:29 <ais523> you know, like Splint but actually working
03:57:31 <ehirdiphone> If n is say read from stdin you just must satisfy the compiler
03:58:19 -!- Slereah has quit (Read error: 110 (Connection timed out)).
03:58:43 <ais523> ehirdiphone: you probably want something along the line of C++'s dynamic_cast
03:59:18 <coppro> Did someone say C++? :P
03:59:18 <ais523> incidentally, for Cyclexa I was planning what's effectively typesafe /scanf/
03:59:29 <ais523> it physically wouldn't let the user input something of the wrong type
03:59:33 <ehirdiphone> type Printf ('%':'d':xs) = Integer -> Printf xs
03:59:55 * coppro will point out that C++ has lots of static correctness... too much, really
04:00:16 <soupdragon> yeah my C++ programs are statically correct.. the problems come when you run them
04:01:02 <ehirdiphone> "Dependent types. ML style module system. Type level metaprogramming. Arbritary syntactic extension."
04:01:03 <ais523> C++ doesn't normally enforce static correctness very fully
04:01:14 <ais523> unless you go and implement integers in the type system, or whatever
04:01:35 <coppro> ais523: That comment interests me... what do you mean by that?
04:01:39 <ais523> (apparently, someone won an IOI round like that once)
04:01:45 <ais523> basically, C++ templates are Turing-complete
04:01:59 <ais523> if you write a program in them, the whole thing gets run at compile-time
04:02:19 <soupdragon> ehird, you didn't answer my question (in such a way that I can understand it)
04:02:20 <coppro> do you mean that the type system doesn't allow distinguishing of values?
04:02:37 <ais523> coppro: not in C++, but you can use types themselves effectively as values
04:02:39 <soupdragon> you can do metaprogramming with dependent types
04:02:51 <coppro> ais523: I'm very familiar with C++, I just wanted clarification :)
04:03:07 <soupdragon> why don't the dependent types subsume metaprogramming?
04:03:10 * coppro remembers the WTFBBQ entry that created a separate type for every integer
04:03:30 <ehirdiphone> data Foo = Foo { a :: Integer, b :: Integer }
04:03:47 <ehirdiphone> With dependent types alone, you could not do
04:04:03 <coppro> http://thedailywtf.com/Articles/OMGWTF-Finalist-10-FerronCalc.aspx
04:04:57 <ehirdiphone> So basically inspecting and creating types programmaticslly in the type system
04:05:20 <ehirdiphone> soupdragon: Ask a mote specific question than what about
04:05:49 * coppro hopes to be at the 2010 IOI; possibly even as a competitor, though that seems unlikely due to stupid circumstances
04:07:11 -!- bsmntbombdood has joined.
04:07:16 <soupdragon> it seems like you have some kind of quotation for types
04:07:32 <soupdragon> (and that will have to include values too, because of the dependency)
04:07:41 <ehirdiphone> soupdragon: That "f Foo" was not runtime code
04:08:54 <ehirdiphone> I would write example code but not on the iph
04:11:25 <ais523> heh, you're reminding me of how every year when it comes round to exam time I realise I've almost forgotten how to write
04:11:48 <soupdragon> ais523, you do most things in your head? or on computer?
04:12:12 * coppro managed to get a computer for his English exam!
04:13:09 <ais523> ehirdiphone: I generally have plenty of paper
04:13:13 <ehirdiphone> About to write dependentkly typed code in a ruby on rails book yo
04:13:29 <ais523> I don't like putting my netbook down directly on a duvet or whatever as it blocks the air vents
04:13:37 <ais523> but it turns out it fits nicely onto an A4 pad of paper
04:13:50 * coppro is currently using a cookie tray
04:14:51 <ais523> coppro: I didn't realise cookie trays were even approximately TC
04:14:58 <ais523> ehirdiphone: ask your parents?
04:15:04 <coppro> ais523: for laptop ventilation
04:15:51 <ais523> maybe you should just wait until morning
04:22:10 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
04:24:13 -!- ehirdiphone has joined.
04:24:39 <ehirdiphone> Can you imgur.com it and link the directvlink here?
04:24:40 <ais523> incidentally, filebin.ca's getting reported as a malware site by Firefox
04:26:13 <ais523> http://imgur.com/n5amE.jpg
04:26:42 <ais523> what did you write it /on/? I hope you haven't damaged a book for our sake
04:27:56 <ais523> ehirdiphone: you might have been able to sell on that book...
04:29:20 <ehirdiphone> ais523: The book is way out of date anyway
04:29:36 -!- adam_d has quit (Read error: 110 (Connection timed out)).
04:30:41 <Gracenotes> that's true. then again this laptop isn't exactly turing-complete
04:31:36 <Gracenotes> given that I can't even allocate enough space to linearly bound any given input size, I'm not quite sure it's context-sensitive
04:32:27 <soupdragon> so called "computers" don't compute anything
04:32:32 <ais523> it looks just like OCaml
04:32:52 <ehirdiphone> It's haskell but with dependent types and type metaprogramming
04:33:07 <ais523> well, they're pretty similar syntactically
04:33:18 <ais523> and I'm more used to OCaml, I think
04:33:30 <pikhq> ehirdiphone: So, "Let's start with what Haskell gets right, and go from there".
04:33:38 <ehirdiphone> ok, so the final topic is... The module system!
04:34:06 <ehirdiphone> pikhq: Actual syntax will differ quite a bit
04:34:39 <pikhq> Gracenotes: MURDER.
04:34:53 <ehirdiphone> And, might be strict not lazy, both for the added safety and because iirc a general implementation of lazy FRP is unsolved problem
04:35:09 <ehirdiphone> soupdragon: Mine is not just for nanespaces!
04:35:10 <pikhq> soupdragon: A modern language without a module system is a crime.
04:35:23 <ehirdiphone> Indeed they are even more powerful than MLs
04:35:33 <ais523> ah, how did you make them interesting?
04:35:57 <pikhq> ehirdiphone: ... ?
04:36:01 <ehirdiphone> ais523: Will explain immediately after haskell modules bashing
04:36:12 <pikhq> We may be using words differently. Explain.
04:36:41 <pikhq> I consider that a somewhat simplistic module system.
04:36:55 <pikhq> Of course, my background is C-heavy, so... Yeah.
04:37:29 <ehirdiphone> Will use ml haskell hybrid syntax for this explain
04:39:48 <ehirdiphone> type List = module { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer }
04:40:42 <ehirdiphone> signature { type T; empty :: T; add :: Integer -> T -> T; length :: T -> Integer }
04:41:05 <ehirdiphone> This is a signature. Signatures -- modules as types -- values.
04:42:01 <ehirdiphone> ais523: Just explaining mls stuff first for pikhq
04:42:17 <ehirdiphone> Here's an implementation of that signature
04:43:20 <ehirdiphone> module List { type T = [Integer]; add x xs = x:xs; length xs = theLanguagesLengthFunction xs }
04:43:37 <ehirdiphone> We could say that that module :: that signature
04:44:37 <ehirdiphone> So, List.T is a type. BUT! If we, in our interface file (basically just the types of things),
04:45:04 <ehirdiphone> Put module List :: signature { that signature }
04:46:50 <ehirdiphone> Because the implementation of T is not exposed
04:47:12 <ehirdiphone> It's conceivable that two modules might have the same signature
04:48:15 <ehirdiphone> So we have functors. A functor is basically a module that takes other modules as arguments
04:49:06 <ehirdiphone> functor Silly (List :: signature { long signature is long }) = module {
04:49:49 <ehirdiphone> main = print (List.length (List.add 2 foo))
04:50:37 <ehirdiphone> (extracts everything into the current module)
04:51:06 <ehirdiphone> pikhq: So we have implementation agnostic modules
04:52:01 <ehirdiphone> Combined with my type level metaprogramming (did you understand the photo?)
04:53:45 <Gracenotes> oh.. what the hell. http://www.xs4all.nl/~weegen/eelis/analogliterals.xhtml
04:53:50 <ehirdiphone> pikhq: ais523 (here is where it departs from ml)
04:54:03 <coppro> Gracenotes: one of Eelis' finest creations
04:55:04 <Gracenotes> I am feeling the joy of human creation simultaneously tinged with desperate sorrow
04:55:20 <ais523> reminds me of Acme::Don't in Perl
04:55:25 <ais523> which was a similarly silly syntax trick
04:55:36 <pikhq> ehirdiphone: That photo...
04:56:07 <Gracenotes> ais523: not sure it's on the same scale
04:56:21 <Gracenotes> you know, ehirdiphone, many of us do use pastebins
04:56:38 <ais523> Gracenotes: maybe not, but apostrophes in keyword names are still epic
04:58:13 <coppro> Don't is a syntax trick?
04:58:18 <pikhq> I just commented on it, in fact.
05:00:22 <ais523> it's equivalent to Don::t using an outdated syntax
05:00:33 <ehirdiphone> pikhq: Who says functor arguments have to be modules? why not types?
05:00:36 <coppro> oh right, now I remember
05:01:58 <coppro> I only have one complaint
05:02:09 <coppro> Specifying the type independently from the value seems blah
05:02:16 <coppro> if they are effectively identical
05:02:25 <ehirdiphone> data Foo { a :: Integer, b :: String, c :: Bool }
05:03:51 <coppro> it's 4 am, you're hard to folllow
05:04:09 <pikhq> That's... Pretty spiffy.
05:04:27 <coppro> I think I get it, and it's neat
05:05:01 <ehirdiphone> The uber cool thing is how all this has no runtime penalty
05:05:09 <coppro> interesting fact I just discovered: Google appears not to offer any search suggestions for searches beginning with "sexy". "sex" is fine, as is "sexiness", but not "sexy".
05:05:32 <coppro> ehirdiphone: Actually, as much as you're going to hate me for saying this, C++ helps too
05:05:33 <ais523> ehirdiphone: pretty much
05:05:43 <pikhq> ehirdiphone: Good God most of that is easily done at compile-time, isn't it?
05:05:54 <ehirdiphone> copproSpecifying the type independently from the value seems blah
05:06:22 <coppro> ehirdiphone: One of your earlier examples, if I read correctly, had you specifying the type and the value of the function redundantly
05:06:37 <coppro> if I misread, my problem, not yours
05:07:14 <coppro> [20:54:48]<ehirdiphone>type Vararg 0 = (); Vararg n = () -> Vararg (n-1)
05:07:16 <coppro> [20:55:00]<ehirdiphone>vararg 0 :: ()
05:07:18 <coppro> [20:55:10]<ehirdiphone>vararg 1 :: () -> ()
05:07:19 <coppro> [20:55:42]<ehirdiphone>Implementation if vararg itself:
05:07:21 <coppro> [20:55:52]<ehirdiphone>vararg 0 = ()
05:07:23 <coppro> [20:56:10]<ehirdiphone>vararg n () = vararg (n-1)
05:07:40 <ehirdiphone> coppro: Ah. That is only because the example is trivial
05:07:58 <ehirdiphone> In my soon after printf example you could easily see the difference
05:08:30 <coppro> just wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates
05:08:39 <coppro> hmm... I'm going to go buy some food
05:08:47 <ehirdiphone> Or just let the compiler infer the type! (yeah right, even haskell can't infer the type in all cases)
05:09:12 <ehirdiphone> (literally impossible for my Lang due to TC type system)
05:09:12 <coppro> ehirdiphone: yeah, they've added it for lambda functions but not for regular ones
05:09:26 <pikhq> Type inference is kinda impossible to do in the general case...
05:09:33 <pikhq> And even more so for TC types.
05:09:45 <ehirdiphone> pikhq: Haskell sans typeclasses is inferrable totally
05:10:08 <pikhq> Haskell sans typeclasses is perhaps even *trivially* inferrable.
05:10:26 <coppro> currently, a generic add functor in C++0x currently looks like this: template <typename T, typename U> auto add (T t, U u) -> decltype(t+u) { return t+u; }
05:10:39 <coppro> (at least it's better than the current mess *shudder*)
05:10:55 <coppro> [22:08:06]<coppro>just wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates
05:11:14 <soupdragon> type inference for functions that work on GADTs
05:11:40 <coppro> ehirdiphone: lambda functions are allowed to infer types on bodies of "{ return foo;}", but IIRC this hasn't been added for normal functions
05:12:10 <ehirdiphone> copprojust wanted to make sure that a generic functor wouldn't have to specify its type independently from the value; one of the major issues with C++'s templates
05:12:42 <coppro> ehirdiphone: I just gave an example; "t+u" is redundant
05:13:12 <coppro> compare to a lambda (no polymorphic lambdas atm): "[](int t, int u) { return t+u; } // inferred return type int"
05:13:21 <coppro> the -> foo is the return type
05:13:31 <ehirdiphone> ehirdiphoneIn my soon after printf example you could easily see the difference
05:13:42 <coppro> it appears after the parameter declaration so the parameters are visible
05:13:51 <ehirdiphone> coppro: When you pinger me snout the I ferrencr only being for lambda
05:14:12 <coppro> okay, I think I'm assuming too much about your knowledge of C++
05:14:17 <ehirdiphone> Read the lines I said before with out your c plus plus stuff
05:14:40 <ehirdiphone> I was just continuing what I said with a quip
05:14:59 <coppro> how about we restart altogether?
05:15:27 <coppro> basically: Make sure that in trivial cases, it's possible to specify a function without specifying the type in a redundant manner
05:15:30 <ehirdiphone> I'm aiming to have no gc w my Lang! If it's possible
05:15:43 <coppro> gc w? garbage collection with?
05:16:27 <coppro> I've always been interested in the notion of graph-based collection
05:16:50 <ehirdiphone> It'd, among other things, let small integers use a full word
05:16:51 <coppro> specifically with the goal in mind that an object is destroyed as soon as its references become invalid
05:17:04 <ehirdiphone> No need for a tag so the gc knows what's a pointer
05:17:30 <coppro> anyway, I'm actually leaving to get food now; if you have anything important to say, ping me or comment when I get back
05:17:44 <pikhq> ehirdiphone: If you can do it, then it would be quite nice.
05:18:15 <ehirdiphone> pikhq: A cool thing arising from all this sweet language nectar:
05:18:50 <ehirdiphone> You can malloc some memory, access it at will, realloc it, etc, with no runtime penalty, SAFELY.
05:22:01 <ehirdiphone> ptradd :: (n::Int) -> MemBlock m -> MemBlock {n-m}
05:23:41 <ehirdiphone> access :: (n::Int) -> MemBlock m -> {n < m} -> Int
05:24:02 <ehirdiphone> called as (access n block) if no proof is required
05:24:37 <pikhq> So, you could use this language much like C. ... Except you're not going to shoot a foot with it.
05:25:36 <ehirdiphone> pikhq: I'm targetting performance because Ur has quite a bit of this stuff and generates objects with little overhead, lots of speed and little memory usage in it's domain
05:26:08 <ehirdiphone> Dependent types = can make more compile time assumptions
05:26:27 <ehirdiphone> And if you did some wizardy GHC style optimisation too?
05:27:18 <pikhq> ehirdiphone: Because of the annotations given to the compiler, optimization would be (relatively) easy.
05:27:42 <ehirdiphone> Hey, if I had no gc and small ints took up the word arithmetic would be 1 instructiob
05:27:46 <pikhq> Much less "checking to be sure this is safe", more with the "just transform it to the equivalent".
05:29:56 <ehirdiphone> soupdragon: Iphone bitch. Be glad im not using text speak
05:30:41 <ehirdiphone> A compiler that does all the things I want will prolly be like 20,000 lines of haskell or more :-(
05:31:05 <ehirdiphone> Maybe even 50,000—70,000 depending on compiler smartness
05:31:35 <ehirdiphone> 100,000 if I want readable error messages :P
05:34:32 <ehirdiphone> I don't even want to write the compiler in another language. Too many opportunities for sweet uses of the lang's features
05:34:58 <pikhq> If you absolutely must write it in a different language, must be Haskell.
05:35:16 <pikhq> It just makes language implementation... Feel right.
05:36:45 <ehirdiphone> (advantages of ML: Usually faster, module system (think e.g. compiler is a functor taking backend module), if I choose to make the language strict it matches the semantics better, that just feels... more right)
05:37:59 <ehirdiphone> It occurs to me that a worthy Emacs mode would be a mode to end all modes
05:38:25 <ehirdiphone> Probably the largest piece of elisp ever. :P *shudder*
05:39:27 <ais523> will it allow impureness?
05:45:17 <ehirdiphone> Well, maybe if you have "pragma unsafe" in your module and import Internals.
05:45:51 <ehirdiphone> But every module using yours must be pragma unsafe too
05:46:15 <ehirdiphone> coppro: I said interesting things right after you left
05:46:39 <ehirdiphone> do I have to repeat them or do you have sufficient scrollback?
05:47:38 <pikhq> ehirdiphone: Yeah, if you have well-defined evaluation order, "pragma unsafe" is perfectly reasonable.
05:48:32 <ehirdiphone> That's just how you do forall in dependently typed langs
05:51:11 <ehirdiphone> So! I hope you all now worship my language and know it will subsume and supersume every other language forever.
05:51:15 <coppro> ehirdiphone: very interesting
05:51:30 <ais523> ehirdiphone: not until it has a really good impl
05:51:33 <ehirdiphone> Or, more seriously, I hope you all now think my language is pretty cool.
05:52:04 <ais523> ehirdiphone: does it compile easily into all TC esolangs?
05:52:17 <ais523> or does it not want to tread on Underlambda's design space?
05:52:28 <coppro> ehirdiphone: region inference
05:52:30 <pikhq> REMOVE ALL OTHER LANGUAGES. THEY ARE INSUFFICIENTLY COOL.
05:52:49 <ehirdiphone> ais523: No, but you can have a compile time BF compiler.
05:53:04 <coppro> one thing I want to clear up before I talk about the language as a whole; by "dependent types" you mean a function whose type can change based on the value of its arguments, correct?
05:53:38 <ehirdiphone> coppro: Not just functions. It is simply: types can take values as arguments
05:54:04 <ehirdiphone> Full explanation is way back in the scrollback
05:54:38 <ehirdiphone> Careful. It's been an hours-long explanation.
05:55:24 <ehirdiphone> Btw I haven't thought of a syntax at all yet.
05:55:35 <ehirdiphone> Just been blending haskell and ml for this talk
05:55:46 <coppro> ehirdiphone: so, basically, template<int I> vs. template<typename T>?
05:56:22 <coppro> (except applicable to all types, not just a very small subset of those available)
05:58:06 <ehirdiphone> And pass it to a function expecting an even number
05:58:07 <soupdragon> you can erase all types into a NULL value, and then eval the real values like an untyped language
05:58:30 <ehirdiphone> Perhaps it can infer it if you do a branch
05:58:47 <soupdragon> (because you can't do case analysis on types)
05:59:01 <coppro> so... attempting another gross oversimplification here... encoding the range of values into the type?
05:59:21 <ais523> more like set of values, only it's allowed to be infinite
05:59:35 <ais523> and you can have loads of types which are similar except in the value sets, automatically generated
05:59:58 <ehirdiphone> You just have to manually satisfy them if the compiler can't
06:00:15 <coppro> The type of an object might be "even integer", whereas another object might be of the type "prime integer"; true or false
06:00:17 <ehirdiphone> If we need an even number, pass a proof that it's even
06:00:52 <coppro> ok, now I'm really confused
06:01:32 <ehirdiphone> Don't worry, it's pretty intuitive in practice
06:01:41 <coppro> There's a certain ACC quote which has never appeared more applicable to the situation
06:01:50 <ehirdiphone> Feels like you're doing the impossible though
06:02:15 <coppro> Like, I understand the notion
06:03:34 <ehirdiphone> Basically, your job as the programmer is: when the compiler can't make inferrences about your values so that it does not matter what they actually ARE at runtime because the type is satisfied no matter what,
06:04:02 <ehirdiphone> (which is just... Writing the code that shows it, basically)
06:04:41 <coppro> like, I get the net effect
06:05:20 <ehirdiphone> Even I don't know the actual inferrence algorithms. I'm going to defer breaking my head that much until I absolutely must
06:05:21 <coppro> it's statically-enforced value control
06:05:52 <ehirdiphone> coppro: But also value liberator, remember the printf?
06:07:00 <ehirdiphone> Lets you express stuff you can't otherwise
06:07:30 <coppro> Now, I admit I don't program in functional languages as much as I'd like, so bear with me here
06:08:03 <coppro> this looks to me a lot like pattern-matching being done at compile time, with an error if nothing matches
06:08:35 <ehirdiphone> Can you elaborate? My mind is rejecting that metaphor.
06:08:57 <coppro> My pattern matching experience is with Erlang, it may be different elsewhere
06:11:23 <coppro> in Erlang, you could do something like printf ([%%, %d, RestOfString], [SomeInteger, RestOfArgs]) -> printAsInteger(SomeInteger), printf(RestOfString, RestOfArgs).
06:11:50 <ehirdiphone> The type was pattern matching on the string
06:12:23 <ehirdiphone> It was just a type with the kind (type's type) String -> Type
06:12:35 <coppro> but now, let's take a scanf example
06:12:56 <coppro> in that case, you are pattern matching on the string and affecting the return type of the function
06:14:07 <coppro> but scanf is a more interesting example
06:14:21 <coppro> but so basically your idea is to be able to check this at compile time
06:14:40 <coppro> and complain if there's any chance there might be an error
06:14:54 <coppro> rather than simply waiting around and hoping things come out right
06:15:24 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
06:15:36 -!- ehirdiphone has joined.
06:15:36 <pikhq> His plan is to have the type of printf be dependent upon the string given as its first argument.
06:15:41 <pikhq> His plan is to have the type of printf be dependent upon the string given as its first argument.
06:15:47 <pikhq> (repeated for sake of ehird)
06:15:56 -!- Sgeo_ has joined.
06:16:03 -!- Sgeo_ has quit (Read error: 104 (Connection reset by peer)).
06:16:09 <pikhq> ehirdiphone: ... After you left?
06:16:17 <pikhq> You've got some crazy log-reading skills.
06:16:40 <coppro> it appeared to me to occur right after he arrived
06:17:29 <ehirdiphone> copprorather than simply waiting around and hoping things come out right
06:17:38 <coppro> ehirdiphone: well... basically, suppose I do printf(some_user_string, 3)
06:18:17 <ehirdiphone> That would simply give a type inferrence error
06:18:56 <ehirdiphone> if s == "%d" then printf s 3 else return ()
06:19:43 <ehirdiphone> Not sure where the proof would go for printf actually
06:19:44 <coppro> I think we're wasting our time
06:19:52 <coppro> yeah, printf would be a nasty proof
06:20:24 <ehirdiphone> Just prove that (printf s) :: Integer -> IO ()
06:20:27 <coppro> well, now I know we agree about the basics
06:21:28 <ehirdiphone> Don't pass a user string to printf, you dumb fuck. ;)
06:21:45 <coppro> Sadly, that's when printf becomes most useful
06:21:56 <coppro> localization, specifically
06:22:22 <coppro> It may be loaded from a file
06:22:37 <coppro> for 30 different languages? no thanks
06:22:53 <coppro> anyway, we're getting sidetracked
06:24:09 <coppro> we're getting sidetracked
06:24:17 <coppro> my basic question is how this relates to the notion of types
06:24:18 <ehirdiphone> big_error = printf "OLE OLE SUPER ERROR %d"
06:24:36 <coppro> using one of your examples, suppose I have a function that takes an integer that must be even
06:24:39 <ehirdiphone> You could use syntactic extension to make that nicer for the translators
06:25:22 -!- cal153 has quit.
06:25:43 <ehirdiphone> With the latter hopefully being inferred by the compiler
06:26:05 <coppro> this makes it feel even more Erlangish to me
06:26:52 <coppro> Erlang: my_function (I) where is_int(I) and I mod 2 == 0 -> whatever
06:28:47 <coppro> but so, for the purposes of the definition, which type is dependent on which value? The type of my_function is dependent on the value of n
06:29:29 <coppro> ok... so what is a "proof"?
06:29:35 <ehirdiphone> coppro: The type of the poop argument is dependent on the value of the number argument
06:29:47 <coppro> ehirdiphone: but the poop argument doesn't really exist
06:30:16 <coppro> btw, can you just type in a pastebin rather than a picture?
06:31:12 <ehirdiphone> evenClub :: (n::Integer) -> {Even n} -> AwesomeParty
06:31:30 <coppro> also, btw, ZREO finished OoT finally; it's awesome
06:31:57 <coppro> not talking about anything relevant
06:32:31 <ehirdiphone> Since the third param must be of type Even 2
06:32:39 -!- Sgeo has quit (Read error: 110 (Connection timed out)).
06:32:56 <ehirdiphone> Obviously, the poop param is erased during compilation
06:33:13 <coppro> that's an interesting way for it to be thought of, and I wonder if it's the correct one, but at least I understand now :)
06:34:17 <ehirdiphone> The issue is that you need to make a type Even which is a drag BUT
06:34:43 -!- jpc has quit (Read error: 110 (Connection timed out)).
06:34:49 <ehirdiphone> type IsTrue True = PoopHaven; IsTrue False = NoValuesForYou
06:36:20 <ehirdiphone> coppro: So, hopefully you at least grok it as well as I do now.
06:36:41 <coppro> ehirdiphone: I now understand.
06:36:54 <ehirdiphone> The whole language pretty much clicked into place combining seeing Ur with my past musings
06:37:08 <coppro> I question whether it would be more effective to attempt to accomplish the goal through a different mechanism
06:37:35 <ehirdiphone> Explaining it is the single most difficult part
06:37:52 <coppro> specifically, of encoding a known subset of values into the type of an object
06:38:11 -!- calamari has left (?).
06:38:17 <ehirdiphone> Using it? Pretty easy. And a dependently typed lambda calculus is just a few lines of code onto a normal typed one
06:38:53 <ehirdiphone> If you mean what I think Iean that cannot accomplish remotely as much sscdependent types
06:39:03 <coppro> I think they're equivalent
06:39:24 <coppro> (note, this is in the "this is a theory" form of "I think", not the "I'm pretty sure I'm right" form)
06:39:34 <ehirdiphone> ais523: maybe dependent types are the key to feather :P
06:40:55 <coppro> basically, in your evenClub example, what you've actually done is included a "virtual" type (in the sense that the caller doesn't noticed it) to the signature
06:41:04 <ehirdiphone> coppro: #agda is full of people who will know more than I btw if I don't grok it
06:41:17 <coppro> ehirdiphone: just wait
06:42:00 <coppro> I'm not trying to debate the way Agda does
06:42:07 <coppro> I'm trying to find another approach to the same solution
06:42:09 <ehirdiphone> Then that would break if you remove the {}s
06:42:40 <ehirdiphone> Remember dependent types are more than just yes no
06:42:42 <coppro> my idea is that { Even n } is not seen as an extra parameter, but rather a constraint
06:42:52 <coppro> ok, restate printf for me
06:44:00 <coppro> ok, I think I get your point
06:44:10 <coppro> ehirdiphone: how much do you know about C++ templates?
06:46:00 <coppro> ehirdiphone: do you know what enable_if is?
06:48:10 <coppro> ok, well, enable_if is a template taking a boolean and a type; if the boolean condition is satisfied, a member type exists; if the condition is not satisfied, the type does not exist
06:48:32 <coppro> this is in many ways similar to the use of a predicate in { Even n }
06:49:18 <coppro> true, but the principle is the same
06:49:35 <coppro> I can if I consider only templates and not the C++ runtime
06:49:37 <ehirdiphone> The whole model I said is to make that work
06:50:20 <coppro> well, allow me to continue
06:50:57 * coppro tries to remember where he's going wit hthis
06:51:23 <coppro> in the case of enable_if, you can implement arbitrary conditionals assuming appropriate predicates exist
06:51:38 <coppro> but there is another way of accomplishing the same task, and that is with restrictions on the arguments
06:52:01 <coppro> there was a proposed feature for C++0x called concepts that would do exactly this; it would provide the ability to constrain template arguments
06:52:32 <coppro> on one level, it's largely sugar, but the underlying notion is different
06:52:57 <coppro> sure, but templates exist as a compile-time system
06:53:08 <ehirdiphone> What you're doing is taking a hard problem
06:53:21 <ehirdiphone> Explaining the solution to an easy problem
06:53:26 <coppro> I'm wondering if dependent types can be implemented in the same way, with compiler-managed contraints rather than predicates
06:53:37 <coppro> the whole C++ thing was an analogy; it's not perfect
06:55:11 <coppro> tbh, I think I need to see a bigger example of your language before I can explain this more clearly
06:55:28 <coppro> since it's hard to explain without a concrete base to work from
06:55:44 <coppro> I don't know if there's an advantage
06:56:05 <coppro> if I sought an advantage in everything I did, I wouldn't be here chatting, I'd be finished my backload of homework
06:56:29 <ehirdiphone> So... Replacing an existing concept with a less simple one. And you have to keep the old one anyway.
06:56:39 <coppro> I don't think you'd need to keep the old one
06:57:08 <coppro> that's part of my issue; I'd need to see a complete example of printf
06:57:15 <coppro> not just "here's my signature kthxbye"
06:57:53 <coppro> not enough, at least not me looking through scrollback
06:58:11 <ehirdiphone> It's right after the printf signature you dolt
06:58:49 <soupdragon> [] ++ ys = ys ; (x::xs) ++ ys = x::(xs ++ ys).
06:58:51 <coppro> ah, I see, I think I just misunderstood the synta
06:59:14 <soupdragon> _+_ : N -> N -> N, _++_ : Vector A n -> Vector A m -> Vector A (n + m)
07:00:55 <coppro> okay, hang on, I'm going to repaste this
07:01:19 <coppro> 19:58:20 <ehirdiphone> printf :: (fmt :: String) -> Printf fmt
07:01:21 <coppro> 19:58:39 <ehirdiphone> type Printf [] = IO ()
07:01:24 <coppro> 19:59:33 <ehirdiphone> type Printf ('%':'d':xs) = Integer -> Printf xs
07:01:25 <coppro> 20:00:05 <ehirdiphone> type Printf (x:xs) = Printf xs
07:01:46 <coppro> so where does the type replacement come in to play here?
07:03:10 <coppro> I misunderstood the way functions work
07:03:35 <coppro> specifically, "a b" is a left-associative operator that executes a on b
07:03:55 <coppro> for multi-arg functions, there's syntactic sugar in the declaration that creates a forwarding function with less arguments
07:04:48 <coppro> as I said, my functional programming experience is sadly lacking :(
07:05:06 <coppro> anyway, this helps clear up a lot, though all it ends up doing is making my idea a lot harder to express
07:05:33 <coppro> absolutely there's currying there
07:05:38 <soupdragon> I don't see what currying has to do with any of it
07:06:32 <coppro> yeah, it returns a function
07:07:07 <coppro> printf "%d" gives me an Integer -> IO, correct?
07:07:47 <coppro> oh wait, that was soupdragon
07:07:57 <coppro> ok, nvm. Your nicks have a too-similar length
07:08:14 -!- ehirdiphone has changed nick to pooop.
07:09:02 <coppro> pooop: Okay, I'm going to try again and try to explain what I was trying to explain before, now with more knowledge of where it isn't relevant
07:09:15 <pooop> coppro: By nickname laws I think you have to have sex with me now. If I was poop I'd need copro
07:09:21 <pooop> But pooop is coppro
07:09:32 -!- coppro has changed nick to Cu.
07:09:54 <pooop> Cu: EVADING THE LAW??
07:10:08 -!- pooop has quit (Remote closed the connection).
07:10:23 -!- ehirdiphone has joined.
07:10:46 <ehirdiphone> Repeat the line you said before the poop shit (which was crap)
07:10:53 <Cu> Okay, I'm going to try again and try to explain what I was trying to explain before, now with more knowledge of where it isn't relevant
07:11:26 <Cu> is there any name for the use of {} in functions?
07:11:32 <Cu> that I can use to conveniently refer to it?
07:11:43 <ehirdiphone> Agda probably has one. Lets call it zooping
07:11:54 <ehirdiphone> It bears some resemblence to the nomic use.
07:12:40 <ehirdiphone> Zoop is the argument or the action of Ingerring a value?
07:12:58 <Cu> so, when you zoop an argument, what you are doing is providing an imaginary argument that the compiler magically inserts based on some value
07:13:19 <Cu> imaginary in the sense that the user never sees it
07:13:29 <Cu> otherwise, 100% real
07:13:36 <ehirdiphone> It exists. If you want to you can use it in the function
07:14:54 <ehirdiphone> But {} does not require the type to be dependent.
07:15:01 <Cu> wait, let's step back, I just realized there's something I don't get
07:15:13 <Cu> Even n is a family of types, one for each integer, all sharing the same values?
07:15:46 <ehirdiphone> All the even ns share the same value, poop
07:16:11 <ehirdiphone> I.e you cannot have a value of type Even 1
07:16:47 <Cu> so, my question is does this mechanism, specifically when used for zooping, have any advantage over a predicate that is used as part of the type matching?
07:17:07 <Cu> yessir, I get that
07:18:00 <ehirdiphone> Also, no, except for being simpler, having an obvious way to pass proofs, and being the same mechanism that things like printf use
07:18:14 <ehirdiphone> All of which make me very skeptical of your idea.
07:18:32 <Cu> ok, so, ignore q1, that's sort of academic at this point as I'm trying to simplify it
07:18:44 <Cu> point 1, whatever
07:18:53 <Cu> point 2, I don't quite understand
07:18:59 <Cu> point 1 = simpler
07:19:07 <Cu> point 3, I'm not sure is related
07:19:43 <Cu> I was sort of missing that bit
07:19:45 -!- Cu has changed nick to coppro.
07:19:51 <ehirdiphone> I.e. If there is an {} arg at this position, {} passes one In explicitly
07:19:59 -!- puzzlet has changed nick to puzlet.
07:20:06 -!- puzzlet has joined.
07:20:22 <soupdragon> if you defined Even : nat -> * as a data type
07:20:28 <coppro> lack of information is a dangerous thing
07:20:31 <soupdragon> you could maybe erase the index to get Even : *
07:20:44 <soupdragon> and then you've got a data type that represents even numbers
07:20:45 -!- puzlet has quit ("leaving").
07:21:15 <coppro> Ugh, just discovered a major flaw with ZREO's "official" OoT release
07:21:22 <coppro> gonna have to complain
07:22:03 -!- puzzlet has quit (Client Quit).
07:22:10 <ehirdiphone> type Even n | even n = Poopy; type Even _ = Lame
07:22:22 <soupdragon> data Even : nat -> * where EZ : Even Z ; ES : Even n -> Even (S (S n))
07:22:37 -!- puzzlet has joined.
07:22:49 <soupdragon> data Even : * where EZ : Even ; ES : Even -> Even
07:23:11 <ehirdiphone> writing a boring type for every constraint
07:24:12 <coppro> ZREO = Zelda Reorchestrated, an awesome project to redo Zelda music in awesomeness
07:24:20 <coppro> they released the OoT soundtrack today
07:24:40 <coppro> except half the Ocarina songs are Ocarina-only, and half are full music
07:24:50 <coppro> one way or the other I could see, but half-and-half?
07:25:15 <coppro> (I highly recommend downloading it, btw)
07:26:15 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
07:26:27 -!- ehirdiphone has joined.
07:26:43 <ehirdiphone> My language will have not only infix operators
07:27:30 * coppro doesn't hold his breath
07:28:43 <coppro> well, agda allows you do define things pretty much however you want
07:29:06 <ehirdiphone> Did you research Agda in the time since I mentioned it? :P
07:29:29 <coppro> ehirdiphone: yes. This is the Internet. I'm pretty confident you do the same thing from time to time.
07:29:44 <coppro> Perl 6 is the only other language I could think of offhand that allows the definition of new infix, prefix, and postfix operators
07:30:28 <coppro> you also tend to keep your mouth shut when something you don't understand comes up, thus increasing others' perception of you (I do this too, but you're way better at it)
07:30:48 <ehirdiphone> I just have that you can name a function (infix/prefix/postfix symbols)
07:31:29 <coppro> ehirdiphone: I mean something you don't understand AND can't readily Google
07:31:59 <coppro> ehirdiphone: ok. The only issue is the syntactical ambiguities that can arise
07:32:07 <coppro> if you allow all three to be overloaded on the same operator
07:32:20 <coppro> two of the three is fine
07:32:30 <ehirdiphone> infix + :: {n::Type} -> {Num n} -> n -> n -> n
07:33:11 <ehirdiphone> prefix ? :: {t::Type} -> Ref t -> SomeMonad t
07:33:37 <ehirdiphone> coppro: I'd just use operator precedence to disambiguate
07:34:00 <coppro> I forget what method Perl 6 uses... something evil
07:34:12 <ehirdiphone> (you can define your own precedence and left right association)
07:34:31 <ehirdiphone> ehirdiphoneinfix + :: {n::Type} -> {Num n} -> n -> n -> n
07:34:59 <coppro> you defined your own keyword there?
07:35:17 <coppro> what does {n::Type} mean?
07:35:22 <coppro> inference of n's type?
07:35:37 <ehirdiphone> coppro: You know what (n::Int) means right?
07:35:56 <coppro> magic dependent value?
07:36:01 <coppro> I thought of it as "named n"
07:36:27 <coppro> {} means infer the type, and let me refer to it as Type?
07:38:07 <coppro> so t becomes whatever the argument's type is?
07:38:26 <coppro> could I do {n::t::Type} ?
07:38:27 <ehirdiphone> If we pass it an argument if a certain type
07:38:33 <soupdragon> This sentence is syntactically unambiguous.
07:39:21 <ehirdiphone> infix + :: {n::Type} -> {Num n} -> n -> n -> n
07:39:59 <coppro> it's an infix that appears to take 3 arguments?
07:40:55 <coppro> oh, yeah, I'd worked that bit out
07:41:48 <coppro> for some reason it was particularly plain to me that {Num n} meant that the type n is some number
07:42:17 <ehirdiphone> coppro: Were you around for the module system stuff?
07:42:35 <coppro> ehirdiphone: no, but I am familiar with the notion of metatypes, which is why I think that bit came so easily
07:43:27 <coppro> http://tunes.org/~nef/logs/esoteric/09.12.29
07:43:36 <coppro> yeah, I didn't think they were related
07:43:40 <ehirdiphone> So I can findvwhere it is; it really is one of the best parts of the language IMO
07:43:42 <coppro> that didn't quite come out right
07:43:53 <coppro> was that the bit about open Foo?
07:44:47 -!- cal153 has joined.
07:45:00 * coppro wonders why he feigns stupidity in this channel
07:45:23 <soupdragon> probably so that guys have a chance to show how smart and alpha they are
07:47:22 <coppro> ah, now I remember another question I had, and realized you'd answered it
07:47:57 <ehirdiphone> coppro: Btw there's a blip in the module talk
07:48:56 <coppro> right, I remembered that vaguely
07:49:17 <coppro> whether you would have full-on type genericism
07:49:43 <coppro> specifically, the ability to make an entire interface dependent on another type
07:49:56 <coppro> which, clearly you can do by generating modules from functors
07:50:22 <coppro> java's genetics consist of a whole bunch of un-evolution
07:50:36 <coppro> yeah, I just wanted to make sure you'd have a mechanism for that
07:50:51 <coppro> (and actually, C++ templates is closer than Java generics, but w/e)
07:52:59 <ehirdiphone> I have been talking about this Lang for so long. Wow.
07:54:32 <ehirdiphone> coppro: I'd give you an awesome explanation of one of the things the Lang will use but I've only really thought it out verbally :(
07:57:08 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:07:30 -!- ehirdiphone has joined.
08:08:04 <coppro> I did have one thing to say to you, but I forgot
08:08:39 <ehirdiphone> coppro: I recorded a ~four minute explanation of the thing but it'd be in multiple parts
08:08:55 <ehirdiphone> Can you handle my unbroken voice????????//::
08:09:56 <coppro> as opposed to hemming-and-hawing?
08:10:09 -!- ehirdiphone has quit (Client Quit).
08:13:11 -!- ehirdiphone has joined.
08:13:43 <ehirdiphone> Wait for all three parts to arrive then set them up in a playlist or sth
08:17:03 <ehirdiphone> My speaking skills are improving, not many ums or pauses in that
08:18:48 <coppro> unless you're trying to sell me replica rolexes, no
08:21:06 <coppro> thanks for spamming some random guy
08:21:17 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
08:22:00 <coppro> ais523: go to messages, hit propose or accept trade, fill in the form
08:22:51 <ais523> thanks, got it, and that's a /really/ weird channel-bounce
08:22:55 <ais523> cross-server, even cross-protocol
08:23:18 <coppro> too lazy to type /msg ais523 on a chat without tab-complete
08:23:40 -!- ehirdiphone has joined.
08:24:20 <ais523> coppro: heh, I was just thinking that myself
08:24:54 <augur> http://www.wolframalpha.com/input/?i=tea%2C+earl+gray%2C+hot
08:25:18 <coppro> ehirdiphone: I was giving him advice for KoL
08:26:01 <coppro> that's sorta the point
08:26:24 <ais523> augur: a rather low-tech MMO
08:27:18 <coppro> mostly I play it for the fun in /games, to be honest
08:27:20 <ais523> it's a moderate amount of strategy + a lot of boredom
08:27:25 <coppro> (though it probably won't appeal to most everyone here)
08:27:52 <coppro> but it's a nice distraction
08:32:03 -!- coppro has quit (Remote closed the connection).
08:32:51 <ehirdiphone> incidentally, I realised that ais523 hates collectively-covering-costs cooperatives. Let's say membership dues = cost/members. This way, everyone pays the same money, and nobody gets rich. By recommending the service to someone who then joins it, the recommender pays cost/(members (members+1)) less each $interval, where members is the number of members before the new member is recruited
08:33:18 <ehirdiphone> so this fair, collectivist cooperative is considered to be evil by ais523 :)
08:33:22 <ais523> ehirdiphone: it's not quite hate, it's more untrust
08:34:01 <ais523> if someone recommends something to me and stands to gain from that, I treat it as a paid advert, rather than as freely-given advice
08:34:07 <ais523> doesn't mean it's unwelcome or bad, just untrustworthy
08:34:07 <ehirdiphone> ais523: So do you not distrust if nobody makes a profit?
08:34:47 <ais523> yes... but suppose you have two identical cooperatives
08:34:51 <ais523> except that you're in one of them
08:35:03 <ais523> the question here, I suppose, is why should I join the one with you in rather than the other one?
08:35:11 <ais523> now, suppose the other one has one more member but is otherwise identical
08:36:02 <ehirdiphone> So you distrust profitless, collectivist cooperatives.
08:36:24 <ehirdiphone> Favouring instead recommendations that involve a business making a handy profit.
08:36:31 <ais523> I distrust recruitment drives that would drive me towards one of them rather than a different one of them
08:36:55 <ehirdiphone> ais523: But that's how they WORK! evryone pays an equal amount
08:37:07 <ais523> ehirdiphone: I don't hate the collective itself
08:37:17 <ais523> I just mistrust /recommendations of which collective to join/
08:37:24 <ais523> from a member of the collective itself
08:37:36 <ais523> I might still favour the entire concept over a for-profit company
08:38:27 <ehirdiphone> If soneone thought another service was superior they wouldn't reccommend theirs just for profit. They'd SWITCH to that alternative THRN reccommend them
08:38:41 <ehirdiphone> Doing otherwise is ridiculously nonsensical
08:42:03 <ehirdiphone> Wonder if anyone's registered http://chicken.coop yet :D
08:45:16 <ehirdiphone> ais523: Do you want my lovely voice explanations of frp, coppro iz ded :<
08:45:46 <ehirdiphone> THEY EXPLAIN IT WITH THE GRACE OF AN OSTRICH
08:45:55 <ais523> ehirdiphone: oh, that's a good argument, about switching
08:46:12 <ais523> for something that's really switchable, I'll consider that to rebut my points
08:46:25 <ais523> also, no, that's me asking you to explain frp before I decide whether I should ask you to explain it or not
08:46:53 <ais523> it's an upside-down T?
08:47:00 <ehirdiphone> That's bottom, your friendly nonterminating value!
08:47:17 <augur> ehirdiphone: http://www.wolframalpha.com/input/?i=Mudkipz
08:47:38 <augur> bottom can also mean nil or false, depending on the language in question.
08:48:02 <ais523> it's the return value of a function with an infinite loop in
08:48:22 <augur> ehirdiphone: in logic its not uncommon to find bottom for false
08:48:43 <ais523> it's kind-of a different sort of return value...
08:48:51 <ais523> what about throwing an exception past the caller to a handler outside?
08:50:36 <ais523> ok, so this explains bottom, which almost certainly has its own unicode char
08:51:18 <ais523> actually used for the geometric meaning, "perpendicular to"
08:51:23 <augur> http://en.wikipedia.org/wiki/Bottom_type
08:51:54 <augur> also http://en.wikipedia.org/wiki/Bottom_element
08:52:50 <augur> says common lisp's nil is a bottom.
08:52:58 <augur> which im not sure i buy, but whatever
08:53:29 <ehirdiphone> You're a bottom. Er, I think this conversation just strayed into territory I don't want it to stray into.
08:53:57 <augur> it seems like Bottom can be non-termination, but it can be other things as well
08:54:23 <augur> and other things that might be conceived as non-termination in some abstract sense
08:54:28 <augur> e.g. not returning a value at all
08:54:30 <ais523> ehirdiphone: err, I don't see why audio's relevant
08:55:21 <augur> ehirdiphone: i love you!
08:55:26 <augur> in that special way
08:55:27 <ehirdiphone> I'm not transcribing 4 minutes of speech :D
08:55:50 <ais523> ugh, filebin.ca is still malware-blocked
08:56:00 <ais523> I could just get around the block, but it feels wrong to do that somehow
08:56:01 <augur> that would be wrong
09:00:59 <augur> your voice is girly
09:01:12 <augur> so i imagine people into girls like your voice
09:03:48 <augur> youre still adorable
09:10:32 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
09:11:06 -!- ehirdiphone has joined.
09:14:38 -!- mycroftiv has quit (Read error: 104 (Connection reset by peer)).
09:15:56 <ehirdiphone> I was enjoying talking about that language
09:19:08 <ehirdiphone> 4 hours 12 minutes. I talked about it continuously for about that long. Wow.
09:19:26 <augur> which language is that
09:20:21 <augur> can you summarize it please
09:21:29 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
09:28:12 -!- mycroftiv has joined.
09:58:54 -!- FireFly has joined.
10:30:30 -!- ehirdiphone has joined.
10:31:37 <ehirdiphone> the sort of thing ais523 would think of if he just generated ideas without honing on interesting things, I think
10:32:02 <ais523> actually, I do do that, just most of the boring stuff gets discarded straight off
10:32:06 <ais523> and I never tell anyone then forget
10:32:30 <ehirdiphone> An Emacs X11 WM that actually makes the windows into Emacs buffers.
10:32:54 <ehirdiphone> (the xemacs wm thing is just a wm written in elisp. Lame.)
10:33:00 -!- adam_d has joined.
10:33:50 <ais523> ehirdiphone: heh, Blender works a bit like that
10:33:55 <ais523> at least, it seems to have stolen the Emacs WM
10:38:13 <ais523> although, what would the modes be
10:39:22 <ehirdiphone> with the oblig menus with actions and settings
10:40:25 <ais523> C-x 5 2, rather than C-x 2
10:40:33 <ais523> to create a floating rather than docked window
10:40:56 <ehirdiphone> that would just open an emacs frame in an emacs buffer :D
10:41:53 <ais523> your applications are buffers
10:41:59 <ais523> you can swap them in and out of windows at will
10:42:18 <ais523> ehirdiphone: you mis-emacs
10:42:34 <ehirdiphone> X11 windows would be drawn in their own BONAFIDE emacs buffer
10:43:02 <ais523> that's what I meant too
10:43:14 <ehirdiphone> Root window = emacs, no window management done on it PFC
10:43:23 <ais523> one window produced by an application under a normal WM = one Emacs buffer
10:44:13 <ehirdiphone> but there shall be only One emacs window; for lo, that is what the Prophet did spaketh unto ya
10:44:54 <ais523> C-x 2 is two emacs windows already
10:45:01 <ais523> you need emacs windows to put the buffers in
10:45:04 <ehirdiphone> "If Emacs be the heritor of thou'st windows, is it not therefore a Sin to have Emacs begat itself?"
10:45:17 <ais523> /every/ window is an Emacs window
10:45:28 <ehirdiphone> There shall be only one Emacs window, and it shall be the root.
10:45:40 <ais523> I was talking about emacs window
10:45:48 <ais523> how would you do extra emacs frames, though?
10:46:08 <ais523> but that's losing possibilities you have with emacs's wm at the moment
10:46:19 <ais523> the ability to create a floating frame that works independently of the others
10:46:26 <ais523> it's tiling and floating
10:46:36 <ais523> hmm... I wonder if C-x 5 o works?
10:47:18 <ais523> hmm... this is a tricky one
10:48:15 <ehirdiphone> It should be recognised as a heresy unique to the Xfolk; lacking as the result is in Emacs mannerisms,
10:49:46 <ehirdiphone> in the model here emacs frames "don't exist"
10:50:18 <ehirdiphone> Frames become an implementation detail; only one, as the root window.
10:50:40 <ais523> hmm, but a floating-mode window makes absolutely no sense in that case
10:50:47 <ais523> from Emacs' point of view
10:50:59 <ais523> you couldn't select it, you couldn't close it, you couldn't create it
10:51:05 <ehirdiphone> it is "in" emacs because emacs' size is that of the screen
10:51:23 <ais523> but it's in a different frame
10:51:25 <ehirdiphone> also, if you focus it the invisible corresponding buffer is too
10:51:38 <ais523> thus it isn't there at all
10:51:52 <ehirdiphone> Windows are Emacs' forte. Frames it thinks of not.
10:51:53 <ais523> it isn't in the root frame because you can't get to it by recursively picking top, left, etc... windows
10:52:12 <ais523> e.g. it would make no sense for C-x o to /cycle/ to it
10:52:20 <ais523> and if it did, what would C-x 2 do? or worse, C-x 1?
10:52:34 <ehirdiphone> ais523: Its like a buffer not in the frame
10:52:51 <ais523> ehirdiphone: oh, in that case, it wouldn't render at all
10:53:01 <ais523> so you'd have no way of focusing on it
10:53:10 <ehirdiphone> ais523: Yes it would because we coded it that way
10:55:50 -!- oerjan has joined.
11:08:30 <ehirdiphone> 4 hrs 12 mins continous talk about my language
11:08:32 <oerjan> just searched for my name today
11:09:18 <ehirdiphone> Your emacs buffer list would be polluted. Cool for window managing
11:09:20 <ais523> what? I'm about to go home to sleep
11:09:22 <oerjan> alas, i usually only read the whole log when it is short
11:09:39 <ais523> ehirdiphone: really? I often have over 30 or so buffers open
11:09:45 <ais523> I rarely kill them, you see
11:09:55 <ais523> and don't use the buffer list at all, except by mistake
11:10:23 <ais523> with asterisks around it if it's not meant to be saved
11:10:34 <ais523> yes, you should be able to save buffers even if they contain windows
11:11:04 <ais523> otherwise the semantics are wrong
11:11:12 <ais523> you could hook it up to cryopid or something, I suppose
11:11:15 <oerjan> i did see the comment about it being more CS than haskell. which actually leaves me suspicious if you are over your head, since my understanding is that creating a sound type system more advanced than haskell's (or even equal) is _hard_
11:11:17 <ehirdiphone> **reddit - what's new online! - Mozilla Firefox**
11:11:26 <ais523> or ideally, just have the programs that run be easy to escape
11:11:39 <ais523> ehirdiphone: Firefox is a big example of something that should save
11:11:40 <ehirdiphone> oerjan: I know it is possible. Agda and Ur do it.
11:11:56 <ehirdiphone> ais523: You can't coherently save tetris f.e.
11:11:56 <ais523> after all, it has a save-tabs-on-closing option, this would be the same thing
11:11:59 -!- FireFly has quit (Read error: 60 (Operation timed out)).
11:12:08 <oerjan> ehirdiphone: yeah, but i'm assuming there were phd theses involved :D
11:12:09 <ais523> ehirdiphone: really? I've seen pieces of hardware that could
11:12:22 <mycroftiv> cant you just make sure that you are within the formal boundaries established by hindley-milner typing?
11:12:31 <ais523> anyway, I really had better go
11:12:35 -!- ais523 has quit (Remote closed the connection).
11:12:37 <oerjan> of course, more power to you if you can pull it off
11:12:40 -!- FireFly has joined.
11:13:04 <mycroftiv> i havent read the immensely huge backscroll so i wont make you explain it all again if you already have
11:13:48 <mycroftiv> actually i guess i lost most of my backscroll from my mouse button forkbombing me
11:14:00 <ehirdiphone> oerjan: maybe I'll just submit the spec and compiler as a phd thesis to MIT or somewhere without being admitted :D
11:15:57 <oerjan> ehirdiphone: it is the soundness proof of your type system i am worried about. not that i know how to do those myself
11:16:43 <oerjan> unless you simply steal an already existing one, you'll have to redo it, and i understand it's quite technical stuff
11:16:45 <ehirdiphone> oerjan: If type checking can bottom out surely it's unsound by some definition
11:17:14 <oerjan> i mean in the cannot-go-wrong sense, i think
11:18:15 <soupdragon> oerjan the fun with dependent types is you need to interleave the value normalization proof
11:18:44 <ehirdiphone> maybe I'll contract a phd out to do the proof :)
11:19:16 <oerjan> ehirdiphone: what soupdragon said. non-termination is fine, except i also recall reading that dependent typing has trouble if your _types_ can bottom out, because then you need to actually evaluate the proofs in the runtime program, you cannot remove that stuff during compilation
11:19:43 <oerjan> because if a proof of well-typed-ness can bottom out, then it is invalid
11:19:56 <oerjan> um proofs of types, i guess
11:20:14 <oerjan> that is not dependent.
11:20:47 <ehirdiphone> oerjan: I was thinking of using a total subset
11:22:53 <ehirdiphone> tbh I think my type system is likely incredibly similar to say agda
11:23:52 <oerjan> i recall some mention of using a monad to encapsulate non-termination
11:24:20 <soupdragon> codata Computation A where Now : A -> Computation A ; Later : Computation A -> Computation A
11:24:36 <oerjan> then it would presumably be fine, since types are not in that monad, or something
11:24:45 <soupdragon> then you can race omega many of these for a fixed point
11:26:09 <oerjan> um shouldn't the _result_ be an A for some option?
11:26:33 -!- anmaster_l has joined.
11:27:20 <ehirdiphone> Hmm my type system is probably closest to epigram
11:27:37 <ehirdiphone> programming more than proofy and haskellsimilar as it is
11:27:40 <oerjan> it was for epigram i heard that mention, i think
11:28:12 <oerjan> except it was not something implemented, iirc
11:28:26 -!- MigoMipo has joined.
11:28:32 <soupdragon> I used it in haskell to write (even more) lazy programs
11:28:33 <ehirdiphone> It just makes code awkward having a partiality monad :p
11:28:35 <oerjan> just an idea for making epigram practically TC
11:28:57 <ehirdiphone> at some point I surrender safety for practicality
11:29:28 <soupdragon> yeah I have no idea how to do even simple proofs about termination for the partiality monad
11:30:22 <oerjan> ehirdiphone: i thought epigram was a total language
11:31:20 <soupdragon> I think it's a weird question, the function space is total but you can still define things like turing machines, mu-recursive functions and their operational behavior
11:31:25 * oerjan may very well be confused, has only read discussions (on ltu mostly?) and that was long ago
11:31:51 <oerjan> well one step of a turing machine computation is total...
11:32:14 <soupdragon> yeah you can take the transitive closure of it though
11:33:16 <ehirdiphone> anyway ur works and only has one phd behind it
11:33:53 <soupdragon> Ur isn't actually dependently typed is it
11:40:45 <ehirdiphone> soupdragon: it does have type-level programming that constructs values. I'd be surprised if it wasn't dependent
11:41:33 <soupdragon> soem error to do with gmp or something
11:47:40 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
11:49:23 -!- Pthing has quit (Remote closed the connection).
12:21:15 -!- oerjan has quit ("leaving").
12:23:44 -!- cheater has joined.
12:24:25 <cheater> has anyone got a working implementation of Piet or a similar lang?
13:44:12 -!- MizardX has joined.
13:45:06 -!- adam_d_ has joined.
13:53:31 -!- adam_d has quit (Read error: 60 (Operation timed out)).
13:53:53 -!- MizardX has quit ("...").
14:09:05 -!- Sgeo has joined.
14:09:41 <Sgeo> Hm, ehird's not here?
14:10:18 <Sgeo> ehird, if you see this, know that the penultimate story of Fine Structure has been published.
14:10:23 -!- adam_d_ has quit (Read error: 110 (Connection timed out)).
14:35:28 -!- soupdragon has quit ("Leaving").
14:53:07 -!- MigoMipo has quit ("When two people dream the same dream, it ceases to be an illusion. KVIrc 3.4.2 Shiny http://www.kvirc.net").
14:55:59 -!- BeholdMyGlory has joined.
14:59:04 -!- Asztal has joined.
15:07:20 -!- bsmntbombdood has quit (Read error: 110 (Connection timed out)).
16:50:59 -!- Slereah has joined.
17:00:59 -!- Slereah_ has quit (Read error: 110 (Connection timed out)).
17:19:22 -!- BeholdMyGlory has quit (Read error: 104 (Connection reset by peer)).
17:21:07 -!- adam_d has joined.
17:23:51 -!- BeholdMyGlory has joined.
18:14:36 -!- adam_d_ has joined.
18:29:20 -!- adam_d has quit (Read error: 110 (Connection timed out)).
19:21:13 -!- MizardX has joined.
19:32:20 -!- jpc has joined.
20:03:18 -!- BeholdMyGlory has quit (Remote closed the connection).
20:10:41 -!- BeholdMyGlory has joined.
20:16:33 -!- oerjan has joined.
20:19:19 <oerjan> <cheater> has anyone got a working implementation of Piet or a similar lang?
20:19:36 <oerjan> have you checked the author's home page at http://www.dangermouse.net/esoteric/piet/tools.html ?
20:34:30 -!- brado has joined.
20:34:55 -!- brado has left (?).
21:55:55 -!- coppro has joined.
21:56:25 -!- Gracenotes has quit ("Leaving").
21:58:50 -!- calamari has joined.
22:21:24 -!- Fredrik1994 has joined.
22:21:29 -!- Fredrik1994 has left (?).
22:44:10 -!- MAKACOW has joined.
22:49:42 -!- MAKACOW has left (?).
23:15:08 -!- Gracenotes has joined.
23:18:46 -!- soupdragon has joined.
23:34:42 -!- soupdragon has quit (Read error: 60 (Operation timed out)).
23:50:22 -!- calamari has quit ("Leaving").
23:59:14 <coppro> http://dangermouse.net/esoteric/