[HN Gopher] Algebraic data types: things I wish someone had expl...
___________________________________________________________________
Algebraic data types: things I wish someone had explained about FP
Author : weatherlight
Score : 68 points
Date : 2021-10-12 15:03 UTC (7 hours ago)
(HTM) web link (jrsinclair.com)
(TXT) w3m dump (jrsinclair.com)
| ldiracdelta wrote:
| """
|
| 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!
| VHRanger wrote:
| YOU DONT NEED TO SHOUT THE TITLE
| [deleted]
| hdjjhhvvhga wrote:
| Using caps in titles is a centuries-long tradition. Labeling
| caps as shouting has just a few decades.
| Zababa wrote:
| Try your reasoning with how people call people with a
| different skin color and you'll understand the problem.
| _dain_ wrote:
| total non-sequitur
| Zababa wrote:
| Depends on how you see it. If you look only at the
| "usage" part, I think my point is fine. There's another
| part of the equation, which is the media. Internet and
| printed text (which was what used full caps titles) are
| not the same, so applying the printed text rules to
| internet text doesn't make sense. But my point about
| usage evolving still stands. Things change more quickly
| these days than before. So comparing simply the length of
| time something existed is a fallacy. I don't know if it's
| possible to compare this exactly, but I would suppose, in
| terms of "evolution of culture/usages", an internet year
| is worth at least a decade of printed text before the
| internet.
| marcosdumay wrote:
| > 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.
| gmfawcett wrote:
| 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.
| open-paren wrote:
| Discussed previously
|
| - https://news.ycombinator.com/item?id=21571938 (November 19,
| 2019 -- 242 points, 112 comments)
| TheGoodBarn wrote:
| Never learned so much from a background image that looks like a
| tortilla
| tobr wrote:
| I think it's a depiction of the average skin tone of an FP
| programmer.
| LandR wrote:
| 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.
| alextheparrot wrote:
| Was just going to say how much I loved it, guess that's art.
| kevbin wrote:
| I dig the Beagle Brothers' aesthetic.
| SahAssar wrote:
| 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.
| weatherlight wrote:
| 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.
| Smaug123 wrote:
| 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.
| tjpnz wrote:
| That site's beautiful.
| _dain_ wrote:
| Sadly it's totally incompatible with dark mode so it's painful
| to read.
| IshKebab wrote:
| 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.
| tunesmith wrote:
| 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.
| bobbylarrybobby wrote:
| 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.
| dllthomas wrote:
| 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.
| Smaug123 wrote:
| 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.
| truculent wrote:
| 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!
| bradrn wrote:
| 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.)
| contravariant wrote:
| 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.
| dilap wrote:
| 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!)
___________________________________________________________________
(page generated 2021-10-12 23:01 UTC)