Live data from Hacker News

Make the Type System Do the Work

nathan.ca

101–110 of 141 posts

Re: Make the Type System Do the Work

#101

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.

[deleted]

Re: Make the Type System Do the Work

#102

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…

To make it even better, you can declare classes that are exactly the size of your primitive type, and do things like endianness conversion for you. I will often even make functions that convert, e.g., a bid into a specific price type. Having all of the numerical quantities in your trading system strongly typed makes working on it much easier. The strong type system that enables this, without sacrificing any runtime speed is my favorite part about C++.

Re: Make the Type System Do the Work

#103
post #41

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…

Type checking always happens at some point in every language, dynamic or static. At some point, a routine gets executed on some form of data, and the success of that routine is predicated on the data being of the right type. In dynamic languages, you end up writing a whole raft of tests that are not much more than type assertions that are otherwise done for you by the compiler in a statically typed language. For stat…

I don't think you really wrote anything I did not acknowledge. Yes, types are a form of complete test over the shape/type of data that they encode. If you can encode your data with the correct type, it will go a long way to making sure you don't have errors in the types.

However, I take issue with this statement: "For statically typed languages, the type check is a type of test that just so happens to be very succinct and easier to write than it is to skip. " For the simple cases, I agree with this. But when you see the type gymnastics that some programs go through to guarantee some traits, it is hard to agree with any claim of "easier to write." Consider a "true" quicksort in haskel[1].

My assertion was that the "hard part" of programming is often in the logic, not necessarily the shape/type of the data. When you see attempts at getting the logic of a program into the type system, things start to take a turn for the worse. Really worse when you find you have many types that all encode the same type of data. (Consider the metric system debate.)

My point about "having the right tests" is that sometimes you only care/have the knowledge to think about/whatever certain scenarios that are either likely or guaranteed to happen. Pushing everything in the type system implies that you had the energy to think of and consider everything. My assertion is often you don't have that time/energy.

So, sure, you will have the "right tests" in that scenario to an extent, since you will have all tests. However, I wonder if most programs couldn't work out with a much smaller subset of those tests.

A direct analogy for the point I am making is physics. Classical/Newtonian physics break down and don't work at a level. Worse, they rely on a lot of simplifications and actually describe what is happening moreso than how/why. Yet, for a large portion of calculations that people will do, they work. I grant that encoding all of the assumptions into the calculations will make them more accurate, but often you don't need that level of accuracy. And they definitely make them harder to understand.

[1] http://www.haskell.org/haskellwiki/Introduction/Direct_Trans...

Re: Make the Type System Do the Work

#104
post #80

Earlier quoted context omitted.

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.

Haskell still has some boilerplate - actually quite a lot if you don't use -XGeneralizedNewtypeDeriving (which has known problems when used with other extensions). With newtype deriving, this is about as simple as it gets: {-# LANGUAGE GeneralizedNewtypeDeriving #-} class Degrees deg where toK :: deg -> K fromK :: K -> deg newtype K = K { unK :: Double } deriving (Show) instance Degrees K where toK = id fromK = id ne…

GeneralizedNewtypeDeriving's problems are fixed in the newest GHC which just had it's first RC a few days ago. It introduces a "roles" system which tracks which types are allowed to use GND without breaking abstraction boundaries. Roles are mostly invisible to end users as well.

Re: Make the Type System Do the Work

#105
post #103

Earlier quoted context omitted.

Type checking always happens at some point in every language, dynamic or static. At some point, a routine gets executed on some form of data, and the success of that routine is predicated on the data being of the right type. In dynamic languages, you end up writing a whole raft of tests that are not much more than type assertions that are otherwise done for you by the compiler in a statically typed language. For stat…

I don't think you really wrote anything I did not acknowledge. Yes, types are a form of complete test over the shape/type of data that they encode. If you can encode your data with the correct type, it will go a long way to making sure you don't have errors in the types. However, I take issue with this statement: "For statically typed languages, the type check is a type of test that just so happens to be very succinc…

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 Python code---it's literally just a syntactic swap.

    def lscan(ary, p, h, i):
      if (i 

Re: Make the Type System Do the Work

#106
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.

no. This was an example to illustrate a point. Use your imagination to find real uses of this approach. And what's wrong with type hierarchies anyway?

Re: Make the Type System Do the Work

#107

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.

Re: Make the Type System Do the Work

#108
post #82

Earlier quoted context omitted.

I think the examples are just too trivial (or in this case, aren't extended to a greater library). Where they really come in handy is if you're using the types all over the place. If I were to create a Degrees class (with Celsius and Fahrenheit) just for representing it in a UI, I'd call it crazy. But if I'm doing conversions all over the place or creating a library for others to use, I would think the plumbing is wo…

If you are "doing conversions all over the place", you are looking at a fundamentally flawed code design that costs you performance. Ensuring consistency of coversions here is like painting a house whose roof's on fire. C/F example is synthetic, but it doesn't make it any good - if you are operating with data that can be expressed in different units, then pick a single unit, stick with it throught the code and conver…

[deleted]

Re: Make the Type System Do the Work

#109

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…

The type of a trig function is just a scalar, no unit.

Re: Make the Type System Do the Work

#110

Does static typing have inherent costs? For instance, there are some desirable properties often present in dynamic languages like hot code loading, or the ability to make code updates independently. Not many statically-typed systems are good at these things, or at least the static typing doesn't work well across boundaries (like a network, etc.). Can these be reconciled? Can something have all of the benefits of, say…

There's Cloud Haskell which is an attempt to do Erlang style distributed concurrency in Haskell. For non-distributed concurrency, you can already get away with using Haskell's green threads and channels. Furthermore, there's the beginning of a hot code swapping system in GHC now, but it's not terrifically popular at the moment---it was built for a particular use at Facebook and hasn't gotten too far from there.

It's worth talking about why Cloud Haskell is tough, though. The primary issue is that Haskell doesn't have any kind of transparency into functions---if you are given a type of `(a -> b)` there's no way to examine what it is on the inside, no concept of source that could be sent to another node.

This limits the kinds of messages and spawning that can happen in a distributed Haskell system. The Cloud Haskell project is working to remove as much of this limitation as possible, though.

Post reply on HN