Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Make the Type System Do the Work

nathan.ca

Post reply on HN
Print view View original

131–140 of 141 posts

Re: Make the Type System Do the Work

#131

Post by jeffdavis »

zvrba wrote: post #77
jeffdavis wrote: post #70

Earlier quoted context omitted.

"what is unsound is supporting mutations that alter identity" EDIT: included code for clarity I can make essentially the same example with concrete entities that exist in time and space, as well: void f1() { GasolineVehicle vehicle(myEngine); f2(vehicle); cout After replacing the engine with a motor, MPG no longer makes sense. At the time you're writing the Vehicle class, it seems perfectly reasonable to define a set…

> At the time you're writing the Vehicle class, it seems perfectly reasonable to define a setPropulsionDevice() method Are you claiming that it seems reasonable to be able to replace a car engine with a jet engine without changing anything else? (The car's hull, construction, etc., and after all these modifications it's not the "same" car anymore.)

No.

Any example I come up with is going to sound contrived, because it is. Real examples get messy, and just add to the confusion.

But real issues show up due to fundamental problems with "is-a": Even if an X value "is-a" Y value, an X variable is not a Y variable (because it can't hold all objects of type Y). So passing a mutable object reference to a function is fundamentally different than passing an immutable object -- but inheritance hierarchies treat them the same.

You can get around this problem by not using inheritance hierarchies that work that way, or by always using immutable objects (value semantics). But I pretty much consider the Java/C++-style inheritance to be a mess.

Re: Make the Type System Do the Work

#132

Post by dragonwriter »

jeffdavis wrote: post #131
zvrba wrote: post #77

Earlier quoted context omitted.

> At the time you're writing the Vehicle class, it seems perfectly reasonable to define a setPropulsionDevice() method Are you claiming that it seems reasonable to be able to replace a car engine with a jet engine without changing anything else? (The car's hull, construction, etc., and after all these modifications it's not the "same" car anymore.)

No. Any example I come up with is going to sound contrived, because it is. Real examples get messy, and just add to the confusion. But real issues show up due to fundamental problems with "is-a": Even if an X value "is-a" Y value, an X variable is not a Y variable (because it can't hold all objects of type Y). So passing a mutable object reference to a function is fundamentally different than passing an immutable obj…

> But real issues show up due to fundamental problems with "is-a": Even if an X value "is-a" Y value, an X variable is not a Y variable (because it can't hold all objects of type Y). So passing a mutable object reference to a function is fundamentally different than passing an immutable object -- but inheritance hierarchies treat them the same.

That's not a problem with "is-a", its a problem with unsound use of mutation in inheritance heirarchies. A mutating method can either: 1) Anticipate that it can fail, or at least the mutation component can (however that is signaled, whether by return value or exception), on some combinations of argument values and object state, in which case it works fine as a method anywhere in an inheritance hierarchy, or 2) Be guaranteed to succeed completely with any arguments of the appropriate types, in which case its fundamentally unsound anywhere except in a final class (since declaring a mutating method is essentially logically equivalent to declaring a method with a -- potentially additional -- return value whose type is simultaneously both the the type of the class it is declared in and the type of the class it is used in.

Re: Make the Type System Do the Work

#133

Post by pointernil »

tel wrote: post #107
pointernil wrote: post #94

I often wonder how the "tool" named MONADS could help to deal with this quite old problem of what I call meta-types or semantic types (i'm sure there is a proper name for this; I'm not a cs/type-theory professional ;) Time handling f.e. and often physical Units would quite often benefit from much stronger guaranties at compile and runtime. And no, OOP and it's tools are not sufficient to handle this... in theory mayb…

I don't think this has much at all to do with monads.

Care to explain in a little more detail? Is a calender resp. date-time monad really such a far fetched idea?

Re: Make the Type System Do the Work

#134

Post by tel »

pointernil wrote: post #133
tel wrote: post #107

Earlier quoted context omitted.

I don't think this has much at all to do with monads.

Care to explain in a little more detail? Is a calender resp. date-time monad really such a far fetched idea?

That's just a state monad, the thread and what I assumed and may have assumed incorrectly you were talking about, was around overloading math operations to work on dimensionalized quantities like feet and seconds and the like. You can dimensionalize time as well—take a look at the time or thyme Haskell packages for some fascinating examples.

Doing computation in the context of the current time is absolutely monadic. If you're handling time abstractly, it's the state monad. If you're handling it for real then you need some kind of monad protecting communication with NTP/your local CPU clock. That's IO in Haskell.

Re: Make the Type System Do the Work

#135

Post by tel »

taeric wrote: post #129
tel wrote: post #105

Earlier quoted context omitted.

The true quicksort example you linked has very little to do with Haskell's type system and everything to do with purity. The qsort version at the bottom of that page is also pretty close to the version used in any mutable language, just with a bit more noise in the syntax. A direct translation to Python might make the syntax easier to understand, though it should be stated that this is not supposed to be pretty Pytho…

My point is pretty much about the "a bit more noise in the syntax." And qsort will only work on array types, something that is typically shunned by people trying to "do all of the work with the type system." Consider the types for "NonEmptyList" and such. Is it neat when these work? Certainly. Do I think they pay obvious dividends in the effort increase? Not so much. I am open to the argument, but I have yet to see a…

Again, that noise is entirely an artifact of purity and syntactic choices, not the types.

I'm not sure exactly what you're arguing for here, but I can explain a use case of NEL—when you consume it you don't have to check the for emptiness. That means that you can eliminate an entire branch of code, either locally or in exception catching, or an entire failure mode.

Frequently people just throw those checks in and then assume, trusting their own eye or documentation to minimize the emptiness checking, but without expressing that into the type the compiler won't be able to help you not repeat that check. It's optimal to check it exactly once and people are liable to check it either 0 or many times.

Re: Make the Type System Do the Work

#136

Post by pointernil »

tel wrote: post #134
pointernil wrote: post #133

Earlier quoted context omitted.

Care to explain in a little more detail? Is a calender resp. date-time monad really such a far fetched idea?

That's just a state monad, the thread and what I assumed and may have assumed incorrectly you were talking about, was around overloading math operations to work on dimensionalized quantities like feet and seconds and the like. You can dimensionalize time as well—take a look at the time or thyme Haskell packages for some fascinating examples. Doing computation in the context of the current time is absolutely monadic.…

Yup, you assumed incorrectly. I can see the qualitative difference between operator overloading and monads. That's why I suggested to transfer the core idea of monads into more mainstream languages to provide more "semantic" safety, so to say.

Thanks for the clarification.

Re: Make the Type System Do the Work

#137

Post by edderly »

jimmaswell wrote: post #111
edderly wrote: post #20

In some environments beware of creating new types and objects: http://developer.android.com/training/articles/perf-tips.htm...

This seems to paint the JIT as something that hurts performance instead of helps it, is that true on Android?

It relates to the behavior of the garbage collection scheme used by dalvik which is a mark and sweep approach. When the GC runs, that’s all the VM is doing. It’s pointed out that a generational garbage collector would be more efficient allocating memory presumably there is a trade off in terms of the overall memory footprint.

Re: Make the Type System Do the Work

#138

Post by eloff »

hdevalence wrote: post #48
eloff wrote: post #26

Did anyone else recoil in horror at how a simple function is turned into a type hierarchy? This is everything that's wrong with Java to me. Classes are all fine and well, but don't take it to extremes. Maybe the examples were just too trivial, but it really is a far greater evil than just using well named variables and a simple conversion function.

Your problem isn't with expressive type systems, it's with languages whose type systems are not sufficiently expressive , though. Well-named variables are interpreted and checked by the programmer; well-expressed type constraints are interpreted and checked by the compiler. Guess which one makes fewer mistakes?

Yes, I'm happy to offload as much as possible to the compiler as long as it doesn't involve hundreds of lines of unnecessary classes and interfaces. That's just wrong.

Re: Make the Type System Do the Work

#139

Post by taeric »

tel wrote: post #135
taeric wrote: post #129

Earlier quoted context omitted.

My point is pretty much about the "a bit more noise in the syntax." And qsort will only work on array types, something that is typically shunned by people trying to "do all of the work with the type system." Consider the types for "NonEmptyList" and such. Is it neat when these work? Certainly. Do I think they pay obvious dividends in the effort increase? Not so much. I am open to the argument, but I have yet to see a…

Again, that noise is entirely an artifact of purity and syntactic choices, not the types. I'm not sure exactly what you're arguing for here, but I can explain a use case of NEL—when you consume it you don't have to check the for emptiness. That means that you can eliminate an entire branch of code, either locally or in exception catching, or an entire failure mode. Frequently people just throw those checks in and the…

My argument is that as you get more types that cover states or behavior of your program, one typically finds more code.

Is there an argument that these are beneficial? Of course there is. I just have not been privy to an example where it carried its weight.

Take the not-empty list. Typically the "cost of checking for empty" is so negligible that to push that thinking into the compiler just doesn't lead to any gains. Not even just marginal gains. It is nigh unmeasurable.

Compound this with similar types over the state of any other object, and you have an explosion of types that becomes unwieldy. Account, NotEmptyAccount, OverdrawnAccount, DrawingInterestAccount... It gets to be just crazy. Especially in areas where you don't care about any of those details, but now have to account for an inheritance tree.

And then you get into the fun of having to logic not just about how the actual program works, but how the interaction of various types works.

So, you keep saying the syntax I was referring to was due to purity. Which is kind of the point. These languages use syntax and types to help ensure purity. Which makes them more to handle for some algorithms. Less for others. And then just hard to really know the true computational cost for a lot.

Which is all to say that it is a design tradeoff. And should be undertaken as an informed decision. Not a "let the type system do the work" kind of one. More of one that "this is so important we need to make sure we can afford the cost of pushing it into the type system." Or, if you would prefer "this particular instance is so cheap to push to the type system, we should do so."

Re: Make the Type System Do the Work

#140

Post by tel »

taeric wrote: post #139
tel wrote: post #135

Earlier quoted context omitted.

Again, that noise is entirely an artifact of purity and syntactic choices, not the types. I'm not sure exactly what you're arguing for here, but I can explain a use case of NEL—when you consume it you don't have to check the for emptiness. That means that you can eliminate an entire branch of code, either locally or in exception catching, or an entire failure mode. Frequently people just throw those checks in and the…

My argument is that as you get more types that cover states or behavior of your program, one typically finds more code. Is there an argument that these are beneficial? Of course there is. I just have not been privy to an example where it carried its weight. Take the not-empty list. Typically the "cost of checking for empty" is so negligible that to push that thinking into the compiler just doesn't lead to any gains.…

I agree completely that it's a tradeoff. I also only bring up purity to suggest that other strongly typed, impure languages could solve this with less trouble.

NEL is a particularly interesting point of compromise. I don't think it carries its weight very frequently at all, though I have used it very effectively in a few cases. I also think the burden of type hierarchies as you're describing isn't much felt in Haskell. You typically don't build large taxonomies, or taxonomies at all, in a language without subtyping.

The only place where I see taxonomies forming at all is in `lens` and there they are used to great effect.

Post reply on HN