Make the Type System Do the Work • Hacker News Board

Re: Make the Type System Do the Work

#41

Post by taeric » Thu, Feb 06, 2014, 5:03 AM UTC

I think the major problem this runs into is that it doesn't necessarily help with the actually hard parts of programming.

That is, sure, mistakes have been made with units. More mistakes are made in other areas, though. Usually amusingly more basic areas.

The question seems to be whether encoding at the type level will help with these areas. It seems the conflict is the idea that fully proving a solution is superior to partially proving it.

Laudable, to be sure, but anyone that has attempted to prove that quick sort works knows, it isn't easy. Just understanding the shorter versions of some programs takes a fair bit of brain power as it is. Understanding the fully specified version can be orders of magnitude more complicated.

So, I am left wondering if it isn't enough to stop at "passes all the tests." Especially if you have the correct tests.

And eventually one wonders whether the "correct tests" includes more stringent types. Maybe it does. Maybe it doesn't. Likely depends on the situation, is my bet.

Re: Make the Type System Do the Work

#42

Post by cmbaus » Thu, Feb 06, 2014, 5:03 AM UTC

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.

yes.

Re: Make the Type System Do the Work

#43

Post by 10098 » Thu, Feb 06, 2014, 5:05 AM UTC

chrisaycock wrote: post #23

This article uses inheritance in C++ to ensure the types line-up, but I have really taken a shine to algebraic data types for my firm's data feed handlers. Here is an example in C++11 that implements a market-data spec line-for-line. #pragma pack(push,1) struct Quote { char symbol[16]; uint16_t bid; uint32_t bidsize; uint16_t ask uint32_t asksize; }; static_assert(sizeof(Quote) == 28, "Quote size wrong"); struct Trad…

My previous job involved dealing with financial data feeds, can confirm. We used that trick all the time.

Re: Make the Type System Do the Work

#44

Post by greatsuccess » Thu, Feb 06, 2014, 5:09 AM UTC

chrisaycock wrote: post #23

This article uses inheritance in C++ to ensure the types line-up, but I have really taken a shine to algebraic data types for my firm's data feed handlers. Here is an example in C++11 that implements a market-data spec line-for-line. #pragma pack(push,1) struct Quote { char symbol[16]; uint16_t bid; uint32_t bidsize; uint16_t ask uint32_t asksize; }; static_assert(sizeof(Quote) == 28, "Quote size wrong"); struct Trad…

Its clever but it doesnt scale to writing systems. Its just a hack.

Re: Make the Type System Do the Work

#45

Post by eropple » Thu, Feb 06, 2014, 5:23 AM UTC

EdwardDiego wrote: post #2

> The only problem is that you end up with a variable that fails to describe itself better than “I’m a number”. Our application servers need to know about updated entities, so we broadcast notifications when an entity has been updated - but we prefer to leave it up to the individual applications to retrieve the updated entity as they see fit. So we're often dealing with numerical ids of entities, and we've had a few…

This method also create a lot of object churn. For reasonably small systems that can be okay, but you have to be mindful of it.

Re: Make the Type System Do the Work

#46

Post by magic_haze » Thu, Feb 06, 2014, 5:27 AM UTC

platz wrote: post #40

moron4hire wrote: post #21

I did just this very thing in C# a few months ago[1]. The problem I had was that it gets out of hand very quickly. I wanted to be able to divide distance by time and get speed out of it, but it is extremely difficult to satisfy all of the M-to-N relationships between types and still end up being usable. I ended up abandoning it for the project I'm building, as I wasn't too clear on what the type of a secant of an ang…

F# has this, I wonder how they did it?

They couldn't do it. The compiler does static verifications that, say, a value of type Meter when divided by a value of type second results in a value of type Meter/Second, where '/' is a custom concept built into the F# compiler. The .NET runtime knows nothing about these custom types.

Re: Make the Type System Do the Work

#47

Post by hdevalence » Thu, Feb 06, 2014, 5:33 AM UTC

skybrian wrote: post #16

This is a good trick but it needs to be used judiciously or you'll end up with lots of boilerplate. I particularly like Go's type system, though, because it makes it very simple: type celsius float64 There's no overhead and it doesn't attempt to prevent you from doing any calculations as a float64; the type checking just prevents direct assignments from a celsius type to another type.

On the other hand, Go doesn't have a way to write code that abstracts over types, and my (albeit limited) experience with Go is that most of the boilerplate is due to the language's poor type system. If you use a language with a better type system (Haskell is the first that comes to mind, though there are others), you can actually do this sort of thing without the boilerplate code.

Re: Make the Type System Do the Work

#48

Post by hdevalence » Thu, Feb 06, 2014, 5:36 AM UTC

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?

Re: Make the Type System Do the Work

#49

Post by tomlu » Thu, Feb 06, 2014, 5:46 AM UTC

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.

It's nice how in Go you can alias a type to int, yet it is its own distinct type with compile time checks and explicit conversions. Definitely takes away all the boilerplate.

Re: Make the Type System Do the Work

#50

Post by laureny » Thu, Feb 06, 2014, 5:47 AM UTC

chrisaycock wrote: post #23

This article uses inheritance in C++ to ensure the types line-up, but I have really taken a shine to algebraic data types for my firm's data feed handlers. Here is an example in C++11 that implements a market-data spec line-for-line. #pragma pack(push,1) struct Quote { char symbol[16]; uint16_t bid; uint32_t bidsize; uint16_t ask uint32_t asksize; }; static_assert(sizeof(Quote) == 28, "Quote size wrong"); struct Trad…

> static_assert(sizeof(Quote) == 28, "Quote size wrong");

A good reminder that trying to "let the types do the work" in C++ is an oxymoron.

If you're so keen on algebraic data types, there are languages much better suited to that than C++.