Hacker News Reader

Comment by tunesmith | Hacker News Reader

Is the combination of sum types and product types... sufficient in some way that product types alone are not? I have the sense it is but I'm not putting my finger on how.

View on HN

Yes. Product types (i.e. tuples) force you to consider all possible combinations of things, and the types have to be the same across all variants.

This means that there are certain states that may be impossible in practice, but possible to represent in your data. This can lead to unnecessary code at best, or undefined behaviour and bugs at worst.

For example, let's say we want to model loading data from a server.

With ADTs:

    type WebData
        = NoRequest
        | Loading
        | Failure HttpError
        | Success MyData

With product types only (and enums), how would we reconcile that the request could return an error _or_ data?

We could try something along the lines of:

    type WebDataStatus
        = NoRequest
        | Loading
        | Failure
        | Success
    
    type WebData = (WebDataStatus, Maybe HttpError, Maybe MyData)

Where the error and data fields are optional.

But in this case, it would be possible to have both error _and_ data fields populated. Not ideal!

It gets worse — technically speaking, your second ‘WebDataStatus’ is also a sum type! Admittedly most non-functional programmers would call it an enumeration, but nonetheless, a language without support for any sum types at all would also necessarily need to lack enumerations. (I therefore prefer to think of most non-functional programming languages as having an incomplete implementation of sum types rather than having no sum types.)

Yes, agreed!

I'm very sorry to say this, but… a category theory perspective points out a way in which they're not "sufficient". The exponential in a category theory context is basically "like a set of functions", in the same way that the product in a category theory context is "like a set of tuples". The fact that the notions are distinct means that functions are one example of an extremely important concept which is "not an ADT".

Category theory has a wealth of other concepts which suggest more general non-ADT properties, too. For example (ignore the jargon):

* Finite limits are a generalisation of finite products (i.e. the ADT product type), where we additionally require intersection types.

* Finite colimits are a generalisation of finite sums (i.e. the ADT union type), where we additionally require quotient types - and I'm not aware of any language, other than maybe Lean and friends, which has user-space quotients! Think of trying to define the rational numbers in user-space, but without forcing the user to deal with normalisation.

One thing that's neat is that with functions as exponentials (A^B being the type of functions taking a B and returning an A) all of the identities you learned in highschool algebra made up of only addition, multiplication, and exponents (division and subtraction don't quite have exact analogs) hold as isomorphisms. Writing the functions to take you in either direction can be an interesting exercise.

For instance, (A^B)^C = A^(B*C):

   (f) => (b, c) => f(c)(b)
   (f) => c => b => f(b, c)

which, of course, is currying and uncurrying.

That's an interesting question, but one that doesn't seem to have a really well defined answer.

The best I can come up with is that if you want to talk about the product of function types (A -> X) x (B -> X) then a sum type allows you to summarize this a single function type (A+B -> X). With just a product you could already do something similar for the type (X -> A) x (X -> B) which is equivalent to (X -> AxB), but with a sum type you have the dual variant as well.

And I suppose that with sum and product types together you can kind of express BNF like rules directly in the type system. Which makes things like expressing syntax trees a hell of a lot cleaner.

That said ultimately a type system is just a part of the language you can use to express certain rules, you can usually still decide on your own rules you'll just have to enforce them manually.

Product types + nullability is the same as sum types if you treat it that way, but it's less nice because the data representation in memory will not be as compact, and you won't get any guarantees from your language that you didn't fuck up (set less or more than exactly one field). Plus also you have to use comments to indicate your intention.

Relatedly, a single field of an interface type + the ability to cast to a concrete type is very similar to a sum type; Go programmers will use this trick sometimes.

Sum type:

I can be A | B | C.

Interface thype:

I am ILetter. Types A, B, C implement ILetter.

Plausible in memory representation of sum type value: 8 bits for the type tag, plus max-size(A,B,C) bits for type.

Plausible in memory representation of interface type value: 64 bits for the type pointer and 64 bits for a pointer to A, B or C.

(Not as nice as the sum type!)

Yes, for the same reason that if you want to do logic, you'll need both the "and" and "or" operators; neither "and" nor "or" alone suffice.

This is not true for classical logic, because AND can be written using NOT and OR using DeMorgan's law.

OR alone is insufficient because you still need NOT (or AND and ⊥). You can also encode sum-like behavior using negation and products (a continuation consuming a pair of continuations).

Recursive sum-of-products types also let you do things that sums and products alone cannot.

Reply on news.ycombinator.com