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

51–60 of 141 posts

Re: Make the Type System Do the Work

#51

Post by jeffdavis »

"'Dog is-a Mammal' ... actually fairly sound"

I disagree in the context of OOP inheritance.

(This example uses shapes, because the idea of mutating mammals gets a little strange.)

Let's say you have a Circle class and an Ellipse class. A Circle inherits from an Ellipse, of course, because a Circle is-a Ellipse. By specializing as a Circle, we get extra reader methods such as getRadius(). Great.

But what about mutators? For an Ellipse, it may have a mutator called squash() that holds the major axis constant and halves the minor axis. But that leaves us with a problem, because circles can't be squashed while remaining circles.

Let's say we have a program like:

    void f1() {
      Circle myCircle(10.0);
      f2(myCircle);
      cout
Inheritance says that f2 must also accept a Circle. But what happens when we try to squash it? We can either throw a runtime error there, or we could let the squash succeed and the getRadius() in f1() will fail.

Although a Circle value is an Ellipse value, a Circle variable is not an Ellipse variable. In fact, inheritance for variables should go in the opposite direction as inheritance for values, because an Ellipse variable can certainly hold a Circle value.

Re: Make the Type System Do the Work

#52

Post by pbsd »

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…

This is a neat trick, but it will segfault in architectures where alignment is enforced (like MIPS, ARM, etc) if the input buffer is not suitably aligned. One relatively cheap way to sidestep this is to memcpy into a stack-allocated struct:

    Data data;
    memcpy(&data, raw_buffer, sizeof data);
    switch(data.data_type)
    // ...

Re: Make the Type System Do the Work

#53

Post by platz »

magic_haze wrote: post #46
platz wrote: post #40

Earlier quoted context omitted.

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.

Ah, I see. Looking at how something similar was implemented in Haskell, they used phantom types and functional dependencies (in the type system) to achieve this - I'm not sure F# has those capabilities.

Re: Make the Type System Do the Work

#54

Post by gizmo686 »

eropple wrote: post #45
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.

Would it be possible to do this as a type-alias type thing that disapears at compile time? As far as I am aware, Java has no support for such type aliasing, but it should be possible to add a pre-compiler phase to your build process that replaces these types with what they are aliases of. The only part of this that seems complicated is the type checker, which would need to be aware of the difference between AccountId and long.

Re: Make the Type System Do the Work

#55

Post by coolsunglasses »

MaxGabriel wrote: post #32
coolsunglasses wrote: post #10

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?

Just getting started? Scotty.

That having been said, learning how and why Snap and Yesod do their thing is advisable.

I don't think there's any real reason not to take some time with Happstack, Scotty, Yesod, and Snap in turn and just see which appeal to you the most.

Scotty is analogous to something like Sinatra and reuses the existing WAI/Warp (think Rack/Ring/WSGI) work that was originally done for Yesod.

Re: Make the Type System Do the Work

#56

Post by coolsunglasses »

dustingetz wrote: post #15
coolsunglasses wrote: post #10

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

yo switch the gist to markdown to get word wrap

Done.

Re: Make the Type System Do the Work

#57

Post by coolsunglasses »

Buttons840 wrote: post #18
coolsunglasses wrote: post #10

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.

Well Haskell is the "practical" choice but there's a lot to learn from Agda and Idris if your interest is in a helpful type system - the topic of the original post.

Re: Make the Type System Do the Work

#58

Post by vinkelhake »

laureny wrote: post #50
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++.

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

Variants of this comment are often seen.

For any given feature, there's going to be a language that shines in that particular area. However, choice of language rarely comes down to a specific feature. There's usually a multitude of aspects that needs to be considered - some of them aren't even technical.

Re: Make the Type System Do the Work

#59

Post by axman6 »

laureny wrote: post #50
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++.

That seems like an orthogonal issue to me. The assert is to ensure that the data type matches some external requirement; a quote is a structure that as 28 bytes long, and if something changes to make a Quote not 28 bytes long, you'll be told. If it weren't there, the algebraic data stuff would still work fine.

Edit: I say this as someone whose primary language is Haskell

Re: Make the Type System Do the Work

#60

Post by MichaelGG »

magic_haze wrote: post #46
platz wrote: post #40

Earlier quoted context omitted.

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.

Is that a real issue? They could generate struct types, but why take the performance loss? It only affects people trying to reflect over the unit of measurement types.

Additionally, phantom types in F# can make wrapping other types (like int -> AccountId) rather succinct.

Post reply on HN