« first day (544 days earlier)      last day (4386 days later) » 

8:00 PM
Everytime I see someone say ff my brain starts by thinking they forgot "sake".
3
 
Why does Vim default with horizontal splits? It messes with my brain.
 
@rubenvb I have no idea.
 
The reason I'm asking is because it seems to me that it's becoming more apparent that Turing Completeness, while neato, isn't important to almost all programs. We could do quite a bit more if we, for example, required all programs to terminate. (Yes yes, this opens up the can of worms that is termination analysis, but that itself isn't too hard in practice.)
 
alright, it was April 5th, more than a few days ago :(
 
@GManNickG Turing Complete is not a choice, it's a fact.
 
8:01 PM
let's see what it gives
 
consider a server application, for example- servers can have months of uptime or more
 
@GManNickG In fact, C++11 requires more programs to terminate.
 
and it's a fact that C++ is Turing-Complete
 
@DeadMG Sure, but that's irrelevant to what I was saying. I don't get what you mean in "Turing Complete is not a choice"
 
you can't choose that while(true) DoUserInput(); is not guaranteed to terminate- it's a simple fact of the realities of what that program does and how it operates
 
8:02 PM
Wow, I just did T const* = alias<T[16]> {} in a parameter declaration.
 
@DeadMG You're misunderstanding what I'm saying, I'm not talking about C++.
 
@LucDanton WTF are you doing.
 
the only languages you could possibly do are minor declarative ones like SQL
but since they're not TC in the first place, it's not changing anything
 
SQL is Turing-complete.
 
@DeadMG I really don't understand what you're trying to say.
 
8:04 PM
Well, at least all SQL dialects I know are.
 
@RMartinhoFernandes API that implicitly accepts a 16-long array via a single pointer.
 
If you required all C++ functions to terminate, for example, then C++ would no longer be Turing complete.
 
@GManNickG What I'm saying is that it's nice to say "If only languages or programs weren't Turing complete", the reality is that they absolutely are Turing complete and there's nothing you can do about it.
 
But from my thought experiment above, still totally useful.
@DeadMG That's simply false. They are that way because we design them to be.
 
because they have to be in order to be useful
 
8:05 PM
@GManNickG int x; while(std::cin >> x) std::cout << x; would not be valid under that requirement.
 
@RMartinhoFernandes It terminates when cin is empty (wrong terminology, sorry).
 
@GManNickG And that is when?
Possibly never.
 
@GManNickG That's not program termination.
from the perspective of the program, cin is more than possibly infinite.
you cannot ever look at that program and guarantee termination.
 
@RMartinhoFernandes Require implementations to timeout after 5 times the age of the Universe.
 
you could trivially redirect cin to /dev/random, for example
 
8:07 PM
$ myprogram < /dev/zero. There, infinite std::cin (yes, it doesn't work with the program above, I know)
 
@RMartinhoFernandes Input cannot be infinite on a finite machine.
 
the rules which dictate when the program ends are totally outside the bounds of the program
 
@RMartinhoFernandes That wouldn't be allowed, silly. That's the point.
 
@GManNickG Why shouldn't it be allowed?
 
@GManNickG You've just banned a massive amount of all useful programs.
 
8:08 PM
Why can't my program run for the entire lifetime of the hardware?
 
what's the difference between me, a user, sitting down and going 0,0,0,0,0,0 and /dev/zero?
 
I should have made myself clearer: I'm not arguing you can't write programs that don't terminate, I'm saying you probably don't need programs that don't terminate.
 
@GManNickG How could you possibly write any program that interacts with the user?
my use of the program is unbounded
 
@LucDanton Would that requirement be useful for optimization (I believe that's the goal here)?
(I'm asking out of genuine curiosity, it's not a loaded question)
 
I don't know about compiler optimization.
 
8:10 PM
@DeadMG By assuming the user will eventually end input.
 
Well, I referred to your message more for context than anything, the question is intended for anyone that has an inkling of an idea :)
 
You're mistaking, "I don't know when it'll stop" with "It'll never stop".
 
@GManNickG I'll argue on your side if you show an optimization that can be done based on that assumption.
 
in that case
all programs must eventually terminate when heat death of the universe occurs
problem solved
 
@RMartinhoFernandes Eh? Not really for optimization, just for safer programs. You can use dependent types without as much restriction, and I know my program doesn't have an infinite loop.
 
8:12 PM
@GManNickG You don't need that requirement in the language to know it doesn't have an infinite loop.
 
@RMartinhoFernandes Right, but I do need it to know my type system is well-defined. (If it has less-restricted dependent types, for example.)
 
Because you know the user will eventually end input.
You're trying to convince us that the compiler needs to know that.
 
what does infinite loops have to do with type systems?
 
@RMartinhoFernandes To be fair, you guys came up with the input example. The compiler needs to know it for other things as well, if you want to start asserting stronger statements about your program.
 
8:14 PM
@GManNickG FTR, int main() { while(true) {} } is UB in C++11.
The compiler is already allowed to assume termination except on the face of things like input.
 
@DeadMG If I have a type that depends on a value but the calculation of that value never halts, but I assume it does anyway, I've just made my type system unsound.
 
@GManNickG How can a compile-time type possibly depend on a run-time value?
 
@RMartinhoFernandes Hell, it's even ill-formed. :P
 
@GManNickG Oops.
 
In computer science and logic, a dependent type is a type that depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like ATS, Agda and Epigram. An example is the type of n-tuples of real numbers. This is a dependent type because the type depends on the value n. Deciding equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type c...
 
8:16 PM
ah, I see
if the user introduces an infinite loop into the compiler, then it's their own dumb fault
and the results are not your problem
 
@DeadMG You mean programmer as user?
 
yes
if I write std::array<T, N> where N is an infinite loop, then that's my mistake
 
Well, it's easy to say, "not my problem", but the point of programming languages is to improve the ease and quality of programs...
 
yes
 
@DeadMG Yes it is, and it would be most excellent if the compiler could tell you that.
 
8:18 PM
but it's also not your job to coddle the programmer and waste your time dealing with every tiny little mistake I might ever make.
and undefine a bunch of useful behaviour just because I might happen to make a mistake or mis-use it
 
@DeadMG Maybe not your job, but there's no reason I can't make it my job.
 
@GManNickG In that case, the compiler is already allowed to reject the program.
 
@DeadMG I think you're exaggerating the effects of not allowing infinite loops.
 
Template recursion depth limit.
 
@GManNickG It's a general principle.
 
8:19 PM
@GMan I know it's probably asking too much, but can you craft a small example? Please...
 
@DeadMG I don't follow.
 
while it's great to have the compiler protect me from error, I would never sacrifice the ability to jump off a cliff if I said so
the compiler's job is to do what I tell it to, and you can pop up as many "Are you sure?" dialogs as you want, but "No." is always the wrong answer.
 
@RMartinhoFernandes We (humans) wanted to stop programming in assembly because it was hard and error prone, so we made programming languages. Now I want to stop programming in C++ because it's hard and error prone, so make a better one, etc.
@DeadMG Sounds like a pretty large claim, what's your justification?
 
Anyway, the dependent type thing is not about std::array<T, N>.
 
@GManNickG Because I'm smarter than a compiler.
 
8:21 PM
@RMartinhoFernandes Oh, you mean example of a dependent type?
 
if I use a pointer, you can never guarantee that it's safe
 
@GManNickG Of an optimisation.
 
but maybe I used my super human brain to parse the specification for this old C API function and I know it's safe
 
It's about the return type of a function something f(int n) that returns an n-tuple.
 
@DeadMG That's not true. ATS does it.
@DeadMG And wouldn't it be nice if the language did that for you?
 
8:22 PM
@GManNickG What, NLP'd the specification of every function I ever call from every library and determined if I was using it correctly?
 
@RMartinhoFernandes Sorry, I'm juggling multiple things at once, what do you mean?
@DeadMG What's NLP'd?
 
@GManNickG Nevermind, I got lost too.
 
(natural language parse)d
 
@DeadMG Not necessarily, you specify it like you specify anything else in programming, with types.
 
It seems reading tropes and language design discussions at the same time is counter-productive.
 
8:24 PM
stackoverflow.com/questions/10130701/…: "I am looking for the fastest way to ...". Why does everyone want the fastest way? Never the best way, the most general way, the most correct way, the most maintainable way, the most understandable way, the best documented way, the easiest way, the simplest way. Always the fastest way.
 
@RMartinhoFernandes Quite alright. So do you want an example of a dependent type, though?
 
@GManNickG No, I know that.
 
@GManNickG That requires the compiler to have, in advance, a way of expressing a type that means everything I could ever express in English.
which I find unlikely
 
@RMartinhoFernandes Okie. <3
 
3 mins ago, by R. Martinho Fernandes
It's about the return type of a function something f(int n) that returns an n-tuple.
 
8:25 PM
@DeadMG Nope, just anything useful. The better the language, the more useful things you can express. Don't mistake "doesn't do what I need" with "useless". Seatbelts don't always save lives, but they sure as hell help.
 
@DeadMG Types are defined by their inhabitants. Math is good enough for that. No need for clunky natural languages.
 
"Returns a pointer that's invalid on a Wednesday if you had a bad day and otherwise every other index is valid if your mother's name is "Adam"".
 
@RMartinhoFernandes Hm, I'm not sure I follow.
 
not to mention the fact that you'd be using up my cycles without asking me checking this stuff
 
@DeadMG Type-checking is a compile-time feature.
Again, you seem to be trying to take things the system isn't intended to do and say, "look, it can't do it, it's useless!"
 
8:26 PM
Martinho's example of a dependent type put them at run-time.
@GManNickG The system is intended to do what I tell it to. If it can't do that, then it's useless.
 
@DeadMG No, I'm thoroughly confused. Don't let me drag you. ;)
 
@DeadMG We'll just have to disagree, then, because you also seem to be presupposing the claim, "...and what I always intend to do is correct".
 
@GManNickG No. What I'm saying is that you can never prove that what I intend to do is incorrect, except in the most trivial examples.
 
DeadMG always supposes that.
 
8:29 PM
@DeadMG We disagree there too. I urge you to look at ATS and see what it does. It's quite possible to make complex programs that are guaranteed to have no errors.
Or even just Haskell, though some of the error checking can't be expressed in the type system (unless you enable the right extensions).
 
@GManNickG I did open the ATS site. Didn't find it easy to find a quick reference on such things.
 
That's the whole point of those languages (I suppose ATS is somewhat like Coq).
 
@RMartinhoFernandes Yeah, cousins. Coq is for theorem proving, ATS is for program proving (which by a certain theorem are the same thing).
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and proofs. It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and logician William Alvin Howard. Origin, scope, and consequences At the very beginning, the Curry–Howard correspondence is...
 
whilst I'm totally in favour of type systems that can prove more rather than less about a program
 
@GManNickG Anyway, I now know what threw me off in all this. I was still thinking this was about optimization, even after you said otherwise. Sorry for messing up the conversation.
 
8:31 PM
I'm not in favour of babysitting a programmer by forcing him to waste his time explaining himself to a program
and I also don't really see the need for it
 
@DeadMG You do it every time you input a type.
 
@DeadMG So, why do you use static typing?
 
there's a big difference between static typing (also I infer everything I can) and everything ever needed to guarantee correctness about my program
 
@RMartinhoFernandes That's okay. I'm still studying this stuff on my own and I think they can help make stronger optimizations. Consider memcpy versus memmove; if the type-checker can show the ranges don't overlap, it'll use the the former, otherwise the latter (or an error, and require it be shown to be one way or the other; programmers can add explicit checks themselves to "cast" the type).
@DeadMG Hardly. Type systems exist to guarantee correctness about your program.
 
@GManNickG They are of limited guarantees.
 
8:34 PM
@GManNickG Kinda like when you use unsafePerformIO to wrap calls to pure C functions from Haskell.
 
@DeadMG Some are, not all type systems are the same.
 
@DeadMG Wait till your software needs to control a multi-billion dollar satelite, or google's autonomous car project
 
not really
types have to be implemented
it's great to say that I have a Plane type
but when I have to implement the "isInFrontOf" method myself, you cannot in the general case ever know if I implemented it correctly
 
We all know that. We also know that getting "a lot of guarantees even if not all" is better than getting "very few guarantees".
 
sure
 
8:36 PM
@RMartinhoFernandes Exactly. A practical language with dependent types will need to have three "layers", safe, trusted, and unsafe. Safe functions can call safe and trusted functions, trusted functions can call anything, and unsafe functions can call anything and do external function calling. Now you have a choice between trusting something unsafe works, or checking that it actually does.
 
but I'm also not going to use a language where when I receive an array from the operating system or other external API, it has to check all my bounds accesses on that pointer.
 
@DeadMG what are you implying? To me it means, that the site may not be optimal, you have no patience or, likely, both.
It reminds me a bit of when you dismissed that presentation on continuous and visual feedback by an Apple 'architect' (? don't remember who) because you didn't see a compelling example in the first minute.
 
@DeadMG To the contrary, you can. The problem is that you literally have to specify the proof of correctness in the type system; ATS makes this very easy. But I'll argue it's still not pragmatic enough yet, but there's no reason to say, "well then forget about it".
 
@sehe All I'm implying is that he's referring to one specific aspect of the language, and I found the site non-trivial to navigate. That's all.
@sehe Hey, I watched plenty of that video, not just the first minute.
@GManNickG If I had the correct mathematical formula, I wouldn't need the type system, or to debug the function.
 
@DeadMG But the point is to have the compiler help you out by verifying that your implementation of the formula is correct.
 
8:40 PM
@GManNickG But if I had the correct formula to compare it to, I wouldn't need the compiler's help.
 
...
> to compare it to
That right there is where compilers excel above the head of humans.
 
@DeadMG You're saying you don't know what your program has to do?
 
@RMartinhoFernandes Sure. I know it needs to find out whether or not a point is in front of a plane.
 
All you need is to express your requirements, the type checker takes care of verifying them.
 
how that's done is another problem
I still have a distinct feeling that I accidentally put all my planes backwards and then checked if all the points were behind the planes...
 
8:43 PM
@DeadMG If the result is still the same, mathematically, for each function you define for your plane implementation, then that's a-okay. That's merely a difference in storage.
 
not for anyone who has to use the Plane class outside of where I passed in the points in the wrong order :P
 
Then you defined "front" wrong in your specification. Of course the type checker can't guess the specification for you.
 
@DeadMG Hm?
 
@RMartinhoFernandes Ah. More accurately, I know what "front" is, but I have no idea what the mathematics of specifying it are.
after all, if I knew them, I wouldn't have the problem in the first place :P
 
And dependent types, while being more powerful for being able to express program specifications, aren't the only useful improvement to be made to type systems. Imagine if C++ had uniqueness types; no more UB for data races, compile-time errors for data races.
 
8:48 PM
@GManNickG unique_ptr?
it would be a tad of a bastardization, I admit
but should be usable
 
@DeadMG Just a coincidence in naming, different things.
 
eh
 
Is there a sane open source 3D engine around? I mean, Ogre is a singleton fest, Irrlicht makes liberal use of the hungarian notation...
 
I checked the example on Wikipedia, and I think it should work
@EtiennedeMartel Why do you think I'm writing my own? :P
 
Yeah, I figured as much.
 
8:49 PM
@DeadMG How so?
 
@DeadMG You're not open sourcing it! It's not a total replacement ;P
 
@GManNickG Consider the first example, where File is File*, and unique File = unique_ptr<File*>
when you call readLine2(unique_ptr<File> f), then you know the caller no longer owns the File in question
because you have a unique_ptr to it.
 
That's not compile-time though.
 
although, of course, the C++ compiler won't tell you if you use a unique_ptr you std::moved from
 
@DeadMG C++ can't do uniqueness typing. I can still form multiple references to unique_ptr's in general, or whatever they are pointing at via get(). (You're not wrong in saying that's an approximation, though.)
 
8:51 PM
but you will get a nice run-time crash the instant it happens :P
@GManNickG Not really. If you actually destroyed and created new File objects, anyone using an old reference would be kaput.
 
@DeadMG Would they be kaput at compile-time?
 
admittedly, no
hence the "bastardization" part :P
 
Do package managers generally allow a program to require a version of a dependency within a certain range?
 
but as I said a little previously, I think that a language with sufficiently generic metaprogramming facilities should be able to include this
 
@GManNickG A reference to a unique_ptr is useless as soon as it gets moved. But yes the accessing members fuck up by letting you stow away references and cheat..
 
8:53 PM
and I think that Wide has the power to do it
 
Like, "This program needs a feature that was added in 1.0, but it was deprecated in 3.0 and we're not keeping this program up-to-date anymore."
 
Cool.
 
@DeadMG "with sufficiently generic metaprogramming facilities should be able to include this" Aka a powerful type system! :P
 
uh, no
type system is one use of a sufficiently generic metaprogramming facility
there are many others
 
8:55 PM
You've lost me on that one.
 
consider expression templates
 
That's using the type system.
 
implementation detail
when you express an expression template, it is about running a function on an expression
or even the trivial factorial or fibonacci programs produced by TMP 101
they have little to do with types
or the dearth of tools which output source code in any given program
 
@DeadMG Yes, but that also has little to do with correctness.
 
@RMartinhoFernandes "everything" includes "correctness"
 
8:57 PM
As an aside, if you ever have the chance to name something, don't put Greek letters in it; it makes searching for it once you've forgotten the name annoying as hell.
 
Where's "everything" in this conversation?
 
> sufficiently generic metaprogramming facility
 
whats the grep command to change all occurrences of barfoo with foo ?
 
@DeadMG I just built bison 2.5 on Linux for MinGW
 
@DeadMG Sufficiently generic to do the kind of correctness checks we were discussing, I assumed.
 
8:58 PM
yes
but GManNickG said that such a thing was a powerful type system
and what I'm saying is that the uses of a generic metaprogramming system are far beyond proving correctness
 
@qwertymk grep only searches.
You're probably looking for sed.
 
and type systems
 
@DeadMG Oh, you expressed that poorly then.
 
@DeadMG I'm losing track of your claim, but is it not the case that metaprograms are expressed within types?
 
@RMartinhoFernandes How would I do that then?
 
8:59 PM
4 mins ago, by DeadMG
type system is one use of a sufficiently generic metaprogramming facility
@GManNickG Only in C++.
 
5 mins ago, by DeadMG
uh, no
 

« first day (544 days earlier)      last day (4386 days later) »