Comment by jallmann | Hacker News Reader

Comment by jallmann | Hacker News Reader

Parent Full thread

Nice article, I never considered the duality of product and sum types before.

The importance of effective ADT usage is generally under-emphasized when discussing the benefits of statically typed FP languages* like OCaml and Haskell — even though it is the way to maximize the utility of such languages, IMO.

With the right data representation, composability improves and algorithms fall into place naturally. This is further enhanced by a language like OCaml — since the compiler catches type errors and non-exhaustive matches on ADTs, any bugs are likely holes in your application model.

There are many benefits in using ADTs, modules and other type-system features to guide your program design. Others have described those benefits very well already — just read anything by Yaron Minsky or Jane Street.

* Data modeling is critical for any problem domain, and statically typed, non-FP languages (Java, C++, etc) certainly have facilities to encourage effective modelling, but languages in the vein of OCaml and Haskell really push to make the type system do as much work as possible.

I wrote a post emphasizing the duality of products and sums. It's a really deep subject!

http://tel.github.io/2014/07/23/types_of_data/

I loved reading this the other day. Thanks again for writing it. I'll be coming to this post often, I think.

I'm glad you enjoyed it! I'm working on one or two most posts in this vein in order to introduce quantified types and recursive types. So: more to come!

ADTs are a bit like garbage collection: they originated in functional languages, they provide huge productivity gains, and they are (in theory) very easy to prop onto any kind of language. You can imagine a variant of C that has ADTs---they'd just be called tagged unions.

ADTs and pattern matching go together. Having tagged unions is awful without a good way to discriminate upon them.

Switch statements are ok but not typesafe since nothing prevents you from desynchronizing the tag and data

If you think of ADT definitions as defining how you construct types then you get a natural method for destructing them or using them automatically. This could be pattern matching or it could be explicit functions

More concretely, even without pattern matching, so long as, for instance, these three functions are all defined

    pair : a -> b -> Pair a b
    pi1  : Pair a b -> a
    pi2  : Pair a b -> b

You'll be equivalently expressive.

C already has product types, so it's sums that are more interesting, and indeed the destructors for sums are harder in C. The constructors

    in1 : a -> Sum a b
    in2 : b -> Sum a b

are no problem, but the destructor

    sum : Sum a b -> (a -> c) -> (b -> c) -> c

needs first-class functions.

There's a difference between "having a destructor" and having a first-class representation of it. For instance, basically every language has a destructor for booleans—it's just if.

The trick is that unless you have first-class functions you probably cannot reify such a destructor. It always just lives in your syntax.

On the flip side, that's really what it means for a language to, say, lack sum types. It's not that the language doesn't have the ability to have choice, it's that it lacks the ability to represent choice in data. In other words, you probably can eliminate choice using if/switch/case/what-have-you but you can't construct it.

Right. I interpreted your previous comment as meaning that you don't need pattern matching because you can just used the (reified) destructor. Conversely, you can avoid the higher-order destructor using pattern matching.

Yep! They are "the same".

C already has sum types, just slightly sloppy ones (as unions aren't required to have a tag).

Reply on news.ycombinator.com