« first day (990 days earlier)      last day (3967 days later) » 

Xeo
10:00 PM
@ThePhD just pull from the puppy directly.
 
There's so much to do. :C
 
@Xeo What can you do with unconstrained fully polymorphic type?
 
Xeo
@CatPlusPlus Ah, true.
 
@ThePhD Oh, it builds. It just wouldn't execute, since you pulled Clang then the part of Wide that makes Clang actually codegen shit was broken.
 
@Xeo How do I do that?
 
10:00 PM
so if you did, say, std.cout << std.string("Hello, World") you'd get six billion missing function errors.
 
Xeo
@CatPlusPlus Didn't make the connection to constraints there.
 
@DeadMG Oh. I don't know what that means in terms of errors but it sounds dangerous.
 
the problem with constraints, as far as I see it, is that either they are weak, or you have to do it manually.
@ThePhD It means Wide can't compile the most basic C++ interoperating programs.
 
Is it broken because we're using an updated Clang?
 
well, it curiously worked fine before I updated
 
Xeo
10:02 PM
@DeadMG Nothing wrong with manually, if you get help with the manual part of it.
 
@Xeo I think I'm not principally opposed to "manually" either. I think it could well be partly about API design as well.
I mean, if you have a function that takes a T and makes a std::vector<T>, then you'd have to analyze your exact uses of that T in all code paths to know it's concrete requirements.
 
Xeo
Haskell shows how "manual" constraints work fine.
 
I really, really, really hope the syntax is:
concept ConceptName : [type_trait0], [type_trait1], ... [type_traitN]
{ /* not even necessary */ };
 
Is there a type system/category theory/I-don't-really-know that guarantees a 1-to-1 relationship between function type and definition?
I imagine not.
 
Xeo
@GManNickG Meaning for the same type, you can only have the same definition?
 
10:05 PM
@Xeo For example, N -> N would not be a valid function type because it has more than one inhabitant.
However, typed well enough you could define (+) uniquely. (Conjecturing this, obviously.)
 
Xeo
So basically the type would be the functions identity, not the name
 
@Xeo Exactly.
 
@GManNickG No, you couldn't, not really.
 
Xeo
Not sure how useful that would be (read: I don't think it'd be useful at all, really)
 
how are you going to define + and -? they are both int -> int.
 
Xeo
10:06 PM
@DeadMG Subtractable -> Subtractable, d'uh!
 
@DeadMG They are both int -> int in your type system, because that's as strong as you can type it. The question is there such a type system that's "better".
@Xeo The take away being now you can just synthesize an implementation. Programming would be specification programming, leaving the implementation totally unspecified.
 
@GManNickG Nope.
 
@DeadMG Proof?
 
simple
 
If you say "Halting" in this next sentence I'm ignoring it.
 
10:08 PM
the set of, hell, let's just say integers, offers more than one operation of the same signature, and that's a mathematical fact.
there is nothing any type system can do to get around that fact.
 
Xeo
@DeadMG Depends on how you define your types. There's only one reasonable implementation for SubtractableInteger -> SubtractableInteger, I think.
 
I'm not sure I follow. Let's say the type signature for my function is "N x -> N y, y = x + 1". That uniquely defines (+), I think.
 
Xeo
(Again, not that that'd be particularly useful.)
 
@GManNickG The issue is not how you would define +, but how you would define all the operations available on integers.
 
Xeo
Since you now have to provide an implementation in the type constrain, basically.
 
10:10 PM
@DeadMG I don't follow. Why do I want to define all operations? Nobody tries to do that, there are an infinite number of them.
 
user142019
I've been thinking for long about a CoffeeScript-like language that compiles to Objective-C. However, some features would require type-checking and that's quite annoying.
 
your type system is worthless if all you can do with integers is add them.
the problem comes when I wish to have addition, multiplication, exponentiation, etc.
 
@DeadMG Who said that was the case?
 
Xeo
@GManNickG Wait, are you saying the compiler should deduce a + b from c = a + 1?
 
@GManNickG Prove that you can define both + and * in the same way.
particularly
 
10:11 PM
@Xeo The problem with these really low level exampels is the specificaiton language needs to understand math implicitly.
 
as far as I am aware, integral multiplication is defined by repeated addition, therefore by default it must have the same types.
 
@DeadMG You seem to think I have a white paper in front of me I have submitted to a committee. I don't, I'm only brainstorming.
 
if you have X * Y defined as X + (X * (Y - 1)) (plus termination ofc) then it's obvious that X and Y can't have different type constraints to X + Y.
 
@Xeo I wrote the wrong function, I meant (++).
 
@GManNickG Right, and I'm replying that your idea is uselessly limited, being as how even trivial mathematical systems define several operations of identical signatures.
 
10:13 PM
@GManNickG Don't you hate when that happens?
 
Xeo
@GManNickG That's concatenation! (:P)
 
@Xeo :).
 
