←2009-12-29 2009-12-30 2009-12-31→ ↑2009 ↑all
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:29 <ehirdiphone> So good to hear about Mike.
00:35:56 -!- MigoMipo has joined.
00:36:31 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
00:37:02 <soupdragon> ?
00:56:23 -!- ehirdiphone has joined.
00:56:46 <ehirdiphone> soupdragon: See todays logs.
00:56:51 -!- ehirdiphone has quit (Client Quit).
01:00:08 <soupdragon> hm
01:07:25 <ais523> definitely
01:08:23 <soupdragon> definitely good or definitely hm?
01:14:30 <ais523> definitely good
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:37 <soupdragon> I do
03:30:57 <ehirdiphone> but I already told you the basics yesterday :P
03:31:10 <ehirdiphone> Elaboration is so passé
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:33:18 <soupdragon> is your friend bipolar
03:33:32 <ehirdiphone> what friend
03:33:47 <ehirdiphone> You mean mike Riley?
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:15 <soupdragon> yeh
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:35 <ehirdiphone> ais523: Sleep pattern messed up again?
03:37:46 <ais523> sort-of
03:37:55 <ais523> also, I sometimes have late Internet nights deliberately, so I can talk to americans
03:38:00 <ehirdiphone> (also, nethack.de?)
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:15 <ehirdiphone> ais523: heh. Mine's messed up too
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:33 <ehirdiphone> ask me about my language!
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:39:39 <ehirdiphone> Yep
03:39:51 <ais523> how might it do I/O?
03:40:01 <ehirdiphone> Even agda is more cs
03:40:10 <ehirdiphone> But not so good for regular programming
03:40:17 <coppro> rofl Talking to Americans
03:40:28 <ais523> coppro: why is that amusing?
03:40:37 <ehirdiphone> ais523: Basic text io... Prolly monads.
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:05 <ehirdiphone> ais523: Tru day
03:42:07 <ehirdiphone> Fat
03:42:09 <ehirdiphone> Dat
03:42:21 <ais523> ***dat?
03:42:26 <ehirdiphone> Yes
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:12 <ehirdiphone> ASK ABOUT ANY :P
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:45:03 <ehirdiphone> Say, the names of the fields of a record
03:45:07 <ehirdiphone> And their types
03:45:08 <ehirdiphone> Etc
03:45:19 <ehirdiphone> NEXT QUESTIONS :p
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:22 <ehirdiphone> Ok
03:46:49 <ehirdiphone> In typed lambda calculus, types index on types and values index on values
03:46:52 <ehirdiphone> That is
03:47:03 <ehirdiphone> A type can depend on another type
03:47:08 <ehirdiphone> Like
03:47:13 <ehirdiphone> (a,b)
03:47:23 <ehirdiphone> Indexes on a and n
03:47:24 <ehirdiphone> B
03:47:27 <ehirdiphone> Types
03:47:38 <ehirdiphone> And values index on values
03:47:41 <ehirdiphone> F x
03:47:42 <soupdragon> I didn't get that ehird
03:47:47 <ehirdiphone> F indexes on x
03:47:55 <ehirdiphone> ais523: Get that so far?
03:48:04 <soupdragon> inspecting types
03:48:06 <ehirdiphone> You give types to types
03:48:10 <ais523> basically, creating types out of other types
03:48:14 <ehirdiphone> And values to values
03:48:25 <ehirdiphone> ais523: Thats nit dependent Tuesday
03:48:28 <ehirdiphone> Types
03:48:34 <ehirdiphone> This I'd just bacgriund
03:48:37 <ais523> ok
03:48:54 <ehirdiphone> ais523: now in haskell
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:49:37 <ehirdiphone> Int -> String
03:49:50 <ehirdiphone> String -> String
03:50:02 <ehirdiphone> the value of "show" changes
03:50:09 <ehirdiphone> Get it?
03:50:19 <ais523> yep
03:50:29 <ehirdiphone> Now for the kicker
03:50:31 <ais523> like overloaded functions, but much more first-class and genreal
03:50:33 <ais523> *general
03:50:49 <ehirdiphone> ais523: Dependent types = types indexing on values
03:50:53 <ehirdiphone> FOR INSTANCE
03:51:00 <soupdragon> no
03:51:01 <ais523> oh, aha, I did know that, just forgotten I had
03:51:15 <soupdragon> indexing is just one sort
03:51:25 <ehirdiphone> soupdragon: Im just explaining it
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:31 <ehirdiphone> Not formally defining it
03:51:35 <ehirdiphone> ais523: Yep
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:01 <ehirdiphone> At compile time
03:52:06 <ehirdiphone> No runtime penalty
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:53:25 <ehirdiphone> Safe
03:53:29 <ais523> yes, definitely
03:53:31 <ehirdiphone> And
03:53:40 <ehirdiphone> Lets us do things we couldn't otherwise
03:53:46 <ehirdiphone> More permissive things!
03:54:03 <ais523> ehirdiphone: incidentally, this is how I think a really good BF optimiser would work
03:54:05 <ehirdiphone> For instance
03:54:14 <ais523> trying to calculate dependent types for tape elements at different points in a program
03:54:33 <ehirdiphone> vararg :: (n :: Integer) -> Vararg n
03:54:36 <ehirdiphone> And
03:55:12 <ehirdiphone> type Vararg 0 = (); Vararg n = () -> Vararg (n-1)
03:55:24 <ehirdiphone> vararg 0 :: ()
03:55:34 <ehirdiphone> vararg 1 :: () -> ()
03:55:37 <ehirdiphone> etc
03:55:47 <ehirdiphone> Ignoring negatives :P
03:56:02 <ais523> curried varargs!
03:56:06 <ehirdiphone> Implementation if vararg itself:
03:56:16 <ehirdiphone> vararg 0 = ()
03:56:28 <ais523> actually, I think that's possible in Underload too, but a completely different way
03:56:35 <ehirdiphone> vararg n () = vararg (n-1)
03:57:03 <ehirdiphone> ais523: And this doesn't inspect n at runtime to determine the type!
03:57:13 <ais523> yep
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:57:41 <ehirdiphone> So it knows your call is correct
03:57:44 <ehirdiphone> ais523: PLUS
03:57:53 <ehirdiphone> All if this leads to more fun
03:57:58 <ehirdiphone> Type safe printf
03:58:19 -!- Slereah has quit (Read error: 110 (Connection timed out)).
03:58:20 <ehirdiphone> printf :: (fmt :: String) -> Printf fmt
03:58:39 <ehirdiphone> type Printf [] = IO ()
03:58:43 <ais523> ehirdiphone: you probably want something along the line of C++'s dynamic_cast
03:58:50 <ehirdiphone> No
03:58:52 <ehirdiphone> Static
03:58:54 <ehirdiphone> Ssh
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:36 <soupdragon> haha cool
03:59:55 * coppro will point out that C++ has lots of static correctness... too much, really
04:00:05 <ehirdiphone> type Printf (x:xs) = Printf xs
04:00:16 <soupdragon> yeah my C++ programs are statically correct.. the problems come when you run them
04:00:19 <ehirdiphone> ais523: ^^^ dependent types rule
04:00:53 <ais523> soupdragon: haha
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:07 <ehirdiphone> soupdragon: Lol
04:01:08 <ehirdiphone> Ok
04:01:14 <ais523> unless you go and implement integers in the type system, or whatever
04:01:14 <ehirdiphone> First amd last gone
04:01:19 <ehirdiphone> Pick one!
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:15 <ehirdiphone> PICK ONE >:( :P
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:27 <ehirdiphone> soupdragon: Reask
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:02:57 <ehirdiphone> soupdragon: You have:
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:12 <soupdragon> or do they?
04:03:30 <ehirdiphone> data Foo = Foo { a :: Integer, b :: Integer }
04:03:47 <ehirdiphone> With dependent types alone, you could not do
04:03:52 <ehirdiphone> f Foo
04:03:54 <ehirdiphone> ==
04:03:56 <coppro> s/WTFBBQ/OMGWTF/
04:04:03 <coppro> http://thedailywtf.com/Articles/OMGWTF-Finalist-10-FerronCalc.aspx
04:04:10 <ehirdiphone> [("a",Integer),
04:04:24 <ehirdiphone> ("b",Integer)]
04:04:31 <ehirdiphone> (f being type level)
04:04:41 <soupdragon> wnat about
04:04:52 <soupdragon> f (A -> B) = "A -> B"
04:04:55 <soupdragon> ?
04:04:57 <ehirdiphone> So basically inspecting and creating types programmaticslly in the type system
04:05:05 <ehirdiphone> Is what I mean
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:07:49 <ehirdiphone> It is type level
04:08:07 <ehirdiphone> Where of course types are values, duh
04:08:32 <ehirdiphone> Foo :: Type or :: Set if you fancy
04:08:36 <soupdragon> well I still don't get it
04:08:47 <soupdragon> but that's okay
04:08:54 <ehirdiphone> I would write example code but not on the iph
04:08:56 <ehirdiphone> Ooh
04:09:13 <ehirdiphone> I'll pen write it and photo it >:D
04:09:58 <soupdragon> haha now you're thinking with iPhones
04:10:35 <ehirdiphone> Paper. Where is paper
04:10:54 <ehirdiphone> I HAVE NO PAPER
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:06 <ehirdiphone> Fuck books with no notes section
04:12:12 * coppro managed to get a computer for his English exam!
04:12:23 <ehirdiphone> I need a bible with a lot of blank pages
04:12:48 <ehirdiphone> PAPER
04:12:57 <ais523> soupdragon: both
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:45 <ehirdiphone> AAAAAAA PEN
04:13:49 <ehirdiphone> Need pen
04:13:50 * coppro is currently using a cookie tray
04:14:14 <ehirdiphone> Ok
04:14:51 <ais523> coppro: I didn't realise cookie trays were even approximately TC
04:14:51 <ehirdiphone> WTF pen is silver
04:14:58 <ais523> ehirdiphone: ask your parents?
04:15:04 <coppro> ais523: for laptop ventilation
04:15:09 <ais523> coppro: ah
04:15:31 <ehirdiphone> ais523: Its 4am
04:15:39 <ais523> good point
04:15:41 <ehirdiphone> I'm not waking them up :P
04:15:51 <ais523> maybe you should just wait until morning
04:15:55 <ehirdiphone> WAIT
04:16:01 <ehirdiphone> We have drawers here
04:16:07 <ehirdiphone> With things in them
04:16:13 <ehirdiphone> SEARCH TIME
04:17:25 <soupdragon> cookie trays???
04:17:33 <ehirdiphone> YEA
04:17:38 <ehirdiphone> PEN
04:22:07 <ehirdiphone> Photo time
04:22:10 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
04:24:13 -!- ehirdiphone has joined.
04:24:21 <ehirdiphone> ais523: I emailed you the photo
04:24:28 <ais523> heh
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:24:44 <ehirdiphone> Thx
04:26:13 <ais523> http://imgur.com/n5amE.jpg
04:26:32 <ehirdiphone> soupdragon:
04:26:37 <ehirdiphone> So here,
04:26:42 <ais523> what did you write it /on/? I hope you haven't damaged a book for our sake
04:27:05 <ehirdiphone> type Fields :: Type -> [(String,Type)]
04:27:07 <ehirdiphone> well
04:27:17 <ehirdiphone> Technically :: Record ->
04:27:26 <ehirdiphone> But that's not too relevant
04:27:27 <soupdragon> okay
04:27:37 <ehirdiphone> ais523: Blank page before index
04:27:46 <ais523> ugh
04:27:46 <ehirdiphone> In ruby on rails book - worthless
04:27:56 <ais523> ehirdiphone: you might have been able to sell on that book...
04:27:56 <ehirdiphone> soupdragon: See what I mean now?
04:28:03 <soupdragon> yes
04:28:12 <Gracenotes> D:
04:28:23 <ehirdiphone> ais523: Oh well
04:28:30 <ehirdiphone> It's for SCIENCE
04:28:33 <soupdragon> hi Gracegoats
04:29:20 <ehirdiphone> ais523: The book is way out of date anyway
04:29:27 <Gracenotes> oh hello soupdragon. wink.
04:29:36 -!- adam_d has quit (Read error: 110 (Connection timed out)).
04:29:45 <soupdragon> ?
04:29:48 <ehirdiphone> Gracenotes: Get a room!
04:29:58 <Gracenotes> wat
04:30:04 <Gracenotes> ehirdiphone: get a real computer :|
04:30:05 <soupdragon> xwat360
04:30:07 <soupdragon> lol
04:30:16 <ehirdiphone> Gracenotes: Get your mo
04:30:19 <soupdragon> iPhone isn't even turing complete!!!!
04:30:19 <ehirdiphone> M
04:30:39 <ehirdiphone> Real men use real turing machines!
04:30:41 <Gracenotes> that's true. then again this laptop isn't exactly turing-complete
04:30:50 <soupdragon> lol
04:30:51 <soupdragon> @
04:30:56 <soupdragon> turing machines
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:15 <soupdragon> it's basically a big lookup table
04:32:19 <ehirdiphone> ais523: grok the example?
04:32:27 <ais523> yes
04:32:27 <soupdragon> so called "computers" don't compute anything
04:32:32 <ais523> it looks just like OCaml
04:32:37 <ehirdiphone> Wat
04:32:52 <ehirdiphone> It's haskell but with dependent types and type metaprogramming
04:32:59 <ehirdiphone> Haskell syntax thru and through
04:33:05 <Gracenotes> what is? Epigram?
04:33:07 <ais523> well, they're pretty similar syntactically
04:33:18 <ehirdiphone> The syntax i used in my example
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:33:47 <Gracenotes> use the C #include system
04:33:49 <Gracenotes> end of story
04:33:50 <ehirdiphone> pikhq: Few differences.
04:33:51 <Gracenotes> amirite
04:34:06 <ehirdiphone> pikhq: Actual syntax will differ quite a bit
04:34:35 <soupdragon> no one cares about module systems :P
04:34:39 <pikhq> Gracenotes: MURDER.
04:34:40 <soupdragon> because they are complicated
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:32 <ehirdiphone> pikhq: Yeah like haskell
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 <ehirdiphone> pikhq: Haskell has nanespaces
04:36:12 <pikhq> We may be using words differently. Explain.
04:36:19 <ehirdiphone> And no functors!
04:36:32 <ehirdiphone> (not that kind)
04:36:41 <pikhq> Ah.
04:36:41 <pikhq> I consider that a somewhat simplistic module system.
04:36:53 <ehirdiphone> Shall I segue into my explanation? :P
04:36:55 <pikhq> Of course, my background is C-heavy, so... Yeah.
04:36:59 <pikhq> Yes.
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:39:56 <ehirdiphone> Erm
04:40:00 <ehirdiphone> That type there
04:40:07 <ehirdiphone> Oh sod it let me retire
04:40:10 <ehirdiphone> Rewrite
04:40:11 <ehirdiphone> Sec
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:41:15 <ehirdiphone> With me so far?
04:41:20 <pikhq> Right...
04:41:23 <ehirdiphone> (ais523 pikhq)
04:41:43 <ais523> yep
04:41:45 <ais523> same as in ML
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:43:42 <ehirdiphone> With me?
04:43:50 <pikhq> Okay...
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:45:12 <ehirdiphone> Then it becomes it's interface
04:45:16 <ehirdiphone> I.e
04:45:28 <ehirdiphone> pikhq: List.T is a type site
04:45:31 <ehirdiphone> Sure
04:45:32 <ehirdiphone> But
04:45:48 <ehirdiphone> It is not useable as [Integer]
04:45:56 <ehirdiphone> It is abstractef
04:46:09 <ehirdiphone> We can only use it from List's functions.
04:46:14 <ehirdiphone> Cool, no?
04:46:25 <pikhq> Yeah.
04:46:34 <ehirdiphone> [1] :: List.T simply doesn't work
04:46:50 <ehirdiphone> Because the implementation of T is not exposed
04:46:53 <ehirdiphone> pikhq: Now
04:47:12 <ehirdiphone> It's conceivable that two modules might have the same signature
04:47:17 <ehirdiphone> E.g.
04:47:30 <ehirdiphone> An implementation using a vector
04:47:36 <ehirdiphone> Yah?
04:47:42 <pikhq> Yeah.
04:48:15 <ehirdiphone> So we have functors. A functor is basically a module that takes other modules as arguments
04:48:18 <ehirdiphone> Observe
04:49:06 <ehirdiphone> functor Silly (List :: signature { long signature is long }) = module {
04:49:26 <ehirdiphone> foo = List.add 1 List.empty
04:49:49 <ehirdiphone> main = print (List.length (List.add 2 foo))
04:49:52 <ehirdiphone> }
04:49:57 <ehirdiphone> We could then do
04:50:13 <ehirdiphone> open (Silly VectorList)
04:50:26 <ehirdiphone> (open is basically import)
04:50:37 <ehirdiphone> (extracts everything into the current module)
04:51:03 <pikhq> Huh.
04:51:06 <ehirdiphone> pikhq: So we have implementation agnostic modules
04:51:10 <ehirdiphone> Sweet, huh?
04:51:15 <pikhq> Yeah.
04:51:21 <ehirdiphone> AND
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:53:58 <Gracenotes> I feel like breaking down into tears
04:54:03 <coppro> Gracenotes: one of Eelis' finest creations
04:54:36 <ais523> hahaha
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:55:55 <pikhq> Spiffy.
04:55:58 <ehirdiphone> http://imgur.com/n5amE.jpg
04:56:06 <ehirdiphone> Seen it?
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:21 <ehirdiphone> Grok it?
04:56:26 <ehirdiphone> Gracenotes: Iphone
04:56:38 <ais523> Gracenotes: maybe not, but apostrophes in keyword names are still epic
04:57:42 <ehirdiphone> pikhq:
04:58:09 <pikhq> ehirdiphone: Yes.
04:58:13 <coppro> Don't is a syntax trick?
04:58:17 <ehirdiphone> Ok pen time
04:58:18 <pikhq> I just commented on it, in fact.
04:58:24 <ehirdiphone> Ok :p
04:58:29 <ehirdiphone> Sec
04:59:57 <ehirdiphone> Too long to write I'll just explain
05:00:08 <ais523> coppro: yes
05:00:22 <ais523> it's equivalent to Don::t using an outdated syntax
05:00:31 <coppro> ah
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:00:38 <ehirdiphone> FOR INSTANCE
05:01:10 <ehirdiphone> functor Input (t :: RecordType)
05:01:15 <ehirdiphone> results in a
05:01:33 <ehirdiphone> signature { input :: IO t }
05:01:47 <ehirdiphone> By using Fields as seen in my photo
05:01:57 <ehirdiphone> It lets you do this:
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:02:39 <ehirdiphone> open (Input Foo)
05:02:47 <ehirdiphone> main = input
05:02:49 <ehirdiphone> Result?
05:02:57 <ehirdiphone> $ ./foo
05:03:06 <ehirdiphone> a= 2
05:03:11 <ehirdiphone> b= foo
05:03:15 <ehirdiphone> c= abc
05:03:28 <ehirdiphone> Invalid input.
05:03:35 <ehirdiphone> c= true
05:03:45 <ehirdiphone> And that results in
05:03:51 <coppro> it's 4 am, you're hard to folllow
05:03:56 <ehirdiphone> Foo {a=2,...etc
05:04:07 <ehirdiphone> pikhq: ais523 get it?
05:04:09 <pikhq> That's... Pretty spiffy.
05:04:27 <coppro> I think I get it, and it's neat
05:04:30 <coppro> but I'm not sure
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:15 <ehirdiphone> coppro: Haskell fu helps
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:39 <ehirdiphone> coppro: Btw, what do you mean by
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:05:58 <ehirdiphone> pikhq: Yep.
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:06:38 <ehirdiphone> coppro: Redundantly?
05:06:42 <ehirdiphone> Like how?
05:07:04 <ehirdiphone> coppro: Do you mean the
05:07:07 <ehirdiphone> signature
05:07:14 <ehirdiphone> List
05:07:14 <coppro> [20:54:48]<ehirdiphone>type Vararg 0 = (); Vararg n = () -> Vararg (n-1)
05:07:16 <ehirdiphone> Thing?
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:53 <coppro> ah, ok
05:07:58 <ehirdiphone> In my soon after printf example you could easily see the difference
05:08:02 <coppro> right
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:14 <coppro> :(
05:09:18 <ehirdiphone> ???
05:09:26 <pikhq> Type inference is kinda impossible to do in the general case...
05:09:27 <ehirdiphone> I think you are confused
05:09:32 <coppro> ehirdiphone: no
05:09:33 <pikhq> And even more so for TC types.
05:09:45 <ehirdiphone> pikhq: Haskell sans typeclasses is inferrable totally
05:09:56 <ehirdiphone> coppro: You are confused
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:30 <coppro> see the redundancy?
05:10:39 <coppro> (at least it's better than the current mess *shudder*)
05:10:40 <ehirdiphone> You didn't say c++
05:10:47 <coppro> I did
05:10:47 <soupdragon> ehird, GADTs?
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:02 <ehirdiphone> soupdragon: What about them?
05:11:03 <soupdragon> not sure if Tom solved it or not
05:11:11 <ehirdiphone> Oh
05:11:14 <soupdragon> type inference for functions that work on GADTs
05:11:16 <ehirdiphone> Haskell inferrence
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:11:55 <ehirdiphone> Wait
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:13 <ehirdiphone> Didn't see that
05:12:16 <ehirdiphone> Xarify
05:12:18 <ehirdiphone> Clarify
05:12:42 <coppro> ehirdiphone: I just gave an example; "t+u" is redundant
05:12:52 <ehirdiphone> Ah
05:13:06 <ehirdiphone> Don't get it but whatever
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:34 <ehirdiphone> Erm
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:28 <ehirdiphone> I didn't realise you'd said them
05:14:40 <ehirdiphone> I was just continuing what I said with a quip
05:14:49 <coppro> ok
05:14:55 <ehirdiphone> Anyway
05:14:59 <coppro> how about we restart altogether?
05:15:06 <ehirdiphone> Doesn't matter
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:38 <ehirdiphone> Region inferrence instead :D
05:15:43 <coppro> gc w? garbage collection with?
05:15:44 <ehirdiphone> Would be uber cool
05:15:48 <ehirdiphone> coppro: Yes
05:16:06 <coppro> interesting
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:21 <ehirdiphone> And probably speed things up
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:42 <ehirdiphone> Probably wouldn't catch all things though
05:17:44 <pikhq> ehirdiphone: If you can do it, then it would be quite nice.
05:17:45 <ehirdiphone> Dunno
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:19:29 <ehirdiphone> malloc :: (n::Int) -> MemBlock n
05:19:55 <ehirdiphone> (Ok, IO (Maybe (MemBlock n)))
05:20:15 <pikhq> Heheh.
05:20:58 <ehirdiphone> pikhq: the kicker?
05:21:06 <ehirdiphone> Even ptr arithmetic
05:22:01 <ehirdiphone> ptradd :: (n::Int) -> MemBlock m -> MemBlock {n-m}
05:22:07 <ehirdiphone> Or similar
05:22:12 <ehirdiphone> Ignoring negatives
05:22:49 <ehirdiphone> *m-n
05:23:22 <pikhq> :D
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:18 <ehirdiphone> woo dependent types
05:24:28 <ehirdiphone> *-> IO Int
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:25:49 <ehirdiphone> (which is web apps, oddly enough)
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:26:30 <ehirdiphone> Dude. Fast.
05:26:42 <soupdragon> :(
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:44 <ehirdiphone> N
05:27:46 <pikhq> Much less "checking to be sure this is safe", more with the "just transform it to the equivalent".
05:27:57 <ehirdiphone> Not like 10 and a branch
05:28:01 <ehirdiphone> As with tagged ints
05:28:04 <ehirdiphone> Well
05:28:07 <ehirdiphone> No branch
05:28:12 <ehirdiphone> Since stariv
05:28:15 <ehirdiphone> Sratic
05:28:17 <ehirdiphone> Static
05:28:19 <ehirdiphone> But still
05:28:28 <ehirdiphone> 1 vs 6 or so
05:28:37 <ehirdiphone> Nice speed up for number chrubchibg
05:28:45 <ehirdiphone> Crunching
05:29:14 <ehirdiphone> soupdragon: why thr dmilry?
05:29:16 <ehirdiphone> The
05:29:19 <ehirdiphone> Smiley
05:29:20 <ehirdiphone> Sj
05:29:22 <soupdragon> because =
05:29:30 <ehirdiphone> Shiws as sad in colloquy
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:33:29 <ehirdiphone> damn this language is sweet :|
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:15 <ehirdiphone> Or one of the MLs
05:35:16 <pikhq> It just makes language implementation... Feel right.
05:35:26 <ehirdiphone> They were designed for it after all :P
05:35:34 <pikhq> Fair point.
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:36:56 <ehirdiphone> Haskell is compelling too though
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:14 <ehirdiphone> Agda has a really advanced emacs mode
05:39:27 <ais523> will it allow impureness?
05:41:05 <pikhq> ais523: Monads.
05:41:29 <ais523> I mean, as well
05:41:31 <ais523> if it's being strict
05:44:44 <ehirdiphone> ais523: No.
05:45:17 <ehirdiphone> Well, maybe if you have "pragma unsafe" in your module and import Internals.
05:45:34 <ehirdiphone> Then you have Internals.coerce :: a -> b
05:45:36 <coppro> back
05:45:51 <ehirdiphone> But every module using yours must be pragma unsafe too
05:45:59 <ehirdiphone> So that's pointless, mostly
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:46:54 <coppro> I have scrollback
05:47:18 <ehirdiphone> coerce would actually be:
05:47:38 <pikhq> ehirdiphone: Yeah, if you have well-defined evaluation order, "pragma unsafe" is perfectly reasonable.
05:47:53 <ehirdiphone> (a::Type) -> (b::Type) -> a -> b
05:48:11 <ehirdiphone> But you use that as (coerce x)
05:48:32 <ehirdiphone> That's just how you do forall in dependently typed langs
05:48:48 <ehirdiphone> I'll probably have shorthand for that
05:49:22 <ehirdiphone> Uh oh, iPhone problem, brb
05:50:00 <ehirdiphone> Fixed
05:50:01 <ehirdiphone> Ping
05:50:18 <pikhq> Pong
05:50:24 <coppro> Paddle
05:50:29 <ehirdiphone> Yay
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:02 <ehirdiphone> ais523: That would be my goal. :P
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:18 <ehirdiphone> coppro: Which part is very interesting?
05:52:25 <ehirdiphone> All of it? :P
05:52:28 <coppro> ehirdiphone: region inference
05:52:49 <ehirdiphone> ais523: No, but you can have a compile time BF compiler.
05:52:53 <ehirdiphone> With syntax.
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:13 <ehirdiphone> BF[ ,[.,] ] :: IO ()
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:14 <coppro> ok
05:54:19 * coppro loads logs
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:56:34 <ehirdiphone> coppro: No!
05:56:40 <coppro> oh :(
05:56:45 <ehirdiphone> Because there,
05:56:54 <ehirdiphone> The value must be known at compile time
05:57:02 <ehirdiphone> Not so with dependent types
05:57:15 <ehirdiphone> And yet, no runtime penalty
05:57:16 <coppro> ah, ok
05:57:24 <coppro> wait, how?
05:57:31 <ehirdiphone> Basically
05:57:37 <ehirdiphone> If you say
05:57:43 <ehirdiphone> Read an int from stdin
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:14 <ehirdiphone> You must satisfy the compiler
05:58:18 <ehirdiphone> That it is even
05:58:30 <ehirdiphone> Perhaps it can infer it if you do a branch
05:58:37 <ehirdiphone> Failing that, DIY
05:58:47 <soupdragon> (because you can't do case analysis on types)
05:58:51 <ehirdiphone> (pass the proof argument yourself)
05:59:01 <coppro> so... attempting another gross oversimplification here... encoding the range of values into the type?
05:59:08 <ehirdiphone> No.
05:59:21 <ais523> more like set of values, only it's allowed to be infinite
05:59:35 <ehirdiphone> coppro: They are real values
05:59:35 <ais523> and you can have loads of types which are similar except in the value sets, automatically generated
05:59:39 <ehirdiphone> Flesh and blood
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:28 <ehirdiphone> Then the value doesn't matter to the type
06:00:37 <ehirdiphone> Voilà, dependency goes poof
06:00:52 <coppro> ok, now I'm really confused
06:01:11 <ehirdiphone> coppro: it's magic.
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:03 <ehirdiphone> coppro: Precisely
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:03:44 <ehirdiphone> You have to prove it.
06:03:47 <coppro> ok
06:04:02 <ehirdiphone> (which is just... Writing the code that shows it, basically)
06:04:20 <ehirdiphone> But really, it's pretty simple.
06:04:33 <ehirdiphone> Just doesn't sound it.
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:06:18 <coppro> "value liberator"?
06:07:00 <ehirdiphone> Lets you express stuff you can't otherwise
06:07:04 <ehirdiphone> Like printf
06:07:07 <coppro> oh, right
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:09:39 <ehirdiphone> Nope
06:11:23 <coppro> in Erlang, you could do something like printf ([%%, %d, RestOfString], [SomeInteger, RestOfArgs]) -> printAsInteger(SomeInteger), printf(RestOfString, RestOfArgs).
06:11:34 <ehirdiphone> Oh
06:11:50 <ehirdiphone> The type was pattern matching on the string
06:11:57 <ehirdiphone> But all functions have that
06:12:23 <ehirdiphone> It was just a type with the kind (type's type) String -> Type
06:12:28 <coppro> right
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:13:22 <ehirdiphone> Printf does that too
06:13:28 <ehirdiphone> The string affects the type
06:14:07 <coppro> but scanf is a more interesting example
06:14:08 <ehirdiphone> But continue
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:39 <ehirdiphone> Colloquy borked
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:51 <ehirdiphone> I do not understand your analogy
06:15:56 -!- Sgeo_ has joined.
06:15:59 <ehirdiphone> pikhq: Saw it first time
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:18 <pikhq> :P
06:16:40 <coppro> it appeared to me to occur right after he arrived
06:16:47 <coppro> he may have caught it
06:16:49 <pikhq> Darned latency.
06:16:57 <coppro> yay IRC
06:17:29 <ehirdiphone> copprorather than simply waiting around and hoping things come out right
06:17:35 <ehirdiphone> Then what pikhq said
06:17:38 <coppro> ehirdiphone: well... basically, suppose I do printf(some_user_string, 3)
06:17:39 <ehirdiphone> That he repeated
06:17:45 <ehirdiphone> Miss anything?
06:17:53 <ehirdiphone> coppro: Wait
06:18:00 <coppro> waiting
06:18:17 <ehirdiphone> That would simply give a type inferrence error
06:18:32 <ehirdiphone> I think this would work:
06:18:56 <ehirdiphone> if s == "%d" then printf s 3 else return ()
06:19:00 <coppro> right
06:19:05 <ehirdiphone> Failing that...
06:19:10 <ehirdiphone> It's proof time
06:19:27 <ehirdiphone> M
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:51 <ehirdiphone> coppro: Hm?
06:19:52 <coppro> yeah, printf would be a nasty proof
06:20:02 <ehirdiphone> No need to prove printf.
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:20:27 <ehirdiphone> ie
06:20:39 <ehirdiphone> That s is only constant output
06:20:48 <ehirdiphone> and one formatting directive
06:21:01 <ehirdiphone> That takes an Integer
06:21:06 <coppro> agreed
06:21:12 <ehirdiphone> But honestly?
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:09 <ehirdiphone> That's not a user strung
06:22:13 <ehirdiphone> String
06:22:22 <coppro> It may be loaded from a file
06:22:25 <ehirdiphone> Compile those in, yo.
06:22:35 <ehirdiphone> Parse the files at compile-time.
06:22:37 <coppro> for 30 different languages? no thanks
06:22:52 <ehirdiphone> Compile only the ones you need.
06:22:53 <coppro> anyway, we're getting sidetracked
06:22:59 <ehirdiphone> Anyway
06:23:06 <ehirdiphone> Alternatively
06:23:30 <ehirdiphone> Make a module signature Translation
06:23:33 <ehirdiphone> With eg
06:23:49 <ehirdiphone> big_error :: Integer -> String
06:23:54 <ehirdiphone> Implementation?
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:24:44 <ehirdiphone> Ok back on track
06:24:52 <ehirdiphone> coppro: No
06:24:58 <ehirdiphone> Wrong terminology
06:25:03 <coppro> ok
06:25:09 <coppro> correct terminology?
06:25:15 <ehirdiphone> You don't take Integer-that-is-even
06:25:22 -!- cal153 has quit.
06:25:31 <ehirdiphone> You take Integer and that-Integer-is-even
06:25:43 <ehirdiphone> With the latter hopefully being inferred by the compiler
06:25:50 <coppro> ok
06:26:05 <coppro> this makes it feel even more Erlangish to me
06:26:08 <coppro> but w/e
06:26:08 <ehirdiphone> It's like having a type
06:26:17 <ehirdiphone> Even (int)
06:26:27 <ehirdiphone> Even 2 has one value
06:26:30 <ehirdiphone> call it poop
06:26:40 <ehirdiphone> poop :: Even 2
06:26:43 <ehirdiphone> but
06:26:52 <coppro> Erlang: my_function (I) where is_int(I) and I mod 2 == 0 -> whatever
06:26:53 <ehirdiphone> Even 1 has NO values!
06:27:03 <ehirdiphone> (nothing) :: Even 1
06:27:14 <ehirdiphone> So the compiler passes "poop" in
06:27:20 <ehirdiphone> If the number is even
06:27:24 <ehirdiphone> It won't type
06:27:28 <ehirdiphone> Erm
06:27:30 <ehirdiphone> Will
06:27:33 <ehirdiphone> Get it?
06:28:16 <coppro> yes
06:28:30 <ehirdiphone> coppro: So
06:28:40 <ehirdiphone> If we don't know the value of n
06:28:41 <ehirdiphone> The co
06:28:44 <ehirdiphone> Mpiler
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:28:48 <coppro> ?
06:28:53 <ehirdiphone> Cannot tell if (poop :: Even n)
06:28:57 <ehirdiphone> Is well typed
06:29:07 <ehirdiphone> And that's where proofs come in
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:29:55 <ehirdiphone> Yes it does.
06:30:00 <coppro> wait, what?
06:30:01 <ehirdiphone> Let me show you.
06:30:05 <coppro> ok
06:30:16 <coppro> btw, can you just type in a pastebin rather than a picture?
06:30:24 <ehirdiphone> iPhone actually
06:30:27 <ehirdiphone> Just one line
06:31:12 <ehirdiphone> evenClub :: (n::Integer) -> {Even n} -> AwesomeParty
06:31:21 <ehirdiphone> {} is agdas notAtion for
06:31:30 <coppro> also, btw, ZREO finished OoT finally; it's awesome
06:31:31 <ehirdiphone> "infer vAlue if possible"
06:31:33 <ehirdiphone> SO
06:31:37 <ehirdiphone> Don't talk btw
06:31:44 <augur> o hai
06:31:57 <coppro> not talking about anything relevant
06:31:59 <ehirdiphone> When we do (evenClub 2)
06:32:05 <ehirdiphone> The compiler does
06:32:15 <ehirdiphone> evenClub 2 {poop}
06:32:24 <coppro> ah, ok
06:32:28 <coppro> I get it now!
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:41 <ehirdiphone> It checks that it is... Voilà!
06:32:51 <augur> voila!
06:32:56 <ehirdiphone> Obviously, the poop param is erased during compilation
06:33:04 <ehirdiphone> As it is useless at runtime
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:33:28 <ehirdiphone> Not thought of
06:33:35 <ehirdiphone> This is how it actually works
06:33:37 <coppro> I know
06:33:39 <ehirdiphone> (in agda)
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:34:58 <ehirdiphone> + syntactic sugar
06:35:03 <ehirdiphone> = tada?
06:35:18 <ehirdiphone> That'd be
06:35:32 <ehirdiphone> {IsTrue (even n)}
06:35:38 <ehirdiphone> Or something
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:04 <ehirdiphone> So I haven't fully sorted it out yet
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:25 <ehirdiphone> coppro: Explain
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:39:44 <ehirdiphone> coppro: Can you still explain?
06:39:47 <coppro> ehirdiphone: I'll try
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:06 <ehirdiphone> Also
06:41:11 <ehirdiphone> Irrelevant
06:41:13 <ehirdiphone> Say you
06:41:17 <coppro> ehirdiphone: just wait
06:41:18 <ehirdiphone> Remove the {}s
06:41:21 <ehirdiphone> Then
06:41:30 <ehirdiphone> You'd just have to append " poop"
06:41:34 <ehirdiphone> To your calls
06:41:41 <ehirdiphone> It's just sugar
06:41:45 <coppro> right, I get that
06:41:52 <coppro> but what if it wasn't
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:14 <coppro> agreed
06:42:17 <ehirdiphone> They are not mandatory
06:42:26 <ehirdiphone> So it is not equivalent
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:45 <ehirdiphone> Remember printf?
06:42:52 <coppro> ok, restate printf for me
06:43:02 <ehirdiphone> Logs. iPhone.
06:43:08 <coppro> right
06:43:10 <coppro> ok
06:43:16 <ehirdiphone> Grep "type Printf" back up a line or two.
06:43:27 <coppro> ugh, different syntax
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:45:06 <ehirdiphone> Not different syntax
06:45:10 <ehirdiphone> Syntax is the sane
06:45:13 <ehirdiphone> Same
06:45:24 <ehirdiphone> coppro: A fair amount.
06:45:32 <ehirdiphone> Almost did SKI once vm
06:45:38 <ehirdiphone> *once. M
06:45:44 <ehirdiphone> *once.
06:45:53 <coppro> SKI?
06:46:00 <coppro> ehirdiphone: do you know what enable_if is?
06:46:31 <ehirdiphone> No.
06:46:35 <ehirdiphone> Ski conbinatirs
06:46:40 <ehirdiphone> Conbinatirs
06:46:48 <ehirdiphone> Com bi nat IRS
06:46:50 <ehirdiphone> IRS
06:46:53 <ehirdiphone> Oes
06:46:53 <coppro> ok
06:46:56 <coppro> ors
06:46:57 <ehirdiphone> Ors
06:46:57 <coppro> I get it
06:47:02 <ehirdiphone> Google it :p
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:09 <ehirdiphone> Only works for compile time constants
06:49:18 <coppro> true, but the principle is the same
06:49:21 <ehirdiphone> You can't just handwave that away
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:49:42 <coppro> they are TC
06:49:45 <ehirdiphone> coppro: No
06:49:48 <ehirdiphone> Because
06:49:56 <ehirdiphone> That's like a run time type system
06:50:04 <ehirdiphone> It can simply pass the actual value
06:50:09 <ehirdiphone> Which we can't.
06:50:20 <coppro> well, allow me to continue
06:50:57 * coppro tries to remember where he's going wit hthis
06:51:02 <coppro> ah right.
06:51:23 <coppro> in the case of enable_if, you can implement arbitrary conditionals assuming appropriate predicates exist
06:51:38 <ehirdiphone> And?
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:48 <ehirdiphone> Which must be compile time constant
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:36 <ehirdiphone> And handwaving the rest away
06:53:37 <coppro> the whole C++ thing was an analogy; it's not perfect
06:53:39 <coppro> etc.
06:54:16 <ehirdiphone> coppro: Bit
06:54:18 <ehirdiphone> But
06:54:25 <ehirdiphone> That is more complicated
06:54:28 <ehirdiphone> printf
06:54:30 <coppro> of course it is
06:54:31 <ehirdiphone> And the like
06:54:40 <ehirdiphone> Require them to be usable as values
06:54:55 <ehirdiphone> So you're just introducing a new concept
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:11 <ehirdiphone> Without even any holes for propfs
06:55:15 <ehirdiphone> Proofs
06:55:27 <ehirdiphone> So... Why?
06:55:28 <coppro> since it's hard to explain without a concrete base to work from
06:55:36 <ehirdiphone> What is the advantage?
06:55:44 <coppro> I don't know if there's an advantage
06:55:50 <soupdragon> 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:34 <ehirdiphone> Compelling :P
06:56:39 <coppro> I don't think you'd need to keep the old one
06:56:45 <ehirdiphone> printf
06:56:55 <ehirdiphone> Not a "constraint"
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:19 <soupdragon> printf "%d" 3
06:57:27 <ehirdiphone> I gave more
06:57:27 <soupdragon> printf "%d %d" 3 4
06:57:38 <ehirdiphone> I gave the relevant type
06:57:47 <ehirdiphone> The magic that makes it work
06:57:53 <coppro> not enough, at least not me looking through scrollback
06:57:58 <ehirdiphone> (well. Just for %d)
06:58:01 <soupdragon> append is a cool one
06:58:11 <ehirdiphone> It's right after the printf signature you dolt
06:58:19 <ehirdiphone> :P
06:58:47 <soupdragon> 0 + m = m ; S n + m = S (n + m).
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:58:53 <coppro> *synatx
06:58:55 <coppro> *syntax
06:59:14 <soupdragon> _+_ : N -> N -> N, _++_ : Vector A n -> Vector A m -> Vector A (n + m)
06:59:27 <soupdragon> it's amazing that ++ typechecks
06:59:56 <ehirdiphone> soupdragon: BUT CAN IT BLEND^WINFER
06:59:59 <ehirdiphone> :P
07:00:24 <ehirdiphone> coppro: Note that (x:xs) is cons
07:00:34 <ehirdiphone> And [] == ""
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:27 <coppro> Is that it?
07:01:32 <ehirdiphone> Ya
07:01:36 <coppro> ok
07:01:46 <coppro> so where does the type replacement come in to play here?
07:01:59 <ehirdiphone> Type replacement?
07:02:09 <coppro> err, the whatever
07:02:11 <coppro> the funny magic
07:02:16 <ehirdiphone> What?
07:02:23 <coppro> wait...
07:02:30 * coppro facepalms
07:02:39 <coppro> ok, so I'm stupid
07:02:49 <coppro> but nvm that
07:02:53 <ehirdiphone> What did you do? :P
07:03:10 <coppro> I misunderstood the way functions work
07:03:19 <ehirdiphone> Howso?
07:03:35 <coppro> specifically, "a b" is a left-associative operator that executes a on b
07:03:45 <soupdragon> oh right
07:03:55 <coppro> for multi-arg functions, there's syntactic sugar in the declaration that creates a forwarding function with less arguments
07:03:56 <soupdragon> you mean like f x y as f(x,y)
07:04:00 <coppro> no
07:04:03 <ehirdiphone> coppro: Ahh yep
07:04:04 <soupdragon> yes you do
07:04:10 <coppro> f x y as f'(x)(y)
07:04:10 <soupdragon> :D:D:D:D:D:D:D
07:04:14 <soupdragon> f' ?
07:04:30 <ehirdiphone> coppro: Ya welcome to currying
07:04:48 <coppro> as I said, my functional programming experience is sadly lacking :(
07:04:59 <ehirdiphone> No worries
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:14 <ehirdiphone> How did it change your understanding?
07:05:24 <ehirdiphone> Don't see currying in printf
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:05:39 <ehirdiphone> Where
07:05:46 <soupdragon> just think of
07:05:52 <soupdragon> f x y as f(x,y)
07:05:56 <ehirdiphone> All the doohickeys have 1 arg
07:06:06 <ehirdiphone> Oh
07:06:08 <ehirdiphone> OH
07:06:11 <coppro> YEAH
07:06:24 <ehirdiphone> In type Primtf's right Gand side
07:06:27 <ehirdiphone> Hand
07:06:32 <coppro> yeah, it returns a function
07:06:41 <ehirdiphone> Nope
07:06:45 <coppro> wait, no?
07:06:45 <ehirdiphone> Returns a type
07:06:56 <ehirdiphone> coppro: For
07:06:57 <coppro> well, a function type
07:07:05 <ehirdiphone> A format string fmt
07:07:07 <coppro> printf "%d" gives me an Integer -> IO, correct?
07:07:13 <soupdragon> no
07:07:14 <ehirdiphone> IO ()
07:07:21 <ehirdiphone> soupdragon: Yes.
07:07:25 <soupdragon> Printf "%d" = Integer -> IO
07:07:32 <coppro> right
07:07:34 <ehirdiphone> IO ()
07:07:36 <ehirdiphone> soupdragon: A
07:07:38 <ehirdiphone> As in
07:07:47 <coppro> oh wait, that was soupdragon
07:07:47 <ehirdiphone> A value if that type
07:07:57 <coppro> ok, nvm. Your nicks have a too-similar length
07:07:59 <ehirdiphone> coppro made no error
07:08:11 <soupdragon> printf "%d" : Integer -> IO
07:08:14 -!- ehirdiphone has changed nick to pooop.
07:08:19 <coppro> lol
07:08:23 <pooop> You're welcome
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:26 <pooop> QED
07:09:26 <coppro> oh dear
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:25 <Cu> lol
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:10:59 * Cu grimaces
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:11:59 <ehirdiphone> (but only some£
07:12:03 <Cu> ok
07:12:12 <ehirdiphone> )
07:12:14 <ehirdiphone> Wait
07:12:40 <ehirdiphone> Zoop is the argument or the action of Ingerring a value?
07:12:43 <ehirdiphone> Which
07:12:49 <Cu> the latter
07:12:52 <ehirdiphone> Ok
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:11 <ehirdiphone> Real argument.
07:13:19 <Cu> imaginary in the sense that the user never sees it
07:13:21 <ehirdiphone> As real as any argument.
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:13:47 <ehirdiphone> But no
07:13:58 <ehirdiphone> Not based on some value
07:14:11 <ehirdiphone> It is disconnected from dependentvtyping
07:14:33 <ehirdiphone> I mean it handles it
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:08 <ehirdiphone> Although it's not much use otherwise
07:15:13 <Cu> Even n is a family of types, one for each integer, all sharing the same values?
07:15:27 <ehirdiphone> Almost right.
07:15:46 <ehirdiphone> All the even ns share the same value, poop
07:15:56 <ehirdiphone> All the odd ns have no values at all
07:16:11 <ehirdiphone> I.e you cannot have a value of type Even 1
07:16:12 <Cu> ok
07:16:45 <ehirdiphone> Cu: All the compiler does is
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:16:53 <ehirdiphone> Gives it "poop"
07:16:55 <ehirdiphone> That's it
07:17:00 <ehirdiphone> No magic
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:38 <ehirdiphone> q1?
07:18:44 <Cu> point 1, whatever
07:18:46 <Cu> tired
07:18:52 <ehirdiphone> Point 1?
07:18:53 <Cu> point 2, I don't quite understand
07:18:59 <Cu> point 1 = simpler
07:19:00 <ehirdiphone> Oh
07:19:01 <ehirdiphone> I see
07:19:07 <Cu> point 3, I'm not sure is related
07:19:13 <ehirdiphone> The way to pass proofs is
07:19:25 <ehirdiphone> evenClub input {...}
07:19:36 <Cu> ah, I see
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 <coppro> right, ok
07:19:59 -!- puzzlet has changed nick to puzlet.
07:20:06 -!- puzzlet has joined.
07:20:11 <soupdragon> just a thought
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:20:54 <ehirdiphone> soupdragon: Yes
07:20:56 <soupdragon> although it's isomorphic to nat
07:21:03 <ehirdiphone> How would you erase the index tho?
07:21:15 <coppro> Ugh, just discovered a major flaw with ZREO's "official" OoT release
07:21:15 <ehirdiphone> The issue with that is
07:21:15 <soupdragon> just delete it in a text editor
07:21:20 <soupdragon> I don't mean automatically
07:21:22 <coppro> gonna have to complain
07:21:23 <ehirdiphone> No convenient {...}
07:21:39 <ehirdiphone> soupdragon: How
07:21:42 <ehirdiphone> Lets say
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> I was thinking of
07:22:22 <soupdragon> data Even : nat -> * where EZ : Even Z ; ES : Even n -> Even (S (S n))
07:22:23 <ehirdiphone> How do you erase the arg there?
07:22:37 -!- puzzlet has joined.
07:22:40 <soupdragon> which you can erase to
07:22:49 <soupdragon> data Even : * where EZ : Even ; ES : Even -> Even
07:22:59 <ehirdiphone> soupdragon: totally boring tho
07:23:08 <soupdragon> not to me
07:23:11 <ehirdiphone> writing a boring type for every constraint
07:23:54 <ehirdiphone> coppro: Oot the zelda game?
07:23:56 <ehirdiphone> or
07:23:59 <coppro> ehirdiphone: yes
07:24:08 <ehirdiphone> "release"?
07:24:12 <coppro> ZREO = Zelda Reorchestrated, an awesome project to redo Zelda music in awesomeness
07:24:18 <ehirdiphone> Ah.
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:26:51 <ehirdiphone> But prefix and postfix too :D
07:27:06 <coppro> Perl 6-style?
07:27:12 <coppro> or Agda style?
07:27:21 <ehirdiphone> My style.
07:27:30 * coppro doesn't hold his breath
07:27:49 <ehirdiphone> How do you have a style anyway
07:28:01 <ehirdiphone> It's just pre and postfix ops
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:30 <ehirdiphone> Anyway whaddya mean
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:29:44 <ehirdiphone> coppro: All the time
07:29:52 <ehirdiphone> A lot of others don't
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:03 <ehirdiphone> coppro: I thought I did the opposite xD
07:31:29 <coppro> ehirdiphone: I mean something you don't understand AND can't readily Google
07:31:41 <ehirdiphone> postfix ! :: Nat -> Nat
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 <coppro> ok
07:33:37 <ehirdiphone> coppro: I'd just use operator precedence to disambiguate
07:33:47 <ehirdiphone> Failing that, flag an error
07:33:51 <coppro> ehirdiphone: ok
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:15 <ehirdiphone> Like haskell
07:34:31 <ehirdiphone> ehirdiphoneinfix + :: {n::Type} -> {Num n} -> n -> n -> n
07:34:39 <ehirdiphone> notice anything interesting?
07:34:59 <coppro> you defined your own keyword there?
07:35:05 <ehirdiphone> Lol
07:35:11 <ehirdiphone> No
07:35:17 <coppro> what does {n::Type} mean?
07:35:20 <ehirdiphone> Ignore that part
07:35:22 <coppro> inference of n's type?
07:35:37 <ehirdiphone> coppro: You know what (n::Int) means right?
07:35:46 <coppro> I think so
07:35:48 <ehirdiphone> Int argument, magic dependent value n
07:35:56 <coppro> magic dependent value?
07:36:01 <coppro> I thought of it as "named n"
07:36:07 <ehirdiphone> Well yes
07:36:25 <ehirdiphone> So n is thr value if the arg
07:36:27 <coppro> {} means infer the type, and let me refer to it as Type?
07:36:32 <ehirdiphone> Which we don't know ar that point
07:36:35 <ehirdiphone> coppro: Ni
07:36:36 <ehirdiphone> No
07:36:44 <ehirdiphone> Listen
07:36:53 <ehirdiphone> Int :: Type
07:36:56 <ehirdiphone> That is
07:37:03 <ehirdiphone> Types are of type Type
07:37:06 <ehirdiphone> That's why
07:37:19 <ehirdiphone> type Printf :: String -> Type
07:37:44 <coppro> oh, ok
07:37:48 <ehirdiphone> So {t::Type} is "a type t; infer value"
07:37:57 <ehirdiphone> That's how we do polymorphism!
07:38:07 <coppro> so t becomes whatever the argument's type is?
07:38:13 <ehirdiphone> We can use t later in the signature
07:38:16 <ehirdiphone> So
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:38:41 <ehirdiphone> Obviously t has to be that type!
07:38:44 <ehirdiphone> coppro: No
07:38:47 <coppro> :(
07:38:56 <ehirdiphone> It is another argument
07:39:21 <ehirdiphone> infix + :: {n::Type} -> {Num n} -> n -> n -> n
07:39:28 <ehirdiphone> Notice anything else interesting?
07:39:59 <coppro> it's an infix that appears to take 3 arguments?
07:40:11 <soupdragon> 4
07:40:12 <ehirdiphone> Four actually.
07:40:19 <ehirdiphone> Last n is the result
07:40:37 <ehirdiphone> coppro: It's {Num n}
07:40:45 <ehirdiphone> That's how we do typeclasses!
07:40:55 <coppro> oh, yeah, I'd worked that bit out
07:41:02 <ehirdiphone> >_<
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:42:46 <ehirdiphone> No it's a different thing
07:42:50 <ehirdiphone> Wait a sex
07:42:51 <ehirdiphone> ...
07:42:54 <ehirdiphone> Sec
07:43:11 <ehirdiphone> Link me to todays log please
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:44:55 <ehirdiphone> But a lot mote before that
07:45:00 * coppro wonders why he feigns stupidity in this channel
07:45:04 <ehirdiphone> First use of "segue" in log
07:45:15 <ehirdiphone> See if you missed any of it
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:27 <coppro> s/realized/realize/
07:47:33 <ehirdiphone> What question?
07:47:57 <ehirdiphone> coppro: Btw there's a blip in the module talk
07:48:05 <ehirdiphone> Scroll down if you think it's over
07:48:16 <ehirdiphone> Before "c="
07:48:37 <ehirdiphone> It's not over
07:48:56 <coppro> right, I remembered that vaguely
07:49:06 <ehirdiphone> So what was the question?
07:49:17 <coppro> whether you would have full-on type genericism
07:49:40 <ehirdiphone> Eh?
07:49:43 <coppro> specifically, the ability to make an entire interface dependent on another type
07:49:50 <ehirdiphone> Like howso
07:49:56 <coppro> which, clearly you can do by generating modules from functors
07:50:02 <ehirdiphone> Like java genetics?
07:50:05 <ehirdiphone> Genetics
07:50:07 <ehirdiphone> Fff
07:50:09 <coppro> lol
07:50:21 <ehirdiphone> If so, yeah, old hat. Of course.
07:50:22 <coppro> java's genetics consist of a whole bunch of un-evolution
07:50:33 <soupdragon> huh?
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:51:01 <ehirdiphone> Yeah
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:54:44 <coppro> try me
07:55:05 <ehirdiphone> But it'd be 50000000 lines of typing. :P
07:55:12 <coppro> oh ok
07:55:19 <ehirdiphone> I'll snail mail you a cassette :D
07:56:05 <ehirdiphone> All this phone and I never speak into it.
07:57:06 * ehirdiphone tries the voice recorder
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:07:40 <ehirdiphone> coppro: What did I miss?
08:07:55 <coppro> nothing
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:00 * coppro is not sure
08:09:24 <ehirdiphone> It's not squeaky! Just... Hovering.
08:09:56 <coppro> as opposed to hemming-and-hawing?
08:10:00 <ehirdiphone> Lawlz
08:10:05 <ehirdiphone> I'll just send it
08:10:09 -!- ehirdiphone has quit (Client Quit).
08:13:11 -!- ehirdiphone has joined.
08:13:22 <ehirdiphone> coppro: Sending them by email now
08:13:32 <coppro> ok
08:13:43 <ehirdiphone> Wait for all three parts to arrive then set them up in a playlist or sth
08:13:50 <ehirdiphone> Just software foibles
08:13:54 <coppro> sth?
08:14:00 <ehirdiphone> Would prefer it were continuous
08:14:04 <coppro> ok
08:14:08 <ehirdiphone> coppro: Somethubg
08:14:11 <ehirdiphone> Thing
08:14:14 <ehirdiphone> =sth
08:14:16 <coppro> oh
08:14:27 <ehirdiphone> .m4a sorry. iPhones fault
08:14:56 <coppro> yuk
08:16:06 <ehirdiphone> Any arrived yet?
08:16:28 <coppro> negative
08:17:03 <ehirdiphone> My speaking skills are improving, not many ums or pauses in that
08:17:14 <ehirdiphone> Or mistakes :P
08:18:19 <ehirdiphone> coppro: in spam maybe?
08:18:48 <coppro> unless you're trying to sell me replica rolexes, no
08:19:00 <coppro> *rep1ica ro1exes
08:20:49 <ehirdiphone> This is coppro @ gmail com right
08:20:57 <coppro> no
08:20:59 <coppro> rideau3@gmail.com
08:21:06 <coppro> thanks for spamming some random guy
08:21:10 <ehirdiphone> :D
08:21:17 -!- ehirdiphone has quit ("Get Colloquy for iPhone! http://mobile.colloquy.info").
08:21:32 <soupdragon> l o l
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:06 <coppro> :D
08:23:18 <coppro> too lazy to type /msg ais523 on a chat without tab-complete
08:23:40 -!- ehirdiphone has joined.
08:23:48 <ehirdiphone> remaile (har har funny pun)
08:23:55 <ehirdiphone> *remailed
08:24:20 <ais523> coppro: heh, I was just thinking that myself
08:24:47 <ehirdiphone> Propose or accept what what
08:24:52 <augur> HAHAHA
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:25:45 <ehirdiphone> KoL is kinda rubbish IMO :|
08:25:50 <ais523> agreed
08:25:57 <augur> watsa kol
08:26:01 <coppro> that's sorta the point
08:26:19 <ehirdiphone> "Its meant to be shit don't you SEE"
08:26:24 <ais523> augur: a rather low-tech MMO
08:26:36 <augur> oh ok
08:26:42 <ehirdiphone> Web based
08:26:50 <ehirdiphone> It's really just clicking yes a lot
08:26:55 <ehirdiphone> Or going somewhere
08:27:06 <ehirdiphone> Then clicking fight a lot
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:33:25 <ehirdiphone> Did that get cut off?
08:33:30 <ais523> no, it didn't
08:33:38 <ehirdiphone> Ended at "member is recruited"
08:33:44 <ais523> yes
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:21 <ehirdiphone> And they don't make a profit per se
08:34:29 <ehirdiphone> EVERYONE pays less
08:34:34 <ehirdiphone> It's altruistic
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:17 <ais523> no
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:34 <ehirdiphone> Intriguing.
08:36:55 <ehirdiphone> ais523: But that's how they WORK! evryone pays an equal amount
08:36:59 <ehirdiphone> Cost/members
08:37:02 <ehirdiphone> It
08:37:07 <ais523> ehirdiphone: I don't hate the collective itself
08:37:10 <ehirdiphone> 's the whole point
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 <ehirdiphone> Thing is
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:38:49 <ehirdiphone> *THEB
08:38:56 <ehirdiphone> *THEN
08:40:55 <ehirdiphone> silence!
08:41:45 <ehirdiphone> btw they're cooperatives not collectives
08:42:03 <ehirdiphone> Wonder if anyone's registered http://chicken.coop yet :D
08:42:14 <ehirdiphone> Negative
08:45:16 <ehirdiphone> ais523: Do you want my lovely voice explanations of frp, coppro iz ded :<
08:45:35 <ais523> ehirdiphone: frp?
08:45:55 <ais523> ehirdiphone: oh, that's a good argument, about switching
08:45:57 <ehirdiphone> ais523: Should I take that as a yes? :P
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:28 <ehirdiphone> Like hosting :p
08:46:34 <ehirdiphone> ais523: _|_
08:46:41 <ehirdiphone> That's not a middle finger
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:47:46 <ehirdiphone> No.
08:47:58 <ehirdiphone> I have never ever heard that.
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:22 <ehirdiphone> ais523: Actually, errors are _|_ too
08:48:37 <ehirdiphone> poop = error "blah"
08:48:41 <ehirdiphone> poop is bottom
08:48:43 <ais523> it's kind-of a different sort of return value...
08:48:48 <ehirdiphone> Nope
08:48:51 <ais523> what about throwing an exception past the caller to a handler outside?
08:49:06 <ehirdiphone> All types are TheType | _|_
08:49:17 <ehirdiphone> Unless you use Total FP
08:49:22 <ehirdiphone> But that's sub tc
08:49:36 <ehirdiphone> ais523: In the io monad
08:49:41 <ehirdiphone> If not, yep _|_
08:49:56 <ehirdiphone> Want those audios? :-(
08:50:36 <ais523> ok, so this explains bottom, which almost certainly has its own unicode char
08:50:46 <ehirdiphone> Yeah
08:50:54 <ehirdiphone> Logical false or sth
08:51:08 <ais523>
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:34 <augur> well, i am, but.
08:53:35 <augur> butt.
08:53:57 <augur> it seems like Bottom can be non-termination, but it can be other things as well
08:54:02 <augur> including null
08:54:13 <ehirdiphone> ais523: There are two chars iirc
08:54:21 <ehirdiphone> WANT THE AUDIO?
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:54:44 <ehirdiphone> ais523: The voice explanation of frp
08:54:57 <ais523> I'd prefer IRC
08:55:02 <ehirdiphone> SOMEONE LOVE ME ;;;;;;;;;;;_;;;;;;;;
08:55:11 <ehirdiphone> ais523: but I already recorded it :p
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:41 <ehirdiphone> augur: the ephebophilic way?
08:55:50 <ais523> ugh, filebin.ca is still malware-blocked
08:55:58 <augur> no ofcourse not
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
08:56:15 <augur> so so wrong
08:56:35 <ehirdiphone> Yeah. Blocks are sacrosanct!
08:56:41 <ehirdiphone> Oh I love comedic timing
08:58:03 <ehirdiphone> NOBODY LIKES MY VOICE ;;;;;;;;;_;;;;;;;;;
09:00:59 <augur> your voice is girly
09:01:12 <augur> so i imagine people into girls like your voice
09:01:58 <ehirdiphone> :|
09:03:46 <augur> its ok
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:11:10 <augur> wabi
09:14:38 -!- mycroftiv has quit (Read error: 104 (Connection reset by peer)).
09:15:42 <ehirdiphone> My conversation died :(
09:15:49 <augur> :(
09:15:56 <ehirdiphone> I was enjoying talking about that language
09:16:12 <augur> what language
09:19:08 <ehirdiphone> 4 hours 12 minutes. I talked about it continuously for about that long. Wow.
09:19:17 <ehirdiphone> augur: My language.
09:19:26 <augur> which language is that
09:19:30 <ehirdiphone> Mine.
09:19:36 <augur> which is?
09:19:43 <ehirdiphone> Mine.
09:19:45 <augur> :|
09:20:10 <ehirdiphone> Do you feel up to reading 4h12m of talk?
09:20:16 <augur> no
09:20:21 <augur> can you summarize it please
09:20:25 <ehirdiphone> No.
09:20:27 <augur> ok
09:21:27 <ehirdiphone> Oh well.
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:30:42 <ehirdiphone> So, I had a brilliterrible idea.
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:31:48 <ais523> heh
10:31:55 <ehirdiphone> Neural analogies whatever next
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:37:19 <ehirdiphone> It would be kinda cool actually
10:37:53 <ehirdiphone> ais523: imagine a modeline on a window
10:38:10 <ais523> ehirdiphone: heh
10:38:13 <ais523> although, what would the modes be
10:39:07 <ehirdiphone> Well, xwm-window-mode for one
10:39:22 <ehirdiphone> with the oblig menus with actions and settings
10:39:34 <ehirdiphone> Minor modes... hmm
10:39:53 <ehirdiphone> ais523: xwm-floating-mode, perhaps?
10:40:10 <ais523> no, that's C-x 5
10:40:18 <ehirdiphone> meaning?
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:35 <ehirdiphone> new-frame or sth?
10:40:38 <ais523> yes
10:40:56 <ehirdiphone> that would just open an emacs frame in an emacs buffer :D
10:41:50 <ais523> no, the point is
10:41:53 <ais523> your applications are buffers
10:41:58 <ehirdiphone> windows
10:41:59 <ais523> you can swap them in and out of windows at will
10:42:04 <ehirdiphone> Not applications
10:42:12 <ehirdiphone> ais523: You misunderstand
10:42:18 <ais523> ehirdiphone: you mis-emacs
10:42:34 <ehirdiphone> X11 windows would be drawn in their own BONAFIDE emacs buffer
10:42:40 <ehirdiphone> Not emacsalike
10:42:47 <ehirdiphone> Actually an 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:17 <ehirdiphone> IFC
10:43:20 <ehirdiphone> Ofc
10:43:23 <ais523> one window produced by an application under a normal WM = one Emacs buffer
10:43:30 <ehirdiphone> yes
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:20 <ehirdiphone> *us:
10:44:52 <ais523> ehirdiphone: err, no
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:34 <ehirdiphone> ais523: X11 window
10:45:37 <ais523> ah, ok
10:45:40 <ais523> I was talking about emacs window
10:45:48 <ais523> how would you do extra emacs frames, though?
10:45:55 <ehirdiphone> Wouldn't
10:46:01 <ehirdiphone> I might think about doing it
10:46:03 <ehirdiphone> Dunno
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:20 <ehirdiphone> Yes, but Emacs is tiling.
10:46:26 <ais523> it's tiling and floating
10:46:36 <ais523> hmm... I wonder if C-x 5 o works?
10:46:48 <ehirdiphone> no. Emacs itself is tiling
10:47:01 <ehirdiphone> Other WMs do the floating
10:47:11 <ais523> well, ok
10:47:15 <ehirdiphone> so an emacs wm should do as emacs does
10:47:18 <ais523> hmm... this is a tricky one
10:47:19 <ehirdiphone> And only tile
10:47:32 <ehirdiphone> ais523: BUT
10:47:42 <ehirdiphone> If floating is to be offered
10:48:15 <ehirdiphone> It should be recognised as a heresy unique to the Xfolk; lacking as the result is in Emacs mannerisms,
10:48:28 <ehirdiphone> being an unadorned Xdevil,
10:48:50 <ehirdiphone> and so on — it is of the Xwindow.
10:49:17 <ehirdiphone> Therefore, xwm-floating-mode. Q.E.D.
10:49:46 <ehirdiphone> in the model here emacs frames "don't exist"
10:49:53 <ehirdiphone> It's like an emacs os
10:49:59 <ehirdiphone> Emacs is the interface
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:42 <ais523> as it isn't anywhere
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:32 <ehirdiphone> ais523: No such thing.
10:51:36 <ais523> exactly
10:51:37 <ehirdiphone> Implementation detail.
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:07 <ehirdiphone> It is omnipotent and sovereign over them.
10:52:12 <ais523> e.g. it would make no sense for C-x o to /cycle/ to it
10:52:18 <ehirdiphone> brb
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:37 <ehirdiphone> Erm
10:52:39 <ehirdiphone> View
10:52:41 <ehirdiphone> You know
10:52:51 <ais523> ehirdiphone: oh, in that case, it wouldn't render at all
10:52:52 <ehirdiphone> Not in the tiling buffer arrangement
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:53:12 <ehirdiphone> brb
10:55:50 -!- oerjan has joined.
11:07:50 <ehirdiphone> Hi oerjan
11:07:55 <oerjan> hi ehirdiphone
11:08:12 <ehirdiphone> oerjan: Good luck logreading
11:08:24 <oerjan> nah
11:08:30 <ehirdiphone> 4 hrs 12 mins continous talk about my language
11:08:32 <oerjan> just searched for my name today
11:08:48 <ehirdiphone> You missed out on so much :(
11:08:52 <oerjan> s/name/nick/
11:08:59 <ehirdiphone> ais523: Issue
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:23 <ehirdiphone> Suck for editing
11:09:39 <ais523> ehirdiphone: really? I often have over 30 or so buffers open
11:09:43 <ehirdiphone> oerjan: it has haskelly type theory!
11:09:45 <ais523> I rarely kill them, you see
11:09:51 <ehirdiphone> ais523: well, ok
11:09:55 <ais523> and don't use the buffer list at all, except by mistake
11:09:57 <ehirdiphone> But what to name them!
11:10:00 <ehirdiphone> *?
11:10:06 <ehirdiphone> The window title?
11:10:17 <ehirdiphone> "title - prog"?
11:10:23 <ais523> with asterisks around it if it's not meant to be saved
11:10:33 <ehirdiphone> "title - prog [xwm]"
11:10:34 <ais523> yes, you should be able to save buffers even if they contain windows
11:10:42 <ehirdiphone> ais523: uh. No.
11:10:52 <ehirdiphone> but ugh, it'd be ugly
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 <oerjan> *in over your head
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:10 <ehirdiphone> It's a wm not an os
11:12:12 <ais523> pause, turn it off
11:12:14 <oerjan> at the very least
11:12:21 <ehirdiphone> ais523: M x tetris
11:12:22 <mycroftiv> cant you just make sure that you are within the formal boundaries established by hindley-milner typing?
11:12:31 <ehirdiphone> oerjan: And they're open source
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:38 <ehirdiphone> mycroftiv: I exceed those boundaries
11:12:40 -!- FireFly has joined.
11:12:44 <ehirdiphone> TC type system
11:12:53 <ehirdiphone> W/ dependent types
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:14:15 <ehirdiphone> easiest doctorate evar
11:15:10 <ehirdiphone> oerjan: but yeah, it won't be easy
11:15:55 <ehirdiphone> so what it's so damn awesome :|
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:17:22 <soupdragon> incomplete
11:17:28 <ehirdiphone> Bottoming out is going wrong to me
11:17:34 <soupdragon> unsound would be like, 3 : String
11:18:03 <ehirdiphone> it must be one of either
11:18:11 <ehirdiphone> presumably incomplete
11:18:15 <soupdragon> oerjan the fun with dependent types is you need to interleave the value normalization proof
11:18:19 <ehirdiphone> i.e. Sound
11:18:29 <ehirdiphone> soupdragon: ouch
11:18:44 <ehirdiphone> maybe I'll contract a phd out to do the proof :)
11:19:03 <ehirdiphone> Or just assume it's sound xD
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:39 <ehirdiphone> types bottoming out as in
11:19:43 <oerjan> because if a proof of well-typed-ness can bottom out, then it is invalid
11:19:52 <ehirdiphone> Foo Integer = _|_
11:19:53 <ehirdiphone> ?
11:19:56 <oerjan> um proofs of types, i guess
11:19:57 <oerjan> no
11:20:11 <ehirdiphone> ah
11:20:13 <ehirdiphone> I see
11:20:14 <oerjan> that is not dependent.
11:20:23 <ehirdiphone> right
11:20:47 <ehirdiphone> oerjan: I was thinking of using a total subset
11:20:52 <ehirdiphone> for the proofs
11:22:53 <ehirdiphone> tbh I think my type system is likely incredibly similar to say agda
11:22:59 <ehirdiphone> just different notation
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:24:48 <soupdragon> least 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:26:50 <ehirdiphone> Don't want to make partiality a monad
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:27:53 <ehirdiphone> what mention?
11:27:58 <oerjan> of the monad
11:28:12 <ehirdiphone> ah
11:28:12 <oerjan> except it was not something implemented, iirc
11:28:14 <soupdragon> really?
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:14 <ehirdiphone> the partiality monad is that point
11:29:28 <soupdragon> yeah I have no idea how to do even simple proofs about termination for the partiality monad
11:29:54 <ehirdiphone> oerjan: wait, isn't epigram tc?
11:30:04 <ehirdiphone> You're thinking of that other Lang
11:30:07 <ehirdiphone> Charity
11:30:22 <oerjan> ehirdiphone: i thought epigram was a total language
11:30:46 <ehirdiphone> hmm. Maybe epigram 1 is but 2 not? Dunno
11:30:55 <ehirdiphone> Maybe both are total
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:32:33 <ehirdiphone> poop.
11:32:45 <oerjan> ehirdiphone: hm?
11:33:16 <ehirdiphone> anyway ur works and only has one phd behind it
11:33:22 <ehirdiphone> I rest my case :p
11:33:53 <soupdragon> Ur isn't actually dependently typed is it
11:34:09 <ehirdiphone> I think it is?
11:40:07 <ehirdiphone> hmm
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:06 <soupdragon> I wish I could compile it :|
11:41:17 <ehirdiphone> Why can't you?
11:41:33 <soupdragon> soem error to do with gmp or something
11:41:53 <ehirdiphone> I'll fix it gimme ssh :P
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:23:50 <cheater> hi guys
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:27:49 <pikhq> Sgeo: Yowza.
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 (?).
20:41:34 <oerjan> cheater: see above ^
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:56:18 <AnMaster> oerjan, dmm made piet!?
23:56:23 <coppro> yes
23:57:24 <oerjan> indeed
23:57:50 <oerjan> and several others
23:59:14 <coppro> http://dangermouse.net/esoteric/
←2009-12-29 2009-12-30 2009-12-31→ ↑2009 ↑all