[HN Gopher] The algebra and calculus of algebraic data types (2015)
___________________________________________________________________
The algebra and calculus of algebraic data types (2015)
Author : thunderbong
Score : 100 points
Date : 2024-07-24 12:35 UTC (10 hours ago)
(HTM) web link (codewords.recurse.com)
(TXT) w3m dump (codewords.recurse.com)
| saltysalt wrote:
| That is such a great website! Amazing content throughout.
| cvoss wrote:
| I always love this topic.
|
| > Nat = 1 + Nat. This equation is clearly inconsistent, since
| x=1+x is false for all possible values of x.
|
| Ah, but no, my friend. That equation is false merely for all
| possible finite values of x. But why impose such a constraint?
| We've already been identifying a correspondence between certain
| types and the number of inhabitants they have. Nat has countably
| many inhabitants. And one more than countably infinite is
| countably infinite!
| empath75 wrote:
| Yeah because aren't the numbers associated with the types
| related to cardinality?
| Infinity315 wrote:
| > Nat has countably many inhabitants. And one more than
| countably infinite is countably infinite!
|
| Two sets having the same cardinality (number of inhabitants) is
| insufficient to prove that two sets are equal. There is an
| additional condition that they all share the same elements.
|
| I read 1 + Nat as: map each element in the Naturals to its
| successor (i.e. Nat - {0}). 0 is in Nat, but 0 does not exist
| in "1 + Nat" since it got mapped to 1.
|
| This would be true if the set we were working with were the
| Integers instead of the Naturals.
| srcreigh wrote:
| This is incorrect.. the equation represents the number of
| elements in Nat based on its definition.
|
| Integers could be Int = Nat | Neg Nat. So Int = 2 * Nat. Your
| logic would presumably interpret this as even naturals.. but
| ya
| zdragnar wrote:
| I'm always confused as to why people want to be able to do
| arithmetic with infinity. Infinity isn't a number.
|
| > countably infinite
|
| Countably infinite means you can count to any particular
| element of a set in finite time, even though there is no end to
| the pattern of elements in the set.
|
| You cannot count to infinity plus one in finite time.
| Smaug123 wrote:
| That's not the attitude which leads to inventing the negative
| numbers, for example! The ordinals are useful and it's very
| reasonable to call them "numbers"; and I'm told that the
| surreal numbers are useful, although I've never actually used
| them.
| gnulinux wrote:
| Infinity is not a number but transfinite numbers [1] like
| omega [2] or aleph-null [3] are. They are just as number as
| 0, 1, -5, 6/7, pi, i, or quaternion numbers. What _is_ a
| "number" is not well-defined, any mathematical algebraic
| object can be called a number with some justification.
| Mathematicians just don't do it anymore, they just call it "X
| Algebra" instead of "X Numbers" but there is no fundamental
| distinction. From this perspective, arithmetic with infinity
| is not only possible but also extremely useful for
| Programming Language Theory, e.g. for Dependent Type Theory.
|
| [1] https://en.wikipedia.org/wiki/Transfinite_number
|
| [2] https://en.wikipedia.org/wiki/Ordinal_number#Ordinals_ext
| end...
|
| [3] https://en.wikipedia.org/wiki/Aleph_number#Aleph-null
| empath75 wrote:
| A set is "countably infinite" if you can construct a one to
| one mapping from the set to the natural (counting) numbers.
|
| The natural numbers are of course countably infinite, but so
| are even numbers, prime numbers, fractions, algebraic numbers
| and lots of other kinds of numbers that people want to do
| arithmetic with. "Uncountably infinite" sets can't be put
| into a one to one correspondence with the naturals, no matter
| how you produce to produce such a mapping, it's always
| possible to produce a number in the set which wasn't part of
| it. Real numbers being the prototypical example of that, but
| the power set (the set of all the subsets) of the naturals
| is, also.
|
| People do arithmetic with all kinds of things that "aren't
| numbers". Math isn't restricted to working with numbers.
| xanderlewis wrote:
| Just to be pedantic: you mean 'one-to-one _and onto_ ',
| otherwise you're only capturing countability rather than
| being countably _infinite_.
| xanderlewis wrote:
| Countably infinite doesn't mean you can count to any
| particular element in finite time; such a definition would
| depend on an ordering which cardinality (and, in particular,
| countability) shouldn't.
|
| For example, uncountable sets can exhibit the property you
| mention: you count to x via the (very) finite sequence {x}
| for any element x of the set of real numbers.
|
| Conversely, countable sets (even if you restrict such
| enumerations to a certain ordering) don't in general have
| this property: ordering the integers by [x < y iff x < y (mod
| 2) or x < y if x = y (mod 2)] (that is, taking two isomorphic
| copies of the integers, identified with the even and odd
| integers respectively, juxtaposed side by side), the sequence
| {0,2,4,6, ...} fails to arrive at 1 no matter how far you
| count along. So there's an element we can't count to in
| 'finite time'.
|
| The property you seem to be alluding to, that 'the set admits
| a total order such that every element can be reached in
| finitely many steps starting at the first element' actually
| corresponds to the order type of the natural numbers -- often
| called o. It's countable, but there are many, many (in fact,
| uncountably many) more sets with this cardinality that don't
| have that property.
|
| The proper definition of 'countably infinite' is simply that
| the set can be placed in bijection with the natural numbers.
| This has nothing (directly) to do with ordering.
| taeric wrote:
| I am always torn when I see these discussions. Yes, I fully
| appreciate a lot of the easy algebra applies to some things. I
| further appreciate many of the optimizations that can be created
| by taking advantage of many of these.
|
| However, I have grown skeptical on its pedagogical use in
| programming. Specifically, I question if it is really how most
| people think in terms of programming.
|
| I further question if this is how most modelling considers
| things. An easy example would be chemistry. There are algebraic
| ideas in chemistry, but I would struggle to say how they look the
| same as this.
|
| Am I looking past an obvious aide to modelling that these
| approaches can give? I appreciate how this post acknowledges that
| there are not obvious uses of integration and such, but I feel
| that sort of proves my point. There are familiar mathematical
| tools that are good to use when we can. This does not mean you
| need to force them onto everything you have.
|
| It would probably help me a ton, if I ever saw these applied to
| state machines?
| marcosdumay wrote:
| > Specifically, I question if it is really how most people
| think in terms of programming.
|
| No, of course not. Algebra is only useful when you want to
| manipulate that exact thing, and most programmers never do any
| complex manipulation of types.
|
| Compiler programmers writing powerful type systems do think
| that way.
|
| > There are algebraic ideas in chemistry, but I would struggle
| to say how they look the same as this.
|
| Oh no, they don't. The algebra of Quantum Mechanics is way
| weirder than that. (At least when you move after simple
| rotations and step-potential wheels.)
| taeric wrote:
| Just to make sure I'm not misreading, this is largely an
| agreement? I think I'm fully in agreement that a compiler
| class should cover this. I will also hasten to say that I
| find it a fun topic, such that I don't think it should not be
| offered elsewhere. I just don't know that I can see a lot of
| application to general programming.
| noelwelsh wrote:
| Here's a very simple example:
|
| A user can have one of two roles: Normal or Admin. You can
| model this as: - User = Name x Password x Role
| - Role = Normal + Admin
|
| or you can multiply it out and get - User =
| Admin or Normal - Admin = Name x Password - Normal
| = Name x Password
|
| Which you should choose depends on the application. The second
| representation forces you to consider at every step if you have
| an Admin or Normal user, which is better for security. The
| first representation is more convenient when you don't care
| about the role.
|
| I do these transformations a lot when modelling things. They
| are trivial, but if you don't understand the underlying algebra
| you might not see them (in the same way the developers who
| aren't used to sum types tend to be blind to them.)
|
| Does that help?
| galaxyLogic wrote:
| What would be User x Role?
|
| Is it (Name x Password x Role) x (Normal + Admin) = ?
|
| What data-structure would that represent?
| taeric wrote:
| I'm not clear that I see the benefit of the techniques here?
| For one, it is not necessarily obvious that the "or (|)" is
| not a distributive property. It is, instead, a population
| description? As such, it seems like it leads to a very weird
| statements compared to what you would get in other uses.
|
| For example, if instead of Role, it was IsAdmin, and IsAdmin
| = True | False, then your application here gets you the odd
| True = Name x Password. What does that even mean?
|
| It also has an odd one of what if Role = Normal + Admin +
| SuperAdmin, but User is still Admin | Normal? What does that
| even mean?
| noelwelsh wrote:
| Or is + (Writing or was a typo)
|
| User has a Name, Password, and a Role, which gives
| User = Name x Password x Role
|
| Role is Normal or Admin. Formally: Role =
| Normal + Admin
|
| Now substitute User = Name x Password x
| (Normal + Admin)
|
| Multiply out User = (Name x Password x
| Normal) + (Name x Password x Admin)
|
| I added an extra step where I named some of the components.
|
| If you understand how this can be represented in code as an
| algebraic data type, you will see these two different
| representations have different properties when you come to
| program with them.
|
| If you don't, I'm afraid this text box does not contain
| enough space. Chapter 2 of https://scalawithcats.com/ goes
| through this in much more detail.
| taeric wrote:
| Cool, was curious why you had + and "or". I was assuming
| both are the same as | in the linked article. (I am
| further assuming you are largely working on the "left
| hand side" per the article?)
|
| The rest of your math, I largely followed, but I can't
| see where `Normal = Name x Password` results. Nor do I
| see what it would communicate. This is why I dropped
| instead to Boolean = True | False. If I substitute that
| in your statements, I get `True = Name x Password`. And I
| don't see how that means anything. :(
| noelwelsh wrote:
| Name and Password are probably going to wrap the String
| type. Admin and Normal don't have data associated with
| them. They are just flags (or tags, depending on the
| terminology you are used to.)
|
| So when we write User = (Name x Password
| x Normal) + (Name x Password x Admin)
|
| we know that Normal and Admin distinguish two otherwise
| identical cases. So with a bit of substitution we can
| write User = Normal + Admin Normal
| = (Name x Password) Admin = (Name x Password)
|
| True + False is isomorphic to Normal + Admin, but if you
| aren't used to working in a language with algebraic data
| types you might not be used to thinking in this way.
|
| In Haskell you'd write something like
| data User = Normal Admin Password | Admin Name Password
|
| You could equally write data User = True
| Admin Password | False Name Password
|
| because True and False are just tags, distinct from their
| use in the boolean type. This would just really confusing
| to other programmers.
| taeric wrote:
| I had a jest, at one point, where I would assume you are
| not modeling a password in your system. :D I'm assuming
| you'd instead model an AuthenticatedUser or some such. To
| that end, I'm fine with giving leeway to the modeling
| here. We are going for pedagogy.
|
| To that end, if this is a matter of going fast due to
| constraints of a message board, I am fine. My specific
| confusion was at the start where you had `Admin = Name x
| Password`. I'm not at all clear on what that would
| communicate to me in the types of any variables I would
| have in my code.
| johnnyjeans wrote:
| I think one of the most critical issues with thinking about
| ADTs in terms of an algebra is that they lack inverse
| operations which are otherwise an extremely critical component
| of how we conceive mathematics. A disjoint union type is
| formally equivalent to addition, but disunion is never defined,
| we are given no formal representation of subtraction. The same
| is given for cognates of division, of logarithms and roots
| (what those might look like is an interesting, if oft.
| neglected manner of research)
|
| There's (somewhat) good reasons we don't define these
| operations, of course. All the same, without being able to
| represent these inverse operations, the ease of which it maps
| to familiar notions of the typical algebras we're used to ends
| up thrown out the window.
|
| The algebra metaphor makes a bit more sense when you move
| beyond ADTs into more advanced levels of type-theory. Dependent
| types are a fair bit beyond a mere algebra, instead being more
| like a complete metalanguage akin to higher-order logic.
| taeric wrote:
| I think this is underscoring my concern with this as a
| pedagogical thing. I have seen people try very hard to find
| analogs with basic algebra. And... by people, I mainly mean
| younger me. Building algebras is, I think, still a very
| valuable thing if you can do it. Often times, though, the
| goal is not to fully mimic the basic algebra of grade school,
| but to map out what is doable with the abstractions that you
| have.
| taliesinb wrote:
| Yes, this is a very cool story.
|
| But, fascinatingly, integration does in fact have a meaning.
| First, recall from the OP that d/dX List(X) = List(X) * List(X).
| You punched a hole in a list and you got two lists: the list to
| the left of the hole and the list to the right of the hole.
|
| Ok, so now define CrazyList(X) to be the anti-derivative of _one_
| list: d /dX CrazyList(X) = List(X). Then notice that punching a
| hole in a _cyclic_ list does not cause it to fall apart into two
| lists, since the list to the left and to the right are the _same_
| list. CrazyList = CyclicList! Aka a ring buffer.
|
| There's a paper on this, apologies I can't find it right now.
| Maybe Alternkirch or a student of his.
|
| The true extent of this goes far beyond anything I imagined, this
| is really only the tip of a vast iceberg.
| itishappy wrote:
| > Can we extend the analogy to integration?
|
| Dumb idea: Unzipping?
|
| Differentiation takes as input the overall structure and extracts
| the behavior at a certain location. Integration takes the
| behavior at many different locations and returns a coherent
| picture of the overall structure.
|
| I'm struggling to picture the math. Does this work the way I
| envision?
| gwking wrote:
| This appears to have been published in 2015. Perhaps update the
| title with the year?
| dang wrote:
| Related:
|
| _The algebra and calculus of algebraic data types_ -
| https://news.ycombinator.com/item?id=17942112 - Sept 2018 (48
| comments)
|
| _The Algebra of Algebraic data types_ -
| https://news.ycombinator.com/item?id=9775467 - June 2015 (40
| comments)
| rramadass wrote:
| For people without some mathematical/language-relevant
| background, the following preliminaries would be useful;
|
| 1) A brief introduction to the Algebra of Types (nice intuitive
| explanation) - https://code.egym.de/a-brief-introduction-to-the-
| algebra-of-...
|
| 2) Algebraic data type -
| https://en.wikipedia.org/wiki/Algebraic_data_type
|
| 3) Comparison of programming languages (algebraic data type) -
| https://en.wikipedia.org/wiki/Comparison_of_programming_lang...
| sakras wrote:
| > Let's pause for a moment to remember that we're dealing with
| types. And the expression 1 / (1 - a) contains both a negative
| and a fractional type, neither of which have a meaning yet.
|
| This makes me wonder, is there a ring of types? There's addition
| and multiplication. Division and subtraction aren't necessary to
| define a ring, so their absence isn't particularly surprising.
| eigenket wrote:
| A ring forms an Abelian group with just its additive operation,
| so you basically have subtraction there. As far I can tell the
| structure we have formed by these datatypes is a semiring.
___________________________________________________________________
(page generated 2024-07-24 23:09 UTC)