@GManNickG There isn't.
 
@DeadMG You're completely missing the point. Drop whatever type theory you have in you head. There aren't any signatures because we're making up a new type theory.
 
user142019
@Xeo Gah, (++) is too specialized. Use mappend!
 
Xeo
10:14 PM
@rightfold Was about to say something about Monoids :)
 
@GManNickG You said that each signature should have a unique definition. That clearly says that you have signatures for functions.
 
@CatPlusPlus Any summary why? I wouldn't be surprised. But saying + and * have the same signature is of course missing the point.
 
It's true for some cases, but not in all.
 
@DeadMG I meant any signatures [in your existing type theory] because...
 
@GManNickG It doesn't matter what you define the types of X and Y to be.
 
user142019
10:16 PM
@GManNickG well, ignoring subtyping and impurity, in some cases you can only have one input/output set for all function definitions of a given type.
 
the problem is that multiplication clearly has identical types to addition, by definition.
 
user142019
fst :: (a, b) -> a is an example. You could implement it as fst (x, _) = x or fst (x, y) = snd (y, x) or whatever you want but the result is always going to be the first element of the tuple.
 
@DeadMG Sigh. The function types are different, is my point. The arguments can both be N, sure; the output is not both N.
 
@GManNickG They both return N. In fact, the multiplication returns the result of addition... so it must return that type.
 
@DeadMG You're really missing the point of this exercise.
 
then you must be doing a very strange job of explaining it
 
user142019
 
it's trivial to construct scenarios where two very different functions have the same type requirements.
 
user142019
The last sentence.
 
@rightfold dat video
lol
 
10:20 PM
Let me put it a different way. A function has inputs A, B, C, ..., and a single output R. You can define constraints on all of these, in any language an SMT solver will understand.
Is it possible to uniquely constrain the functions we find useful for programming?
 
no, since both addition and multiplication have the same constraints (for a simple proof by counterexample)
unless you want to suggest that the return value should be constrained to be A + B for addition, and A * B for multiplication.
 
Rebase tiiime.
 
in which case, that's just recursive since you haven't defined A * B at the time you're trying to use it to express the requirements on the result of A * B.
 
@CatPlusPlus You really like pwning your history, don't you?
 
@DeadMG Knowledge of + and * is built into SMT's, which is what I was saying to Xeo: these baseline examples aren't much use since their constraints are their definitions.
Consider more high level like a sorting function.
 
10:23 PM
@ThePhD Temporary branches vOv
 
@GManNickG Arguing that they are special because they are primitive is useless.
 
There's more than one way to sort, which makes it interesting.
 
I need to sync between computers somehow.
 
for example, matrices.
 
@DeadMG Not really. That's the whole point of SMT solvers.
 
10:24 PM
or complex numbers.
 
user142019
What is rebasing? Merging multiple commits into one?
 
or wave functions.
 
@CatPlusPlus ~~~Dropbox~~~
 
the simple fact is
your definition of + and * is recursive, so even if you were to primitive away the integers, any type and function pair with a similar setup has the exact same problem.
 
Rebasing is changing parent of a changeset subgraph, but in git it can also squash and edit commits.
 
10:25 PM
so unless you want an infinite set of primitives which includes the entire of mathematics
it can't possibly work.
 
user142019
Ah, I see. Neat.
 
@DeadMG I see what you're saying, I don't think it's right. You're limiting yourself too much.
Both + and * return N, yes. We agree. The different is the constraint on the values to the inputs.
 
none in both cases.
all integers are valid on both sides of both + and *.
 
@DeadMG Er, you have no constraints on what add and multiply should do?
@DeadMG So return 0 is valid for both?
 
that's the output, not the input.
 
Ell
10:27 PM
Remotes?
 
@DeadMG The sentence you're replying to talks about output.
 
plus, I already described how that's recursive and unusable.
@GManNickG You said "Constraint on the values to the inputs". That says "inputs" to me. Unless you made a typo.
 
@DeadMG You think you did, but the point of this tangent is to summarize why not. Don't be circular.
 
@GManNickG Ok. Then define the constraint on the return value of + without requiring the definition of + first.
 
@DeadMG Values [of the return types]. Unclear, yes.
@DeadMG Wow. You now have forgotten the point of primitivizing integer arithmetic in SMT solvers?
And that I said these bottom level examples aren't useful because they are built into SMTs?
 
10:29 PM
@GManNickG As I said before, that requires an infinite set of primitives to be effective.
 
SMT?
 
@DeadMG No.
 
ok
 
