Algebraic data types: things I wish someone had explained about FP (2019) | Hacker News Reader

Algebraic data types: things I wish someone had explained about FP (2019)

jrsinclair.com

92 pointsweatherlight38 comments

I would add only one thing to the article. Algebraic data types are so great because they are so dumb. ADTs are inherently stateless, for example (as long as you don't put stateful things inside them). This makes them extremely easy to reason about: they're no harder to reason about than an integer is.

Never learned so much from a background image that looks like a tortilla

I'm finding the code snippet colours and fonts really annoying to read.

Actually, even the main text on the site with the `blotchy` background is hard to read for me.

At least FF reader mode makes it readable.

Was just going to say how much I loved it, guess that’s art.

I dig the Beagle Brothers’ aesthetic.

"""

But, you might also notice a functional programmer over there. The one with a smug look and condescending smile on their face. And after bracing yourself, you ask them 'What’s so amusing?'

[...]

Now, let’s assume you manage to refrain from physical violence.

"""

Hilarious!

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.

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.

Discussed previously

- https://news.ycombinator.com/item?id=21571938 (November 19, 2019 — 242 points, 112 comments)

> And you’d be right. Arrays, Objects, Maps, WeakMaps, and Sets are all algebraic data types.

Hum... I have a very strong impression that it's only the type system that can be algebraic. For single types, the name doesn't make any sense.

It's like asking if "2" is a vector. You can have a vector space where it's an element, but without context, the question doesn't make sense.

You can think of data structures like arrays in an algebraic way. Consider the type of "arrays of booleans, of length 8." This type is in 1:1 correspondence with the type of "8-tuples of booleans", i.e., it's a product type. Like any algebraic type, we can compute its cardinality: there are 2^8 values in this type. Similar thinking can be applied to the other (abstract) types that you mentioned, although it helps to have information about their internal structure.

Although if you just consider 1-1 correspondence, then basically any type with a countable number of inhabitants is isomorphic to the integers (when the type is viewed as a set of inhabitants). And that makes sense, because we can always just take the binary representation of any data type in memory.

And if you just have unit type, empty type, sums and products, then you can only make types with finitely many inhabitants. Adding the integers to that makes you able to make any countable type, but potentially in a trivial way as described above.

Therefore just viewing the types as sets does not give a very satisfactory basis for determining whether a type is an "algebraic data type". Maybe we could do better if we consider some more aspects related to type safety, but it's not immediately obvious to me how.

"Any type with a countable number of inhabitants is isomorphic to the integers" --> I assume you mean "countable" in the sense of "countably infinite." Clearly the finite types can't be put into correspondence with the integers.

I agree that viewing the types just in terms of their cardinality isn't terribly insightful. But I do think it's helpful to realize that arrays aren't some other kind of thing that's separate from ADTs, and that you can bring the same algebraic reasoning tools to bear on arrays (and other pedestrian data types).

My point was basically that you can implement the array abstract data type (creation, set value at index, get value at index) in a lot of ways, including by using ADTs (although it seems hard to get an O(1) implementation if you use ADTs, unless you have some clever compiler or language mechanism). But just because you can implement arrays in terms of ADTs doesn't mean that arrays ARE ADTs.

Now that I think of it a bit more, it seems to be a category error to say that a "set" or an "object" or a "dictionary" is an algebraic data type. Algebraic data types are types (values) constructed out of simpler types (values) in a certain way, and that can be deconstructed in a way that mirrors the way they were created. You can implement various APIs/interfaces on top of that, including dictionaries and sets and whatnot.

But my point was that you can do the same on top of just integers (assuming you have the common integer operations), and you could even package it up in a type safe way so that the fact that you used integers in the implementation does not leak out, assuming the language has some modularity/abstraction mechanism so that you can make stuff private to a module. But based on this it seems to be a stretch to say that dictionaries are REALLY just integers or bitstrings.

And just like you probably wouldn't want to bring "integer reasoning" to bear on dictionaries, you probably don't want to use ADT reasoning to reason about dictionaries either. Because then you are really reasoning about the concrete implementation details and generally speaking those details are hidden from clients of the dictionary (and subject to change at any time).

I think I see where you're going, and it seems completely reasonable to me. :) I like the distinction you've drawn between implementation and interface in your dictionary and abstract-array examples. I don't think that abstract interfaces make algebraic reasoning completely impossible, e.g., you could represent unknown implementation details as variables (or even functions). But it's good to be clear re: what questions you're asking, the level of abstraction you're thinking at, and whether any analogy to ADTs is useful or simply a distraction.

I think a nice corollary to your second point is that the existence of an isomorphism between two collections doesn't mean they are the same thing. This is easy to see when you discuss integer reasoning. E.g., if we have a infinitely countable data type, so we have an isomorphism to Z. But that doesn't automatically make our data type a ring (not in any meaningful sense).

Yes, you can think of them in an algebraic way. You also can not think of them in an algebraic way.

I guess you explained it better than me. What makes them algebraic is the way you think about them and the full set of types they are part of. For the types themselves, the name is meaningless.

OK, I see your point better now. You're saying that reasoning about a type algebraically is more of a perspective, not a fundamental statement about the type itself. I think I could get behind that. :)

For what it's worth, not all functional languages emphasize the ADT notion per se. E.g., the Ocaml manual generally talks about records, tuples, and variant types; "algebraic" really only comes up with GADTs are discussed.

Typescript has a fairly official way to do sum types (less poncily known as tagged unions):

https://www.typescriptlang.org/docs/handbook/unions-and-inte...

Might make the example a bit clearer.

Even if the title is shown in uppercase in the article it is handled with `text-transform: uppercase;` so I'm not sure how it became uppercased here unless the poster did it manually.

I literally copied I except i shortened the functional programing bit to FP. (char length)

I use the Grammarly Chrome plugin, which sometimes causes text to behave differently when it's copied and pasted.

The 'class Digit' example has 11 possible values, not 10:

  > d = new Digit('')
  Digit { value: NaN }

This needs (2019) in the title since the post was written/published in 2019.

That site's beautiful.

Sadly it's totally incompatible with dark mode so it's painful to read.

YOU DONT NEED TO SHOUT THE TITLE

Using caps in titles is a centuries-long tradition. Labeling caps as shouting has just a few decades.

Reply on news.ycombinator.com