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.
Make the Type System Do the Work
101–110 of 141 posts
Re: Make the Type System Do the Work
#102This 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…
Re: Make the Type System Do the Work
#103I 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…
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
#104Earlier 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…
Re: Make the Type System Do the Work
#105Earlier 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…
def lscan(ary, p, h, i):
if (i Re: Make the Type System Do the Work
#106Did 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.
Re: Make the Type System Do the Work
#107I 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…
Re: Make the Type System Do the Work
#108Earlier 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…
Re: Make the Type System Do the Work
#109I 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…
Re: Make the Type System Do the Work
#110Does 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…
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.