00:07:26 -!- pikhq has joined. 00:15:08 To me, at least, GNU is more a part of the operating system than KDE is. 00:16:45 I reset my computer yesterday - so its gets a new name "befunge" 00:23:13 * Phantom_Hoover → sleep 00:27:17 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds). 00:34:43 -!- variable has quit (Ping timeout: 264 seconds). 00:36:15 -!- variable has joined. 00:39:19 -!- copumpkin has changed nick to MostInterestingM. 00:39:43 -!- MostInterestingM has changed nick to copumpkin. 00:40:04 copumpkin: hey what is the Monad instance for that 00:40:45 -!- elliott_ has joined. 00:40:46 it's too interesting to repeat 00:40:48 sorry 00:40:54 AWW 00:41:10 -!- elliott has quit (Read error: Connection reset by peer). 00:41:12 oh, the AW comonad transformer? 00:41:15 -!- elliott_ has changed nick to elliott. 00:41:17 -!- elliott has quit (Changing host). 00:41:17 -!- elliott has joined. 00:41:29 doesn't really work 00:41:39 there are comonad transformers? :D 00:42:14 . 00:42:19 http://hackage.haskell.org/package/comonad-transformers 00:43:12 * oerjan cunningly checks #haskell logs but is none the wiser 00:44:21 i'm sure Sgeo would like that AWW transformer 00:44:26 lol 00:46:00 -!- cheater00 has joined. 00:49:16 -!- cheater- has quit (Ping timeout: 240 seconds). 01:02:52 -!- nddrylliog has joined. 01:04:48 ohai. anyone alive? 01:05:09 no 01:05:10 :) 01:05:11 *GASP* *GACK* 01:05:31 Brains... 01:07:07 nice! 01:07:18 got a crazy ideas I'd like feedback on 01:07:26 -s 01:09:46 What is the ideas? 01:09:51 https://docs.google.com/present/edit?id=0AakBA-t72L0TZGZncTh0aGJfMTAwZzM0cTJmYzk&hl=en&authkey=CMyQ8Qc 01:10:15 ^ here it is, in its nake beauty. Bear in mind that it's 02:23 AM. 01:10:18 +d 01:11:06 who the fuck makes slideshows at 2:23 am 01:11:14 -!- Mathnerd314 has joined. 01:11:19 elliott: :D 01:11:28 nddrylliog: you're disturbed! 01:11:46 elliott: oh, breaking news. 01:11:50 :D 01:12:03 We also know that it's probably stupid to try to access element -1, or element i > size (syntactic sugar aside). 01:12:03 But we have to spell it out carefully so that the program won't crash and burn because we joyfully walked over the boundaries of the allocated memory. 01:12:08 nddrylliog: you may like http://www.ats-lang.org/. 01:12:29 basically, I'm hesitating between "this has been done before" and "nobody's smart enough to implement such a compiler" 01:12:29 nddrylliog: it's a low-level functional systems programming language with dependent types to ensure safety and correctness. 01:12:38 with option 2 being a little more hopeful than the first 01:12:59 oh yeah, ATS sounded fun 01:13:11 http://www.bluishcoder.co.nz/tags/ats/ are probably interesting posts since most of chris double's are :P 01:13:58 elliott: but I hope you undertand from my slideshow that what I'm suggesting is way more than just pre/post conditions 01:14:04 elliott: ooor just safety 01:14:05 well I haven't read any more yet! :D 01:14:23 "An array has constant time access to element of index 0" 01:14:26 and index N... but 01:14:31 is that important for the compiler to know? 01:14:51 that comes later 01:14:56 that's just a human description 01:14:59 with redundant rules, etc. 01:15:01 nddrylliog: looking at slide 11, i can safely say you're going to need to write proofs to program in this language 01:15:05 this part doesn't matter much, it's just examples 01:15:08 at least in complicated cases 01:15:25 elliott: I think that's a safe assumption, yeah 01:15:31 nddrylliog: that element inside array can be written as e.g. 01:16:08 Record ElementOf (array : Array) := mkElement { index : nat; index_in_range : index < sizeOf array; data : something goes here } 01:16:10 nddrylliog: in Coq 01:16:15 where "index < sizeOf array" represents a proof of that 01:16:25 yep 01:16:32 I should really take a look at Coq, it's been teasing me for years 01:16:40 such a Coqtease 01:16:42 i apologise 01:16:43 i'm sorry 01:16:46 don't kick me oerjan 01:16:52 i'm a good person, inside 01:17:09 goddamn, 78 google results 01:17:14 :D 01:17:16 there are weirder people than me 01:17:27 i cannot kick you, i didn't get the pun 01:17:42 oerjan: cock-tease + Coq 01:17:44 element { 01:17:44 0 <= index < size 01:17:44 data 01:17:44 } 01:17:44 (0 <= index < size) => exists(element e | e.index == index) 01:17:45 nddrylliog: rephrase: 01:17:48 element { data } 01:18:13 (0 <= index < size) <=> isElementAt(array, index) 01:18:14 or something 01:18:16 * oerjan wasn't aware of that word 01:18:35 elliott: right but how do you define isElementAt ? 01:18:36 "So, what can our language do?" <-- absolutely nothing, you haven't specified any computation mechanism >:D 01:18:59 bbbahh at this point it can check for things 01:19:03 nddrylliog: well here's an abstract array structure in Coq 01:19:20 also, having a good person inside is no excuse, that's true even for cannibals! 01:19:33 Record Array (elemType:Set) := mkArray { size : nat; get : forall index:nat, (index < size) -> elemType } 01:19:51 nddrylliog: where get is initialised by the run-time system and such 01:19:54 i.e. this is just abstract 01:20:09 yeah but. you're missing the "consecutive" element part. 01:20:16 nddrylliog: howso 01:20:39 grr this is the only point I wanted to get across in these slides and I failed 01:20:44 the point is 01:20:46 :))) 01:20:48 you're not describing an array 01:20:52 you're describing any kind of list-like structure 01:21:02 I, on the other hand, I'm describing a specific implementation of a kind of list-like structure 01:21:03 nddrylliog: sure... but that's just a stupid low-level detail :D 01:21:09 no it's not 01:21:11 that's my point 01:21:13 OH YES IT IS 01:21:14 cache 01:21:19 ^ cache cache cache cache 01:21:22 another stupid low-level detail, like CPUs and the universe 01:21:25 victim cache - if anyone ever does that in hardware 01:21:27 and existence 01:21:29 TLBs 01:21:33 hit, misses, lines 01:21:34 (of coke) 01:21:42 nddrylliog: i'm sorry, all I can see is "DETAIL DETAIL DETAIL" 01:21:47 nddrylliog: more seriously, you might want to look at Frama-C 01:21:58 nddrylliog: it's a theorem-proving system for C code 01:22:04 nddrylliog: that uses Coq as a backend 01:22:21 (I realise it's not what you want, but you could perhaps compile your language to this.) 01:22:24 (Or even just get ideas from it.) 01:22:28 right, right 01:22:32 anything that looks like it interests me 01:22:47 but yeah, this idea is pretty much all about the details 01:22:53 that makes a program run fast, you know. 01:23:05 correctness and conciseness are just two nice side effects :) 01:23:23 nddrylliog: "In the following code, # means belong to and something' means the future version of something" <-- go purely functional, simply return a new array satisfying an additional condition 01:23:35 nddrylliog: this will make your language's semantics a _lot_ simpler and allow for easier implementation 01:23:49 nddrylliog: (without significantly reducing performance -- in most cases, it is easy to turn this into mutation at the compiler level) 01:23:54 nddrylliog: (after you verify correctness) 01:23:59 that's... what I'm doing 01:24:03 where are you seeing any modification? 01:24:16 well 01:24:23 well hmmph actually it's a bit unclear, I agree. 01:24:45 but mhm yeah I can go purely functional. 01:25:21 nddrylliog: well 01:25:27 array.insert (index i, data d) => 01:25:27 (element e | e.data == d, e.index == i) # arra 01:25:30 nddrylliog: I would rephrase this as. 01:26:00 nddrylliog: erm 01:26:04 nddrylliog: dude, your element e thing is broken 01:26:08 because it doesn't specify what array it refers to 01:26:09 :) 01:26:23 nddrylliog: it should be (exists e : element theArray | ...) 01:26:26 i.e. taking the array as a type parameter 01:26:47 here's how i would phrase it: array.insert(index i, data d) == array' => exists (e : element array' | e.index == array.size && e.data = d) 01:27:55 "The compiler can detect edge cases itself, and optimize for them." 01:28:00 beware the sufficiently-smart compiler argument 01:28:10 yeah I know, I know 01:28:20 your language seems nice, but so far, you haven't provided ANY concrete details as to how any of this could be implemented :) 01:28:29 but it seems so simple from here, and we could help it for complex cases 01:28:46 yeah I know but you should know how my brain works - I have ideas how to implement that. I'm being practical 01:28:47 as someone who's looked a lot at formal verification of software 01:28:51 THIS IS NOT SIMPLE AT ALL :) 01:28:52 and 01:28:56 even these simple examples you give 01:28:57 yeah it's not :) 01:29:09 nddrylliog: well let's put it this way i think your language would advance the state of the art about 20 years. 01:29:13 but hmm your version of insert is 1) much longer 2) I don't see what's wrong with my 'element e' 01:29:26 when you first define it, it doesn't belong anywhere... yet 01:29:35 nddrylliog: by version is much longer but much more precise and purely functional 01:29:45 nddrylliog: also, exists (element e | e.index == n && e.data = d) is true by definition 01:29:48 you can construct such an element structure 01:29:55 nddrylliog: the point is that you've just said it exists, not where it is 01:29:55 uhh 01:29:58 so "e: element array'" replaces the '#' notation 01:30:01 basically that statement is logically nonsense. 01:30:03 nddrylliog: no it doesn't 01:30:05 well 01:30:05 yes 01:30:08 your # notation makes no sense :) 01:30:11 at all 01:30:12 yeah 01:30:20 when I wrote that, I knew it would be a nightmare to implement 01:30:22 well it does intuitively, but not from a logic point of view at all 01:30:36 and it would also hold you back a bit i think as far as what propositions you could construct 01:30:57 nddrylliog: my insert is also longer because i removed the "future value" stuff and replaced it with a saner functional approach :) 01:31:10 nddrylliog: you may want to rephrase the whole thing as array.insert's type signature returning a certificate 01:31:21 basically return a tuple of (array', proof of the proposition on array') 01:31:38 (you can have language support for ignoring the proof but absorbing it into the "environment" to make actually using the function easier) 01:33:03 hmm 01:33:10 what do you mean make using the function easier? 01:33:39 -!- azaq23 has quit (Ping timeout: 240 seconds). 01:33:40 nddrylliog: as in, without having to explicitly say "first_tuple_element result" 01:34:02 you could e.g. say that %x takes the first element of tuple x, but remembers the second one for the proof system 01:34:07 then you could do, like 01:34:16 (%array.insert(42))[0] 01:34:21 nddrylliog: oh and my insert was actually an append i just realised 01:34:25 which is why it was different to yours 01:35:14 oh yeah, that too 01:35:21 but we can do e.index == i, no big deal 01:35:30 but hum why the [0] ? 01:36:16 nddrylliog: just an example 01:36:24 nddrylliog: also just saying e.index == i isn't really enough 01:36:35 nddrylliog: you'd want to also demonstrate that every element at i and after in the original array is at i+1 01:36:39 to make managing things easier 01:37:45 well the thing is 01:38:09 since we have (e1, e2: element array) => (e1.index != e2.index) 01:38:15 there's a conflict 01:38:23 no there isn't 01:38:24 so either the compiler would say that insert is invalid 01:38:33 how is there a conflict? 01:38:41 either it would figure out that the only way to do it is to move all the elements on the right of it 01:38:43 *of i 01:38:50 because then we'd have two elements with index i 01:38:58 no we would no 01:38:59 t 01:39:02 here's how i would write insert's type signature, Coq-style (since Coq is less ambiguous ... :)) 01:39:23 sure 01:40:22 insert : forall (array : Array), forall (i : Index array), ElementType -> (Sigma (array' : Array), (forall (j : Index array), j < i -> ... bleh 01:40:30 oh btw, "i think your language would advance the state of the art about 20 years." => yes, I figure that it's better to work on such a language even if it's not an easy problem, rather than try to re-implement Java/C# done right (ie. ooc) 01:40:46 nddrylliog: i think using any kind of non-opaque integer for index types is a bad idea. 01:40:54 because the propositions get really gnarly :) 01:41:18 nddrylliog: have an opaque index type or something 01:42:47 opaque? 01:42:57 the only opaque I know is C-struct-opaque and I don't see how it applies 01:43:10 nddrylliog: I mean exactly that. as in, you don't know that an (Index array) is a number. 01:43:31 ah. 01:43:33 well why not 01:43:36 it doesn't change much 01:43:42 as long as it's comparable 01:44:48 then you could even implement a hashtable on top of that dynamic array, haha :) 01:46:13 nddrylliog: it does change much 01:46:21 because it lets your propositions be less ugly :P 01:46:32 how so? 01:46:39 well see my line of coq above. it got ugly. 01:46:51 nddrylliog: and the nice thing is you'd need no < relations or whatever. 01:46:58 (Index array) is always addressable, no exceptions. 01:46:59 or whatever. 01:47:09 and also, you know, maybe the compiler will think of a better representation of indices for your very specific type of data, because it has to be a genius already :) 01:47:17 oh right 01:47:28 (note: I'm interested in your ideas, don't take my mocking seriously :P) 01:47:43 256-elements array = use chars for indices \o/ (on an 8-bit processor, obviously - otherwise we're losing the perf. improvement) 01:47:43 | 01:47:43 >\ 01:48:01 elliott: I don't take it seriously :) it's very constructive so far 01:48:11 elliott: from what I can see, Coq quickly gets clumsy.. probably because it works 01:48:28 nddrylliog: oh Coq isn't a party. but yes, it works. frama-c seems nice enough. coq is a good backend at least :P 01:49:01 elliott: let's talk about your element { data } part 01:49:05 elliott: why rewrite it that way? 01:49:07 nddrylliog: the thing is that Coq was designed by taking a core, simple logic to ensure correctness, and then the rest was built on top of that 01:49:16 rather than starting with convenience and ending with a mess like a lot of people :P 01:49:19 elliott: somehow it bothers me to 'declare' index inside element, because it somehow makes me think the compiler will store it 01:49:22 nddrylliog: well i don't think your element structure even makes much sense. 01:49:39 but.. not so much because from all the constraints it can be deduced that it's unnecessary to store it 01:49:41 elements aren't "real", there are just valid indices that you can access. 01:49:48 really you want an index type. 01:50:10 which could even be defined to be index array := n | 0 <= n < size array. 01:50:25 -!- pikhq has quit (Ping timeout: 255 seconds). 01:51:33 well we have to be able to express that elements belong to the array and that they have a data.. and they definitely all have an index associated 01:51:48 I'd have trouble defining the 'get' operation without element.index :) 01:52:01 nddrylliog: no you wouldn't 01:52:10 get : (array:Array) -> Index array -> ElementType 01:52:19 (assuming all arrays have the same type of element for simplicity) 01:52:20 nddrylliog: see? 01:52:45 nddrylliog: then you can prove that "forall idx:(Index array), exists (e:ElementType), get array idx == e" 01:52:49 because that's just a direct restatement of the function 01:52:49 s/defining/implementing 01:52:56 well this would be easier to implement. :p 01:53:00 probably. 01:53:13 easier to make a compiler for it, or easier to implement get in that language? 01:53:13 you'd likely have to actually implement arrays at some level... but then your genius layer takes care of that :) 01:53:23 I'm still not seeing your implementation of get, only the function's signature 01:53:59 the point is, my (horrible, sketchy, ambiguous, not purely functional, unimplementable) language does away with that array primitive 01:54:07 there is no implementation there. 01:54:16 nddrylliog: no, in your language _everything_ is a primitive. 01:54:17 yep 01:54:18 pretty much. 01:54:21 haha 01:54:24 what do you mean? 01:54:28 nddrylliog: ok, well let's put it this way 01:54:37 nddrylliog: let's imagine a proposition IsArray T, where T is a type. 01:55:11 yep 01:55:38 nddrylliog: IsArray Ary := exists (Index : Ary -> Type | exists (get : Ary -> Index Ary -> ElemType)) 01:55:42 (ignoring the consecutive things FOR NOW) 01:55:54 nddrylliog: then your language pretty much takes IsArray and comes up with a type that fits. 01:56:01 ofc you'd likely want to specify how index behaves more. 01:56:08 but whatever 01:57:58 nah nah nah don't "whatever" me - speak your mind 01:59:05 nddrylliog: no no no that was me speaking my mind 01:59:06 -!- pikhq has joined. 01:59:18 "but whatever" was just me breaking out of the train of thought as it became too complicated :) 01:59:25 right 01:59:34 but hu 01:59:36 *hum 01:59:41 embedded 'exists' = my mind hurts 02:00:46 nddrylliog: you may want to become rather proficient with formal logic if you're embarking on this endeavour. :p 02:00:53 Recursive call to slow_fib has principal argument equal to 02:00:53 "S n1" 02:00:53 instead of one of the following variables: n0 n1. 02:00:54 oh fuck you. 02:00:58 fuckity fuckity fuck 02:01:35 hahahahha 02:01:47 I think I have something simpler in mind :) 02:01:52 I'm going to try to implement it. 02:01:56 not necessarily right now, though 02:02:02 nddrylliog: what simpler thing? 02:02:45 Toplevel input, characters 142-154: 02:02:45 Error: This clause is redundant. 02:02:46 you're redundant. 02:03:11 haha :D. This is Coq's error messages? 02:03:20 Fixpoint fibonacci (n:nat) : Z := 02:03:20 match n with 02:03:21 | O => 1 02:03:21 | S O => 1 02:03:21 | S (S n as p) => fibonacci p + fibonacci n 02:03:21 end. 02:03:23 aha 02:03:25 i can do it like that 02:03:27 nddrylliog: yeah :) 02:03:33 recursive functions in Coq have to be written... anally 02:03:37 since it has to ensure termination 02:03:58 oooooooouch. 02:04:03 I have made TeX to read its own output. 02:04:15 zzo38: what' with you and TeX? 02:04:17 s 02:05:33 it doesn't have that stupid principle argument why do you think i'm writing it like this coq 02:05:36 what have i ever done to you 02:05:50 nddrylliog: What do you think? 02:05:59 -!- BeholdMyGlory has quit (Remote host closed the connection). 02:06:22 zzo38: dunno, maybe some child abuse story 02:06:29 nddrylliog: No. 02:06:52 -!- Slereah has joined. 02:07:14 zzo38: okay, I was messing with you. But making TeX do all sorts of weird stuff sounds extremely cool. Really. 02:07:30 nddrylliog: he's done underload in tex 02:07:34 which kinda puts yours to shame :P 02:07:38 yup, I remember :) 02:07:40 haha, totally 02:07:47 oh and mine doesn't work on all examples, too 02:08:16 zzo38: isn't your current project a magic the gathering card generator based on TeX that's written in an underload-like language implemented in tex? i forget how texnicard is structured exactly 02:09:04 elliott: Something like that. It is not specific to Magic: the Gathering, and it uses TeX and METAFONT, but the main program is a C program (using Enhanced CWEB), it has a built-in programming language something like Underload (although more like dc than like Underload). 02:09:46 nddrylliog: sometimes Coq's error messages are even better: "Anomaly: uncaught exception Not_found. Please report." 02:09:54 (ok so the Program system is experimental.) 02:10:54 I should learn Coq. And Standard ML. And Erlang. And Esperanto. 02:11:16 Sgeo: aaaaaaaand lojban. 02:11:40 I love some Lojban words, like their "we"s. English should import those wes 02:12:17 (TeXnicard is less specific to Magic: the Gathering than Magic Set Editor) 02:13:18 nddrylliog: (match Fib0 return Fib n 0 with x => x end) 02:13:20 FUCK YEAH COQ 02:13:27 looks like i have to prove that 0 = 0 02:13:34 elliott: ooooh. kinky 02:13:58 elliott: "prove me, baby. prove me good" 02:14:02 hm wait i thought dependent pattern matching was meant to solve problems like this :D 02:14:05 now how do you use it again... 02:17:01 lol it still doesn't work 02:17:56 elliott: you're more or less scaring my ass off Coq :) 02:18:04 nddrylliog: oh i'm actually just pretty stupid 02:18:18 elliott: not a relief - not what it looks like 02:18:23 but coq is a great way to prove to yourself that you're stupid in general 02:18:41 nddrylliog: well i may be giving you the misleading impression that i'm actually any good at Coq at all, which I am not 02:19:54 wat da fak 02:19:56 oh 02:20:00 elliott: oh I do smell the faint odor of someone trying to pretend he knows more than he does - but it's not bothering me :) 02:20:24 I'm doing it all the time anyway 02:20:36 Of course Sensei's Library uses custom wiki software. Why wouldn't it? 02:20:39 * Sgeo facepalms 02:20:51 Oh, it's based on PhpWiki 02:21:12 nddrylliog: oh i make no pretensions about knowing what i'm doing 02:21:21 "The source could (if at all) only be published on alt.tasteless.jokes." 02:21:25 nddrylliog: i just know that a lot of things REALLY DON'T WORK, mostly because i tired them 02:21:53 http://bpaste.net/show/13336/ 02:21:58 ^ that looks pretty compilable to me. 02:22:05 Toplevel input, characters 1068-1072: 02:22:05 Error: 02:22:05 In environment 02:22:05 slow_fib : forall n : nat, Sigma nat (Fib n) 02:22:05 n : nat 02:22:08 The term "Fib0" has type "Fib 0 0" while it is expected to have type 02:22:09 "Fib ?182 02:22:11 match ?183 with 02:22:14 | 0 => 0 02:22:16 | 1 => 1 02:22:17 | S (S n as p) => 02:22:19 match slow_fib n with 02:22:21 | witness fibn _ => 02:22:24 match slow_fib p with 02:22:26 | witness fibp _ => fibn + fibp 02:22:27 end 02:22:29 end 02:22:31 end". 02:22:34 sorry for flooding, actually no i'm not, you all had to see that. 02:22:57 seriously, "witness" is a keyword in Coq? 02:24:03 nddrylliog: no. 02:24:05 that's my constructor. 02:24:30 nddrylliog: don't worry, it doesn't feel so much like an interrogation, as a shouting match 02:25:43 haha, that's the spirit 02:25:48 Recursive definition of slow_fib is ill-formed. 02:25:50 not again. 02:26:05 i know what i'll do. 02:26:11 i'll tell it i'm going to use a termination proposition 02:26:15 and then add it as an axiom 02:26:16 that'll show it! 02:27:42 haha that sounds so dirty 02:29:32 now if you'll EXCUSE me, I'm going to devote 15 minutes of my life to watching two British dolts walk around in a computer game made out of 1 m^3 blocks being confused and doing lots of silly things. 02:29:39 because my time has no value! 02:29:43 at least, not at 3 am. 02:31:10 haha 02:31:23 I'm probably going to die of a haha overload. 02:32:40 hahahahaha 02:34:39 -!- augur has quit (Remote host closed the connection). 02:42:28 elliott: aauughh 02:42:37 :wat: 02:43:51 you've haha'd me to death 02:43:57 seriously, cereals and coma sound good right now. 02:44:09 cheer(io)s o/ 02:44:25 you've turned nddrylliog into a cereal killer! 02:45:41 nddrylliog: and coma? 02:45:50 "I'm going to eat cereal and then ENTER A VEGETATIVE STATE." 02:47:18 oerjan: dammit, that's my CS nick :) 02:47:29 -!- op_y_mous has quit (Quit: Quitte). 02:47:32 elliott: and ya, I can't really call that sleep, when I just pass out 02:47:35 ah yes, the famed computer science codenames 02:47:39 /nick TheCoqinator 02:48:20 one would think that to be rather coqy. 02:48:57 -!- asdf__ has quit (Quit: Leaving). 03:10:24 -!- nddrylliog has quit (Quit: Page closed). 03:17:08 The term "prfp" has type "(fun H : nat => Fib ?119 ?120) n2" 03:17:08 while it is expected to have type "Fib (S ?119) ?118". 03:17:47 -!- augur has joined. 03:23:52 wat 03:24:07 -!- Slereah has quit (Ping timeout: 240 seconds). 03:24:42 angkor 03:27:38 angkor wut? 03:28:23