01:07 (quit) Quetzalcoatl_: Remote host closed the connection
01:22 (quit) sunnyps: Quit: Ex-Chat
01:23 (quit) j3parker: Ping timeout: 265 seconds
01:23 (quit) bremner: Ping timeout: 260 seconds
01:23 (quit) stamourv: Ping timeout: 265 seconds
01:23 (quit) adadglgmut: Max SendQ exceeded
01:24 (join) j3parker
01:26 (join) adadglgmut
01:29 (join) bremner
01:46 (quit) tewk: *.net *.split
01:53 (join) tewk
04:15 (join) hanDerPeder
04:43 Lajla: emma, how is your training going?
04:55 emma: Lajla: I have yet to dive in very much save the most basic things. I hope after I sleep tonight, which I've not done yet, I'll work through some of the docs.
04:56 Lajla: emma, you slacker, I have already coded a working interpreter for another language in it.
04:56 Lajla: But, if you succeed, will you father my children?
04:56 Lajla: With our superior genes our children will develop awesome powers like a healing factor and a skeleton laced with used iPod parts.
04:57 emma: I'm pretty sure that will be biologically impossible :)
04:58 Lajla: emma, which part of my far-fetched story?
04:58 emma: The part where I'll father your children :P
04:59 Lajla: emma, how do you kbnow that I'm infirtile?
05:00 emma: Are you saying you would father my children then? I'm a little confused :P
05:01 emma: I think the trouble at the root of this is that neither of us have a penix.
05:03 Lajla: emma, no, you mine.
05:03 Lajla: Ahhh
05:03 Lajla: Well, binary cloning and all.
05:03 Lajla: It would explain why you once didn't ban me.
05:03 Lajla: As I always say, women are better leaders, they ban me less namely.
05:03 emma: I wasn't aware I ever had that option.
05:07 Lajla: emma, long time ago at ##not-physics
05:08 emma: I see. Well I'm here to learn about Racket so let's not get so off topic :)
05:09 Lajla: No one's talking about racket anyway, but ask, I might know it.
05:23 (join) sunnyps
06:26 Lajla: emma, come on, ask me.
06:27 Lajla: I feel paedagogical if that's a word.
07:57 (join) dzhus
09:27 (quit) dzhus: Read error: Connection reset by peer
10:16 (join) masm
10:17 (join) jao
11:08 (join) stamourv
11:34 (join) jonrafkind
11:52 (quit) hanDerPeder: Quit: hanDerPeder
12:08 (join) shofetim
12:11 (join) dzhus
12:23 (quit) jao: Ping timeout: 265 seconds
12:25 (quit) sunnyps: Quit: Ex-Chat
12:47 (quit) masm: Quit: Leaving.
12:56 (join) masm
13:14 (join) jao
13:39 (quit) shofetim: Ping timeout: 248 seconds
14:09 (join) hanDerPeder
14:10 (quit) hanDerPeder: Client Quit
14:17 (join) hanDerPeder
14:21 (quit) jonrafkind: Read error: Connection reset by peer
14:22 (join) jonrafkind
14:22 (quit) jonrafkind: Read error: Connection reset by peer
14:23 (join) jonrafkind
14:57 (join) shkk
14:58 (quit) alexsuraci: Remote host closed the connection
14:59 shkk: Hi All, what file extension does PLTScheme store normal scheme programs ?
14:59 shkk: PLTScheme <-> Racket
15:02 jonrafkind: pltscheme = .ss, racket = .rkt
15:02 shkk: thanks jonrafkind
15:03 (quit) shkk: Quit: Page closed
15:06 eli: bremner: The "compiled" directories are almost all platform independent, except for a few C-compiled extensions, which are in a directory that is named after the platform.
15:08 (join) shofetim
15:28 (quit) shofetim: Ping timeout: 260 seconds
15:29 bremner: eli: Thanks for clearing that up. Am I right in thinking there is nothing built in to racket that would look for the architecture dependant bits in a different place than the architecture dependant ones?
15:30 eli: bremner: Yes, but there shouldn't be any problem having those be in /usr/share.
15:31 bremner: Well, it's a debian policy problem, but not typically a technical one I agree
15:35 eli: Yeah, I know that debian is full of policies...  The thing is that the platform name in the directory makes it pefectly fine with sharing.
15:36 bremner: Ack
15:36 (quit) hanDerPeder: Quit: hanDerPeder
15:38 bremner: Could be t-shirt. Debian is full of...policies. :)
15:40 eli: Heh, that would fit in nicely.
15:41 eli: Reminds me of the time I had to contact a few R5RS authors, because Debian insisted that the document is not kosherly free.
16:01 (quit) masm: Quit: Leaving.
16:01 bremner: You'll be glad to know that exchange is preserved for posterity in debian/copyright
16:06 bremner: huh, I found only two directories with x86_64-linux in my racket install. That is pretty managable, if correct.
16:21 (join) shofetim
16:21 (nick) samth_away -> samth
16:22 samth: bremner, there are indeed only a couple of bits of c code in the standard distribution
16:33 (quit) shofetim: Read error: Connection reset by peer
16:38 (join) Wikian11
16:39 Wikian11: Heya
16:39 Wikian11: Im learning Racket, and noticed that the quick  tutorial brings up an error
16:39 samth: which part of it?
16:39 Wikian11: running "#lang slideshow" brings up an error
16:39 samth: what is the error?
16:40 Wikian11: module: name is not defined, not a parameter, and not a primitive name
16:40 samth: i think you need to change the language that drracket is set to
16:40 samth: did you choose a language called "beginning student"?
16:40 Wikian11: Its on.."Beginning student"
16:40 Wikian11: Yes
16:41 samth: you need to go to "choose language" in the language menu, and choose "use the language declared in the source"
16:41 Wikian11: okay.
16:41 Wikian11: thanks
16:42 jonrafkind: probably beginning student should have a check for that
16:42 samth: yes, it should
16:42 Wikian11: Im new to programming, so i figured that would be the best choice..
16:43 jonrafkind: you could go through htdp with the beginning student language, I think
16:43 samth: if you're entirely new to programming, i recommend the textbook how to design programs
16:43 samth: which is available free at htdp.org
16:45 Wikian11: samth - the regular text, or the racket version?
16:45 samth: there is no racket version of htdp.org yet
16:46 Wikian11: Oh
16:46 chandler: Why on *earth* isn't the "use the language declared in the source" language the default? I still don't get that.
16:46 Wikian11: The regular or drscheme version then?
16:46 samth: Wikian11, there is only one version of how to design programs
16:47 Wikian11: http://htdp.org/2003-09-26/Book/curriculum-Z-H-4.html
16:47 Wikian11: then whats all the drscheme stuff for
16:47 Wikian11: when you click the logo
16:48 samth: chandler, b/c students often get/got confused when they get dropped into a full-fledged language and their textbook doesn't work
16:48 Wikian11: What do you mean, samth?
16:48 samth: Wikian11, those are instructions for how to use DrScheme (now called DrRacket) with the text book
16:48 Wikian11: Oh
16:48 Wikian11: Should i read it, then the text book, or skip it?
16:48 chandler: samth: I think we just saw an example of how the current policy causes confusion anyway.
16:49 samth: chandler, i agree, and the plan is to eventually switch everything to using #lang
16:49 samth: Wikian11, i recommend starting with the textbook, and ignoring the companion unless you need it
16:50 Wikian11: Samth - okay
16:50 Wikian11: Samth - are you a racket developer?
16:50 samth: Wikian11, yes
16:51 Wikian11: Samth - cool
16:58 Wikian11: Was it your first language?
17:01 samth: Wikian11, no
17:01 Wikian11: What was? BASIC?
17:01 samth: TI calculator basic, then pascal, then scheme
17:02 Wikian11: Cool
17:03 (join) masm
17:24 (quit) Wikian11: Quit: ChatZilla 0.9.86 [Firefox 3.6.6/20100625231939]
17:25 (quit) dzhus: Ping timeout: 248 seconds
17:30 (quit) jonrafkind: Ping timeout: 240 seconds
17:36 emma: Hey guys -- A friend of mine is concerned that raket is two times slower than sbcl even though it is a simpler language and should be easier to make go fast. I'd like anyone here to comment on that so I can have a good answer for him.
17:37 samth: racket is not simpler than sbcl
17:37 samth: at least not in the sense that allows it to go faster
17:38 Lajla: emma, faster with what?
17:38 Lajla: Numbers, nondeterministic programming, databases?
17:39 chandler: emma: Your friend is (frankly speaking) full of it.
17:40 emma: chandler: That won't be a compelling answer. :) Could you flesh that out assuming he's a very reasonable and highly intelligent person (becuase he is). :)
17:41 chandler: As samth said, Racket is not a "simpler" language than Common Lisp in any sense related to efficiency.
17:41 samth: http://shootout.alioth.debian.org/u32/benchmark.php?test=all&lang=sbcl&lang2=racket
17:42 chandler: In fact, the higher-order control flow operators offered by Racket add an additional challenge for optimization.
17:42 chandler: The shootout is a horrible, awful, incredibly terrible benchmark. I wouldn't look to it for guidance on anything.
17:43 Lajla: emma, well, that's numbers.
17:43 Lajla: I do believe that CL is faster with numbers due to some type declaration stuff.
17:44 samth: chandler, my point is just that dumb microbenchmarks show that racket vs SBCL is a push
17:45 chandler: samth: Those aren't "dumb microbenchmarks". One wouldn't ordinarily write the pidigits program by concocting a new binding to GMP, and if you wrote the program that way in SBCL you'd get effectively identical results.
17:45 chandler: It's a comparison of completely different programs that purport to do the same thing, and it's of no value at all.
17:45 stamourv: Lajla: we're getting there with Typed Racket
17:46 Lajla: stamourv, typed racker I never really understood, it's not complete static typing a la Java or C, right?
17:46 Lajla: That would take out apply methinks
17:46 chandler: Why?
17:46 stamourv: Lajla: you
17:46 stamourv: 're right, it's not like C or java
17:46 Lajla: Because you can't at compile time ferify the contents of apply.
17:47 stamourv: no, but there's still some things you can do
17:47 chandler: You can verify the type of its arguments.
17:47 Lajla: stamourv, well, a compiler at compile can't decide, it can only prove, it can either prove it's not going to have type errors, or prove that it's going to have them, Java and C have 1, my guess is that Racket has 2?
17:48 Lajla: chandler, how would (apply f (cons + (cons - (list 1 2 3)))) analogues pay out?
17:48 stamourv: Typed Racket proves that you won't get type errors
17:48 chandler: I think your statement about Java and C is *very*, very wrong.
17:48 Lajla: stamourv, then how does apply work?
17:50 emma: I passed along the best responses I got here and I think he seems to agree that those benchmarks don't mean very much in isolation.
17:50 chandler: http://docs.racket-lang.org/ts-guide/types.html#%28part._varargs%29
17:51 stamourv: Lajla: it's restricted compared to racket's apply
17:51 stamourv: but in practice, it doesn't usually matter
17:52 Lajla: stamourv, well, that's what I gathered because there isn't really a way around it.
17:52 bremner: about the earlier discussion about architecture dependent bits, there is also  /usr/lib/racket/mzdyn3m.o
17:52 Lajla: The link seems to imply that (apply f (cons + (cons - (list 1 2 3)))) is not really possible no.
17:53 Lajla: chandler, c'est treux, in C and Java the compiler rejects all code of which it can't prove it's not going to have type errors.
17:54 chandler: What? Both C and Java compilers accept code that has type errors.
17:55 chandler: They reject code that can be proven to have type errors, but they can't reject all programs that contain type errors.
17:55 bremner: well, C has a very generous notion of correctly typed.
17:55 chandler: C is an untyped language anyway.
17:55 chandler: (Essentially.)
17:55 chandler: Java most definitely does *not* reject type errors, and it is easily possible to cause a type error at runtime.
17:55 chandler: Er, reject all programs containig type errors.
17:55 Lajla: chandler, example?
17:57 chandler: Anything which casts java.lang.Object to some other type.
17:57 Lajla: And C is hardly 'untyped', it simply has machine-types, not 'human-types'.
17:58 Lajla: chandler, more concrete example please.
17:58 chandler: If you don't get it from that, then you don't understand Java and you should take my word for it. Otherwise, start from a Java tutorial.
17:58 bremner: Lajla: consider old style vectors in Java
17:59 Lajla: chandler, or maybe you, I think your notion of 'type error' might be a bit unorthodox.
17:59 bremner: i.e. vectors of Object
17:59 Lajla: bremner, go on.
17:59 bremner: that's it. Thats the whole example. It is equivalent to an array of (void*) pointers in C
18:00 chandler: Lajla: It's not unorthodox at all.
18:00 bremner: (with better run time checking)
18:00 Lajla: bremner, and those can't cause type errors, they can cause segfaults.
18:00 chandler: Er, what do you think that segfault is indicative of?
18:00 Lajla: chandler, as I said, your idea of 'type error', might be a bit unorthodox.
18:01 Lajla: A segmentation is hardly a type error.
18:01 Lajla: A type error is simply matching an operation with operants of a type it's not defined on.
18:01 chandler: Where did this definition come from?
18:02 chandler: Which literature on type systems are you referring to in particular?
18:02 Lajla: chandler, well, give me yours.
18:02 Lajla: chandler, about any book on type theory really.
18:03 Lajla: Though, more formally, the word 'defined' should be avoided I give you, it's the matching of operations with operants that are either not explicitly allowed, or explicitly dissalowed depending if your type system is constructive or deconstructive.
18:03 chandler: A type system that allows casts to and from (void*) is a type system that accepts anything. It's pointless.
18:04 bremner: well,  you can't cast floating point numbers to pointers, there are some rules :)
18:05 Lajla: The 'type' of a pointer says little more than the breadth of the bit vector it dereferences in C really.
18:05 Lajla: It's largely to enable pointer arithmetic -> ad hoc array indexing.
18:07 chandler: Not just that. It also conveys information about alignment and, in some implementations, memory region.
18:10 chandler: Anyway, if you're willing to accept a "basically anything could happen" semantics, any compileable C program could be said to be type-correct. I'm not sure this is in any way useful. Dereference of an incorrectly-assigned pointer (for instance) is a clear indication of a type error in a program.
18:10 Lajla: That follows from the breadth of the vector though.
18:10 Lajla: Well, that's not so much a 'type error' as a segmentation fault.
18:10 bremner: so, ah, before we got into this discussion about terminology, I think perhaps the point might have been that (other than typed scheme) scheme is dynamically typed, in that types attach to objects rather than variables.
18:11 bremner: whereas java and C, to the extent that they are typed, are statically typed
18:11 chandler: The type theoreticians call that "untyped", which is also what I accused C and Java of being.
18:11 Lajla: bremner, that is the 'naïve definition of the destinction between dynamic and static typing' you come across often and should be avoided accordingly 'some' [who?] sources
18:11 Lajla: chandler, quite so.
18:12 bremner: Lajla: [citation needed]
18:12 Lajla: Dynamic typing from a formal perspective is untyped,  (vector-ref list char) just has a side effect of printing "erorr: blablabal" just as (display "Hello, World!") has a side effect.
18:12 Lajla: bremner, sure, hold on.
18:12 bremner: nah, don't bother
18:13 bremner: well, if your formalism can't distinguished between tagged and untagged languages, I'm not buying it :)
18:15 Lajla: http://www.pphsg.org/cdsmith/types.html
18:16 Lajla: bremner, well, the point is that in 'dynamic typing' the difference really is nothing different than let's say the first index of an array.
18:16 Lajla: I can write in C too a function that consumes an array, checks its first index, if it's first index is not a 'c' it quits with an error code.
18:16 Lajla: Or possibly doesn't even quite but simply uses printf to write "type error: 3738 your first character must be a 'c'"
18:17 Lajla: 'dynamically typed' langauges are just statically typed languages with one type really.
18:17 Lajla: This is why the different ideas needn't even be mutually exclusive.
18:19 Lajla: But bremner let me put it like this, you would agree that Haskell is statically typed surely? But in Haskell, you can't change the value of a variable, therefore, a variable and its value are necessarily the same, but still it's statically typed and not dynamically typd.
18:22 chandler: You've confused me drastically
18:22 chandler: er, +.
18:23 samth: chandler, i think you're unfair to Java here
18:23 Lajla seems to have that effect on people.
18:24 chandler: Lajla: I've noticed.
18:24 Lajla has a 'formal thought disorder', which basically means 'it takes 3-odd weeks before people stop being confused'
18:25 samth: Java is a statically typed and safe language
18:25 samth: C has an unsound type system
18:26 samth: Racket is untyped (except Typed Racket)
18:28 Lajla: samth, well, type error or not is tangent to safety.
18:28 (join) hanDerPeder
18:28 samth: Lajla, no, it really isn't
18:28 Lajla: In fact, the unsafety of C more or less comes down to that all that undesired behaviour is not classed as a type error by the type system.
18:29 samth: if your language is unsafe, then it almost certainly does not have a sound type system
18:29 Lajla: samth, 'sound' is to the eye of the beholder.
18:29 samth: no, that is also not true
18:29 Lajla: And it still does not imply a 'type error'.
18:29 Lajla: samth, well, the decision to make C like that was a conscious choice.
18:29 samth: soundness is a property of type systems
18:30 samth: certainly it was a concious choice
18:30 samth: but it was a choice to have an unsafe language with an unsound type system
18:30 Lajla: I'm pretty sure that 'unsound' is not a formal property here.
18:31 samth: no, it is certainly a formal property
18:31 Lajla: samth, define it.
18:31 samth: unsound means that if you have an expression of type T, and the expression evaluates to some value, then that value is of type T
18:32 samth: C does not have this property
18:32 chandler: That's what "sound" means, right?
18:32 Lajla: samth, you mean sound?
18:32 samth: right, sorry
18:32 Lajla: samth, you basically mean 'for any expression of type T, its evaluation is of type T'?
18:33 samth: in any non-trivial language, expressions of type T may produce dynamic errors, or they may fail to terminate
18:33 Lajla: Sure
18:33 samth: soundness is that they produce only values of the correct type, or a predetermined sort of error
18:33 Lajla: but that definition is particularly easy to escape from by just defining a type that is the union of T and whatever it evaluates to.
18:34 Lajla: As in, it depends on your definition of our 'T' here.
18:34 samth: but that isn't what the C typechecker does
18:34 samth: soundness means that if the C typechecker says something, we can believe it
18:34 samth: but that isn't the case
18:35 samth: we could design a different, sound, type system for C, that would say very different things
18:35 samth: but that wouldn't be the C type system
18:35 Lajla: Maybe not, but I could just interpreted the C typesystem as having all types simply enote the breadth of the bit vector and nothing more and then have it sound type system by a different interpretation.
18:35 Lajla: by just a different interpretation*
18:35 samth: but that isn't what the C type system computes
18:35 Lajla: Also, 'the type checker' is hardly a formal idea.
18:36 Lajla: samth, and as soon as you make that argument you've crossed the line of formality.
18:36 samth: Lajla, the C spec has rules about what produces a type error
18:36 Lajla: samth, how the C spec calls things is irrelevant for formal proves about it.
18:36 Lajla: proofs*
18:36 samth: you can make up different rules, but they aren't the rules of the C type system
18:36 samth: no, it is totally relevant
18:36 Lajla: It's about what it can ultimately be proven to be isomorphic with.
18:37 Lajla: samth, then I'm afraid your idea of 'formalism' is unorthodox.
18:37 chandler: samth: Yes, I was being deliberately unfair to Java, mostly driven by frustration with code full of messy casts that I've had the misfortune of working on in the past.
18:37 samth: the C type rules are not isomorphic to a sound type system, either
18:37 samth: chandler, deliberate unfairness is fine :)
18:37 Lajla: samth, but we just established that it was by just a different interpretation of it.
18:38 samth: no, that isn't what we did at all
18:38 Lajla: Without changing any of C's behaviour.
18:38 samth: you described a different type system
18:38 Lajla: samth, and one that rejects and approves the same programs.
18:38 Lajla: In the same code.
18:38 samth: not all type systems for the same dynamic semantics are isomorphic
18:38 Lajla: All that's relevant is that it partition the set of rejected and approved programs in the same way.
18:39 samth: what soundness theorem does your type system satisfy?
18:39 Lajla: Are you suuure you're not speaking of the soundness of formal systems?
18:39 samth: when I have a value of type (char*)(void)
18:39 samth: what do i know about it?
18:40 samth: i certainly don't know that it's a function
18:41 Lajla is confused, justice is served
18:41 Lajla: I don't see how the informal idea of 'what do I know about it?' has to do with its type.
18:42 samth: what formal properties do i know about values that inhabit that type?
18:42 samth: what values inhabit that type?
18:42 Lajla: As far as I know, the 'type unsafeness' of C just means that its type systems can lead to behaviour which is undesriable for human beings, that doesn't mean that there's formally anything strange about them.
18:43 Lajla: samth, that quaestion is quite vague.
18:43 samth: yes, but that's because you do not know far enough in this instance
18:43 Lajla: Rather, ask me to partition.
18:43 samth: no, that question is quite precise
18:43 samth: describe the values that inhabit that type
18:43 Lajla: samth, I am not convinced the set of 'formal properties' that that expression has is finite.
18:43 samth: certainly
18:44 Lajla: In any case, it will be large and I'm not going to list them all.
18:44 samth: but you can describe the set of values that inhabit that type - what properties do they share?
18:44 samth: are they just random?
18:44 Lajla: Delimit your domain of discourse.
18:44 Lajla: Ahhh, in that way.
18:44 samth: if so, how do you know that C produces them?
18:45 Lajla: Well, I get what you mean but the idea of a cast is that the expression does not have that type.
18:45 Lajla: A cast in theory is a function.
18:45 Lajla: That can simply fail like any other function because it's input is strange.
18:45 Lajla: As in, it's a function bit vector -> char
18:45 samth: i don't know what "theory" you are referring to
18:46 samth: but the C semantics gives a meaning to casts
18:46 samth: that is not what you are describing
18:46 Lajla: samth, but behind all that it comes down to a function bit vector -> char, surely?
18:47 samth: what do chars have to do with anything?
18:47 Lajla: What not?
18:48 samth: why would casts be functions that produce characters?
18:48 samth: first, casts are usually the identity function at runtime
18:48 Lajla: samth, no, in this specific case.
18:48 samth: second, the cases when they are not do not involve chars
18:48 Lajla: Produce a value of type char.
18:49 samth: i don't have any idea what you're talking about
18:50 Lajla: http://www.google.com/search?hl=en&q=soundness+of+type+system which one should I pick?
18:51 samth: i recommend "a syntactic approach to type soundness"
18:54 Lajla: samth, well, found it, but let me ask you this, do you believe in 'runtime type errors'?
18:54 samth: but really i recommend this: http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/
18:55 samth: what do you mean, do i believe in them?
18:55 Lajla: samth, that they exist
18:55 Lajla: or rather, can you formalized them, or do you believe they can be formalized.
18:55 samth: what do you mean by 'runtime type errors'?
18:56 samth: I believe that I get an error from evaluating this: (+ 'foo 'bar)
18:56 samth: and that that error can be ruled out by some type systems
18:56 samth: and that other type systems do not rule out that error
18:56 Lajla: samth, yes, but can you formalize the difference between an error and a side effect of writing to the standard output?
18:56 samth: yes
18:56 samth: it's very easy
18:56 Lajla: samth, how?
18:57 samth: i recommend any book that shows formal semantics of programming languages
18:57 samth: they will almost all show examples of errors
18:57 Lajla: samth, well, to be honest, this is the part where I'm starting to become sceptical.
18:57 samth: skeptical of what?
18:58 samth: the book i pointed at has a whole chapter on type soundness, i recommend it
18:58 Lajla: Of your idea, as far as I know, there is no real difference, runtime type errors as far as I know do not exist formally.
18:59 samth: why don't they exist formally?
18:59 Lajla: samth, maybe, but if it defines them at hand of runtime type errors then I'm sceptical.
18:59 samth: one of the nice things about formalism is that you can model whatever you want
18:59 Lajla: Well, because they are formally the same as simply print("string");
18:59 samth: no, they aren't
18:59 Lajla: It's a function that takes an argument, and possibly has a side-effect depending on that argument's value.
18:59 samth: that's one semantics of them
18:59 samth: another would be to raise an exception
19:00 Lajla: Which can be writing "string" to the standard output, or writing "error: arguments do not match" to standard output.
19:00 samth: a third could be to return an error value
19:00 Lajla: samth, well, that can also be done by just a function receiving just a value.
19:00 Lajla: I can make a function that accepts integers as arguments and raises an error code and quits for any nonzero value.
19:00 Lajla: Is that then a type error to that function?
19:01 samth: no, it isn't
19:01 Lajla: Then what is the difference?
19:01 samth: well, rather, it depends on your type system
19:01 samth: a type system determines certain errors that it rules out
19:01 samth: it is sound if it actually rules them out
19:01 Lajla: I am some-what weary of using the term 'type system' to dynamic typing.
19:02 samth: Lajla, you don't appear to know what you are talking about, yet you are repeatedly condescending to people who do
19:02 Lajla: samth, I feel that you are not really aware of what you talk about to be honest. =P
19:03 samth: however, i am the author of multiple published papers in the area of type systems, so i feel quite secure in my knowledge in the area
19:03 Lajla: For one, you used the term 'type system' for dynamic typing which is kind of strange, it's a property of static typing and most people I've spoken to kind of shrivel when people compare the two saying they are completely different and unrelated but just have the same name by intuition
19:03 samth: no, i have not suggested that static typing and dynamic typing are the same
19:03 Lajla: Well maybe I'm wrong, maybe we're using a same word for different things, who knows, but I wouldn't use the word 'type system' for dynamic typing
19:04 Lajla: But let it be, I have to call my ex any-way, but to me some of the things you say sound kind of 'informal' or 'intuitive' perhaps.
19:04 samth: that's because i'm trying to communicate via IRC with people who aren't formally trained in programming languages
19:05 samth: however, i recommend reading the chapter on type soundness in the book i pointed you to
19:10 Lajla: samth, alright, I'll give it a try then if you say so.
19:12 Lajla: But it still strikes me as some-thing which assumes dynamic type errors as a given itself without showing they can be derived from the other axioms/
19:13 samth: i don't know what you mean by dynamic type errors
19:15 Lajla: Ehh, runtime type error*
19:17 samth: i don't know what it would mean to derive errors from axioms
19:19 Lajla: samth, I mean the existence of the category 'runtime type error'
19:20 samth: that's not something that can be derived from any axiom set i know of
19:20 samth: any more than the existence of programs can be derived from axioms
19:27 Lajla: samth, but, what I gather here is that the model classifies some behaviour as a runtime type erro by axiom.
19:27 Lajla: And a type system is sound if it stops this subset of behaviour from occurring?
19:28 (quit) masm: Quit: Leaving.
19:28 samth: i don't think the term "runtime type error" is helpful here
19:29 samth: a type soundness theorem states that a well-typed program produces a value or one of a specific list of errors
19:29 samth: thus ruling out all other errors
19:29 Lajla: Neither do I, that's why I avoid it.
19:30 Lajla: samth, so it's with respect to a specific list?
19:30 samth: yes
19:30 samth: sometimes the list is empty, if there are no possible errors
19:30 samth: but those languages are rarely useful
19:31 Lajla: samth, so, I can for instance introduce printing out "Hello, World!" in my own list, and say that Haskell is not type sound with respect to my own list?
19:31 Lajla: If so, then I understand what you're saying.
19:31 chandler: Gosh, is this discussion still going?
19:31 samth: you can state the conjecture that a well-typed Haskell program never produces an IO action that prints "Hello World"
19:32 samth: that conjecture is false
19:35 Lajla: samth, we said that well-typed was with respect to some list of debehaviour we defined as erronrous right?
19:35 Lajla: So, if we define printing out that as erronous, then with respect to that specific list, Haskell is not well typed, correct?
19:36 Lajla: Or type sound*
19:40 samth: if you claimed that the Haskell type system ruled out such behavior, you would be incorrect
19:41 samth: if you wrote a type system such that values of type IO () couldn't print that, and then they could in the dynamic semantics, that would be unsound
19:41 samth: just claiming that a type system doesn't do X doesn't make it unsound
19:42 samth: as that book chapter mentions, soundness is about the agreement between the runtime and the type system
19:42 samth: as it happens, the haskell type system and runtime agree
20:01 (quit) tcoppi: Ping timeout: 276 seconds
20:18 (quit) hanDerPeder: Quit: hanDerPeder
20:18 (join) tcoppi
20:44 emma: If I find mistakes as I read the racket-lang.org/guide/ should I mention them here or to someone here?
20:47 mattmight: Since no one's replying, I suppose here's good, as long as someone from the Racket team is on.
20:51 chandler: emma: No; it's better to send them to the racket list.
20:53 emma: but even if they are just minor typos?
20:53 emma: I don't want to come across as a pedant or seem difficult. I just plan to read through the whole thing so I'm sure I'll find some typos.
20:54 chandler: I'd suggest batching them into a list in that case.
20:54 chandler: It's useful feedback, so I doubt you'd seem a pedant.
20:54 emma: Okay sure. Thanks!
21:17 eli: emma: If you have a few quick ones I can fix them now.
21:30 (join) JoelMcCracken
21:36 (join) jonrafkind
22:30 (join) sunnyps
22:59 (join) waltermai
23:05 waltermai: hey all, I'm using DrRacket on my old netbook and wanna use it on my new one, a lemote yeeloong. the source won't build and binary installs don't work. I tried to use ... | tee build.txt , but that didn't write the output of make to a file for me. I'm pretty close to giving up and pouting.
23:07 chandler: Ah, now that's an interesting netbook. Where did you find one of those?
23:08 waltermai: a guy named david is reselling them for the fsf
23:08 waltermai: at least I think that's who it's for
23:08 chandler: Ah, right, I read something about that.
23:08 waltermai: it's really cool, but I can't run my new favorite ide on it.
23:08 chandler: I'd be surprised if there was a prebuilt binary on the Racket distribution site that would work on a MIPS machine like that.
23:09 waltermai: ...or any of racket, for that matter. chandler: I tried building from source as well.
23:09 waltermai: something about xsrc/precomp.h
23:09 chandler: Oh, dear. It looks like there's no MIPS build in Debian since 4.2.1.
23:09 chandler: Did that come with gnewsense on it?
23:10 waltermai: sure did, though I reinstalled without gnome.
23:10 jonrafkind: waltermai, can you make a bug report out of your error?
23:10 jonrafkind: most likely it can be fixed
23:10 chandler: There might be a plt-scheme package there, which is an older version.
23:11 waltermai: I've emailed the bug list folks, and they want a file of the make output
23:11 waltermai: which I'm having some trouble getting together. can't get tee to work.
23:11 chandler: try: make >build-log 2>&1
23:11 jonrafkind: can you copy/paste it with the mouse?
23:11 chandler: Somewhere I had a MIPS Lenny image for use with qemu that might be useful for this.
23:11 jonrafkind: you dont really need the whole thing, just the lines around the error
23:12 waltermai: hmm, that's the part I sent to the bug folks, but they wanted the whole thing.
23:12 waltermai: chandler, I'll try that.
23:12 jonrafkind: waltermai, actaulyl try this. type 'script' then build or wahtever, then hit ctrl-d
23:12 chandler: jonrafkind: I think the method I gave is easiest and will work.
23:12 chandler: waltermai: If you want to follow the progress, just open a new terminal and run "tail -f build-log" in that directory.
23:13 waltermai: I think I need to get the source again from git, make won't run twice for some reason. back to you guys in a moment.
23:13 jonrafkind: if you running make from the src/ directory you should do 'mkdir b; cd b; ../configure; make'
23:14 chandler: Often times build logs end with a bunch of logs of make spam, so a copy from the terminal doesn't provide anything useful.
23:14 (quit) stamourv: Remote host closed the connection
23:14 chandler: er, "bunch of lines".
23:14 waltermai: jonrafkind, i used a build directory
23:14 jonrafkind: so then you should be able to rm -rf b; and redo that
23:14 waltermai: okie doke
23:15 waltermai: thanks for your interest, guys
23:16 jonrafkind: you're just lucky this isn't the #c++ channel
23:16 chandler: Ah, and here's the qemu image I had around: http://people.debian.org/~aurel32/qemu/mips/
23:17 waltermai: it seems most irc channels are hostile towards questions from less knowledgeable folks.
23:17 jonrafkind: the internet runs on hate
23:17 chandler: I see less hostility towards that than towards questions from people who are vague, inexpressive, and unhelpful.
23:18 waltermai: chandler, such is the state of having less knowledge, no?
23:19 waltermai: so it's a makin'.
23:20 chandler: Not necessarily. So far you've used as much precision as you could given your knowledge, and you've provided as much information as you have available. Many people don't do that.
23:20 chandler: It's more about a style of communication than it is how much knowledge you happen to have about the subject of your question.
23:20 waltermai: at their own peril, I'd imagine.
23:20 chandler: Indeed!
23:21 waltermai: well, I'm practiced in stupidity. ;)
23:21 chandler: Which makes me suspect that you're actually a smart cookie.
23:21 chandler: I practice my own stupidity regularly.
23:23 waltermai: so drracket is super neat, but so is emacs. I'm quite torn.
23:24 waltermai: just throwin' it out there.
23:24 chandler: Have you seen geiser?
23:24 (quit) JoelMcCracken: Quit: Leaving
23:24 waltermai: I've not been able to get it running properly. I'm an emacs noob too.
23:24 waltermai: and I've only tried it with an uninstalled build of the latest guile.
23:25 waltermai: ...and emacs lisp is the suck, imo.
23:25 waltermai: as far as lisps go.
23:25 chandler: See? You're definitely not stupid.
23:26 chandler: wingo (from #scheme) has been working towards integrating guile into GNU Emacs, actually.
23:26 chandler: This could be promising eventually.
23:26 chandler: In the meantime, you might want to give geiser a try with racket - it is quite nice when it works. :-)
23:27 chandler: DrRacket is nice too, though. I'd use it more, but I really rather like paredit.
23:27 waltermai: I've seen some things to this effect on the guile savannah page. exciting, if it ever happens... drracket uses most of the same keybindings. I've not seen paredit.
23:28 chandler: Hm. Here's the MIPS build log from Debian's autobuilder: https://buildd.debian.org/fetch.cgi?&pkg=plt-scheme&ver=4.2.4-2&arch=mips&stamp=1266948413&file=log
23:28 chandler: minion: paredit?
23:28 chandler: Whoops, this isn't #scheme.
23:29 waltermai: paredit seems to do the one thing in emacs that I was thinking drracket does better (or one of the few things).
23:30 waltermai: and I like being able to browse the web and email and irc from the same place, with emacs.
23:30 chandler: Hm. The mipsel build seems to have failed for a much less catastrophic reason. Actually, this seems like a build host misconfiguration. https://buildd.debian.org/fetch.cgi?&pkg=plt-scheme&ver=4.2.4-2&arch=mipsel&stamp=1266855447&file=log
23:32 waltermai: ah, it's done
23:32 chandler: And your little netbook is a mipsel. Maybe the build would have failed after that point anyway.
23:33 waltermai: at the end it says "Compiling xformsupport\n make[4]: *** [xsrc/precomp.h] Error 1", which seems to be the relevant part. I'll send it along to the bug folks. thanks again dudes.
23:34 chandler: Hm. Is that all? The make[4] line is just make noise.
23:35 waltermai: well, thats not *all*, but that's where the errors begin.
23:35 chandler: lisppaste: url?
23:35 lisppaste: To use the lisppaste bot, visit http://paste.lisp.org/new/racket and enter your paste.
23:35 chandler: Can you paste a few lines from before that point and a few lines after there?
23:35 waltermai: hah, no, it's on a different computer. lemme jump onto irc from that one, then I can.
23:35 waltermai: brb.
23:37 (quit) waltermai: Quit: Leaving
23:38 (join) waltermai
23:39 waltermai: backskies. k, now to get the relevant text...
23:39 waltermai: should I just yank it all in, or is there a special way to paste multiple lines?
23:40 waltermai is getting his yank/paste verbs confused
23:40 waltermai: lisppaste: url
23:40 lisppaste: To use the lisppaste bot, visit http://paste.lisp.org/new/racket and enter your paste.
23:40 waltermai should think before speaking
23:40 chandler: Just go there and stick it in the box. :-)
23:43 lisppaste: waltermai pasted "build-log lines" at http://paste.lisp.org/display/112415
23:43 waltermai: that was the most involved captcha I've ever seen.
23:44 chandler: Involved in what way?
23:44 waltermai: I had to do arithmetic.
23:44 waltermai: http://paste.lisp.org/+2EQN
23:44 chandler: The bot already gave the url. :-)
23:44 chandler: You must be using a text browser of some kind.
23:44 waltermai: oh.
23:45 waltermai: yeah, emacs-w3m!
23:45 chandler: Hm. Still no clues from that.
23:45 chandler: I think I'm going to give up for now; hopefully the maintainers will have a better idea if you pass along the full log.
23:46 waltermai: and I just wasn't using my eyes. I expected lisppaste to paste it to the channel in full instead of stating the url... okay dude, thanks for the interest.
23:48 chandler: IRC reacts badly to large pasts - lisppaste manages that particular problem.
23:58 Lajla: samth, I never claimed that, I said that if I added that behaviour to the list of errors you mentioned and changed nothing else.
23:59 Lajla: Then with respect to my new list of errors, haskell's runtime could produce that error.