Live data from Hacker News

Make the Type System Do the Work

nathan.ca

31–40 of 141 posts

Re: Make the Type System Do the Work

#31
post #27

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…

This is incredibly common in embedded programming. Lots of times you'll have some binary packet come over the wire, the first field is a packet type specifier, you can then just cast the rest of your byte buffer to the proper type. It is very unfortunate that C (and until recently C++) did not have a way to specify the size of enums. Basically this has resulted in crappy #defines being used for far too many years. I…

I agree, this typed enum in C++11 made a MachO manipulation library much nicer.

Re: Make the Type System Do the Work

#34

To take this to the current state of the art, look at Haskell, Agda, and Idris. Latter two being dependently typed. Steps for learning Haskell: https://gist.github.com/bitemyapp/8739525

Any recommendations for web programming in Haskell?

I highly recommend taking a look at the Happstack Tutorial. There's both a Lite version [1] and a full Crash-Course [2].

[1] http://happstack.com/page/view-page-slug/9/happstack-lite [2] http://happstack.com/docs/crashcourse/index.html

Re: Make the Type System Do the Work

#35

To take this to the current state of the art, look at Haskell, Agda, and Idris. Latter two being dependently typed. Steps for learning Haskell: https://gist.github.com/bitemyapp/8739525

What are your impressions of the three languages? Personally, I'm learning Haskell first, because Haskell is the most popular of the three and there is plenty of good learning material. As far as Adga and Idris go, I think Idris looks more appealing.

Learn Haskell first. When you've gotten your head at least partially around it then the latter two become much more approachable. Programming in a dependently typed language is not simple if you're not used to the algebraic methods they're based on. That said, Idris seems to be aiming to be much more "practical" than Agda.

Also, all that said, once you start getting to the point where you're really getting comfortable with Haskell types you absolutely should learn Agda or Idris since they do advanced types far better than Haskell does. Many confusing Haskellisms become obvious in the light of Agda/Idris.

Re: Make the Type System Do the Work

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

What is missing the rest of the program that could be using temperature hundreds of times scattered throughout the calculations and UI. A small type hierarchy provides type safety for all that other code and is certainly less prone to errors than well named variables and simple conversion functions.

The example is bit too trivial as the hierarchy doesn't provide much value. I would assume the base class would actually provide some useful functionality that isn't in this example or it could be eliminated entirely.

Re: Make the Type System Do the Work

#39
post #28
post #24

The big problem (other than verbose code) with rolling up stuff into classes in C++ is that performance suffers. Many platforms will not pass small structs efficiently. Inspired by Haskell's newtype, I drafted a proposal for C++14 which would have introduced native newtype to C++, but it got rolled into an omnibus paper (n3635) and appears to have been forgotten. The proposal is modelled on strong enums, but generali…

I don't think there's going to be any performance difference at all compared to the basic case, which actually is another reason why this is so good. Ultimately, all these struct just hold a double, which means that in memory they're exactly a double and nothing more, there's no type tag or anything like that. And all the code is static so there is no vtable, just the double value. The compiler does the rest, not the…

It can make a difference due to weird ABIs. For example, in the ARM procedure call standard, 64-bit values can be returned in r0 and r1, but 64-bit structures can't (no matter whether they contain two 32-bit values or just one 64-bit value). However, I'd call that fairly niche - it's hard to imagine an application that would notice a significant performance difference.

Re: Make the Type System Do the Work

#40

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?
Post reply on HN