Sparse Matrix T...?
 
In computer science and mathematical logic, the Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming. Basic termino...
 
10:29 PM
Simultaneous Multithreading?
 
so your SMT has every single mathematical type, ever built-in, which has both * and + with the same constraints?
 
Special Math Theory?
AWWW
I WAS CLOSE.
 
@DeadMG No.
 
even the ones which haven't been built or invented yet?
 
oh... ahaha guesswork fail...
 
10:29 PM
then how is it not useless?
 
user142019
@Mysticial Super Mario Tennis
 
I can't define my own types that have properties even similar to the basic integers.
 
Just like mathematics is built on axoims, and more theorems follow from them.
 
@Mysticial I had Theory in there.
 
user142019
Oh wait, that's called Mario Power Tennis. Whoops. :v
 
10:30 PM
@DeadMG Sure you can. Give an example.
 
ok.
 
Or maybe we can't. The whole point is to figure out. Not hand-wave it away.
 
I define my new type as exactly like the integers, except that when you add them, it adds an extra 1 to the result (once, not recursively, that would be dumb).
 
@DeadMG You tried. :) Small hobby of mine.
@DeadMG Okay. So D (for DeadMG) is your type.
 
sure.
 
10:31 PM
Let's just make up some syntax, like class D { int underlyingValue; };
 
works for me.
D operator+(D lhs, D rhs) { return lhs.value + rhs.value + 1; }.
 
@DeadMG In C++, sure.
 
else all operations taken from integers directly.
@GManNickG Yeah.
oh, er, ignoring the fact that int in C++ is not AP, of course.
 
reword, squash, squash, squash, reword. :v:
 
doesn't VS support in-class initialization?
 
10:33 PM
nop
 
But in constraints-land, maybe: function operator++(x,y), requires: x, y : D; result.underlyingValue = x.underlyingValue + y.underlyingValue + 1;
 
ok
 
Note there is no function definition, just constraints. But we can synthesize a definition from the constraints.
 
so instead of doing anything, at all, differently to how it's done now, you just took the definition and said "This is a constraint on the return value"
which, arguably, it is.
 
Obviously such integer-like operations are really simple, as their constraints are there definitions, since our constraint language understands integers.
@DeadMG Right. The point being you can run an SMT against the implementation and verify it matches the constraint.
And now you have a formally verified function.
 
10:35 PM
@GManNickG The definition is the constraint.
an SMT can't do shit with that.
 
@DeadMG In this case, yeah.
That's why I suggested a sorting example.
 
what would be the easiest language to make raw numbers into graphs with?
 
ok
 
@Crowz Graphviz.
Or DOT language, rather.
 
well, you only have two choices, which is to either specify the result of heapSort to be heapsorted, or define it to be sorted, in which case you ban all but one sorting algorithm.
also, Turing-Complete is going to kill you.
 
10:37 PM
And I forgot squashing asks for a new message anyway.
 
@DeadMG Yes, that's what sparked me to ask. Setting the stage took a little longer than I imagined.
 
Meh, fuck turing completeness. I don't care if I have it or not.
 
well
 
@DeadMG I think the idea is to specify "this is a function that results in a sorting list, and at some point the list is a heap [which I defined elsewhere]".
 
10:38 PM
@GManNickG That's really no different to defining the result to be heapsorted.
 
I think perhaps that uniquely defines a heapsort.
 
you're still banning all implementations of heapsort that heapsort slightly differently.
 
@DeadMG Yes.
 
also
since real programs are, in fact, Turing-Complete, then if you don't have it, the answer to your original query is definitely "No."
 
That's fine, the point of this was not to bicker, but just see if this had been more formally explored before and if someone knew. How limited is such a constraint language?
 
10:40 PM
well, very.
almost all useful systems are TC.
you hit TC almost as soon as you can branch.
 
Haskell isn't TC.
 
user142019
@ThePhD Wat.
 
user142019
Of course Haskell is TC.
 
user142019
Poop is leaving your mouth.
 
Lies. It's only turing half-complete.
 
10:41 PM
TC is almost completely irrelevant to software engineering regardless. If I can program what I need to, it's good enough. Human programs are wide, not deep.
 
yep
 
user142019
@ThePhD Elaborate.
 
Heh, wide.
 
but since you hit TC almost immediately, a non-TC system cannot really implement any useful programs at all.
 
@rightfold I'm just being an ass. :D
 
10:42 PM
@rightfold The "All loops must terminate" requirement of C++11, I'm not sure, but that might make C++ non-Turing-Complete.
 
user142019
You can simulate any single-taped Turing machine using Haskell.
 
@DeadMG I don't doubt you hit TC soon, I do doubt all useful programs require it.
 
Ell
I thought Turing machines had infinite memory and time :3
 
user142019
Ignoring memory constraints but that's always ignored when talking about TC-ness.
 
@DeadMG while (true) {} is illegal?
 
10:43 PM
@GManNickG The problem has little to do with requirement. It's about proof.
 
user142019
@ThePhD The compiler can assume that a thread either terminates or exhibits side-effects.
 
@DeadMG Huh?
 
even if you state that you are in a non-TC language, like C++11 if my conjecture was correct, you still run into very real problems.
 
@DeadMG Is this true?
 
@ThePhD It can be optimised out. :v:
 
10:43 PM
for example
a TC machine can run an algorithm that never halts, like the empty loop.
 
user142019
@CatPlusPlus The fastest infinite loop ever!
 
72
Q: Optimizing away a "while(1);" in C++0x

Johannes Schaub - litbUpdated, see below! I have heard and read that C++0x allows an compiler to print "Hello" for the following snippet #include <iostream> int main() { while(1) ; std::cout << "Hello" << std::endl; } It apparently has something to do with threads and optimization capabilities. It looks ...

 
but a non-TC machine can still run an algorithm that runs for unbounded finite time.
this is effectively just as intractable
 
Also IIS doesn't support name-based SSL.
 
Goddamnit. I'm learning C# since I need it for work... and the sheer amount of syntax sugar is driving me nuts. lol
 
10:45 PM
I've hit this today after refreshing API site for half an hour and wondering why log from a different site changes.
@Mysticial It's good for you.
 
user142019
@Mysticial Can you give a specific example?
 
@DeadMG: Anyway, any total functional programming language is not TC, yet can compute quite a bit.
 
right, but "finite but unbounded" is just as big a problem as "infinite", realistically.
 
user142019
C# doesn't have that much syntactic sugar. You should see CoffeeScript. :lol:
 
@rightfold I had to learn C# lambdas, nullable types, null-coalescing operator, and properties in 2 days from just trying to read our source code.
 
10:47 PM
@Mysticial There's syntax sugar?
 
Oh and partial classes...
 
@Mysticial It's trivial.
 
None of these exist in C++ or Java.
 
@DeadMG But you weren't talking about "realistically", you brought in theoretically when you mentioned TC.
 
@Mysticial Partial classes are the best. <3
 
user142019
10:47 PM
@Mysticial Lambdas exist in C++.
 
It's what allows me to edit teh same class between 2 people.
 
ok, well I'm actually pretty sure it's an equally big problem theoretically.
 
@rightfold cross that out.
 
Nullable types is more-or-less boost::optional.
 
user142019
And nullable value types is similar to boost::optional<T> but with the syntax of either Nullable<T> or T?.
 
10:48 PM
Lambdas are just anonymous functions, nothing magical about that.
 
user142019
Null-coalescing is like JavaScript ||. Don't know if you know JavaScript.
 
Null-coalescing x ?? y desguars to (x != null ? x : y).
 
Ell
How about open classes. Monkey patching yay!
 
user142019
@CatPlusPlus But evaluates x only once.
 
Fuck open classes.
 
10:49 PM
@Ell That's essentially JavaScript.
 
user142019
@ScottW I would have liked T? if it was required to make reference types nullable.
 
user142019
There's a few things about C# that I don't like. I should make a list of them.
 
Properties are just get/set methods hidden away behind a common name.
 
user142019
All reference types being nullable is one of them, as well as some stuff in object that had to be in an interface (in particular comparison and hash function).
 
<3 Properties.
 
10:50 PM
The only magical thing is auto-properties, which also generate a field for you.
I.e. T Property { get; set; }
 
@ThePhD Could you please send me i686-w64-mingw32-g++.exe? I appear to have accidentally done something horrible to mine.
 
@DeadMG I uploaded the entire thing to Downloads.
Just go grab it from the downloads page on your Wide page.
 
@ThePhD I don't have the bandwidth to grab the whole thing.
 
Oh. Uh. Right, well I'm at work right now, but I'm about to head home...
 
10:51 PM
ok
 
user142019
@Mysticial Wait till you see query expressions. :)
 
@rightfold I also learned the hard way that x = 1 / 2.; is invalid code in c#...
 
user142019
Also, out parameters must be removed from C#. They're worthless. C# has tuples.
 
Because of class extensions... :(
 
Skipping that zero is a crappy convention anyway.
 
10:53 PM
never mind I got it
 
user142019
Dividing an integer by a floating point number should be illegal.
 
user142019
It should require an explicit cast.
 
user142019
Yes, another thing to put on my list.
 
Also fuck Rails and Ruby forever.
 
Ell
Ruby is beautiful
 

« first day (990 days earlier)      last day (3967 days later) »