Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Algebra of Algebraic data types

codewords.recurse.com

Post reply on HN
Print view View original

1–10 of 42 posts

Re: The Algebra of Algebraic data types

#3

Post by m_mueller »

As someone new to this I have to say the first paragraph doesn't do a good job at introducing the concepts. I was completely lost in how to read this. Isn't + == "or" and x == "and" like in boolean algebra? What does 'either' even mean here, if not 'or'? So then why is the Bool type 1 + 1 == 2? Shouldn't it be 1 + 0 == 1 if you want to map the possible states? Same question for "maybe" that seems to work like in Rust or Swift - shouldn't it be a + 0? If not, what does "a or unit" mean? So many questions...

Re: The Algebra of Algebraic data types

#4

Post by tikhonj »

m_mueller wrote: post #3

As someone new to this I have to say the first paragraph doesn't do a good job at introducing the concepts. I was completely lost in how to read this. Isn't + == "or" and x == "and" like in boolean algebra? What does 'either' even mean here, if not 'or'? So then why is the Bool type 1 + 1 == 2? Shouldn't it be 1 + 0 == 1 if you want to map the possible states? Same question for "maybe" that seems to work like in Rust…

Take a look at this other blog post[1] with the same title, which I think does a better job of explaining the core ideas.

[1]: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of...

Re: The Algebra of Algebraic data types

#5

Post by sjolsen »

It's worth noting that if you take the expansion for List:

    L a = 𝟏 + a × (L a)
        = 𝟏 + a + a² + a³ + ⋯
and substitute 𝟏 for a:

    L 𝟏 = 𝟏 + 𝟏 + 𝟏² + 𝟏³ + ⋯
        = 𝟏 + 𝟏 + 𝟏  + 𝟏  + ⋯
        = 𝟏 + (L 𝟏)
you get ℕ:

    ℕ = 𝟏 + ℕ
The zero-power rule (x⁰ = 1) from classic algebra also holds; there is exactly one function from 𝟎 to any type (or in set-theoretic terms, from the empty set to any set).

There was an interesting paper on "closed semirings"[0] posted here a few days ago. Clearly, the product and coproduct on types form a semiring, and interestingly, List is the closure!

[0] http://www.cl.cam.ac.uk/~sd601/papers/semirings.pdf

Re: The Algebra of Algebraic data types

#6

Post by hiker »

sjolsen wrote: post #5

It's worth noting that if you take the expansion for List: L a = 𝟏 + a × (L a) = 𝟏 + a + a² + a³ + ⋯ and substitute 𝟏 for a: L 𝟏 = 𝟏 + 𝟏 + 𝟏² + 𝟏³ + ⋯ = 𝟏 + 𝟏 + 𝟏 + 𝟏 + ⋯ = 𝟏 + (L 𝟏) you get ℕ: ℕ = 𝟏 + ℕ The zero-power rule (x⁰ = 1) from classic algebra also holds; there is exactly one function from 𝟎 to any type (or in set-theoretic terms, from the empty set to any set). There was an interesting pape…

The "Analytic Combinatorics"[1] book by Flajolet and Sedgewick is also relevant here.

[1] http://algo.inria.fr/flajolet/Publications/book.pdf

Re: The Algebra of Algebraic data types

#7

Post by mafribe »

eru wrote: post #2

(Formal) differentiation also makes sense for grammars, and in particular gives rise to an interesting way to match regular expressions.

The paper introducing this concept is [1] but was long forgotten. Recently the use of derivations to implement regular expressions has become popular again, see e.g. [2].

[1] J. A. Brzozowski's, "Derivatives of Regular Expressions", https://dl.acm.org/citation.cfm?id=321249

[2] https://www.cl.cam.ac.uk/~so294/documents/jfp09.pdf

Re: The Algebra of Algebraic data types

#8

Post by sjolsen »

m_mueller wrote: post #3

As someone new to this I have to say the first paragraph doesn't do a good job at introducing the concepts. I was completely lost in how to read this. Isn't + == "or" and x == "and" like in boolean algebra? What does 'either' even mean here, if not 'or'? So then why is the Bool type 1 + 1 == 2? Shouldn't it be 1 + 0 == 1 if you want to map the possible states? Same question for "maybe" that seems to work like in Rust…

>Isn't + == "or" and x == "and" like in boolean algebra?

In a sense, yes. "×" denotes the product of two types— i.e., the type of pairs of one value of the first type, and one of the second. "+" denotes the disjoint union of two types, the type of values which are taken from the first type or the second type. Importantly, when you have "a + a," taking a value from the left "a" is distinct from taking a value from the right "a."

>So then why is the Bool type 1 + 1 == 2? Shouldn't it be 1 + 0 == 1 if you want to map the possible states?

"0," "1," and "2" here do not denote states; rather, they denote types. In particular, "0" is the type with zero values, "1" is the type with one value, "2" is the type with two values, etc.

The reason that "1 + 1 = 2" is true is that there are two ways to form a value of type "1 + 1:" take the one possible value from the left "1," or take the one possible value from the right "1." The Bool type, by definition, has two values, so it needs to be given by the type "2," or equivalently, "1 + 1."

>Same question for "maybe" that seems to work like in Rust or Swift - shouldn't it be a + 0? If not, what does "a or unit" mean?

"a + 0" is, as the algebra suggest, just "a." This is because the only way to form a value of type "a + 0" is to use a value from "a;" there are no values in "0" to choose from. The Maybe type is effectively the identity type plus a single "None" value. Thus, we call it "a + 1;" there is a "Some" for each value in "a," and a None for each (i.e., the only) value in "1."

Re: The Algebra of Algebraic data types

#9

Post by m_mueller »

tikhonj wrote: post #4
m_mueller wrote: post #3

As someone new to this I have to say the first paragraph doesn't do a good job at introducing the concepts. I was completely lost in how to read this. Isn't + == "or" and x == "and" like in boolean algebra? What does 'either' even mean here, if not 'or'? So then why is the Bool type 1 + 1 == 2? Shouldn't it be 1 + 0 == 1 if you want to map the possible states? Same question for "maybe" that seems to work like in Rust…

Take a look at this other blog post[1] with the same title, which I think does a better job of explaining the core ideas. [1]: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of...

Thank you, that clears lots of things up.

Edit: Wow, even currying is explained nicely. This blog entry is pure gold.

Re: The Algebra of Algebraic data types

#10

Post by sjolsen »

mafribe wrote: post #7
eru wrote: post #2

(Formal) differentiation also makes sense for grammars, and in particular gives rise to an interesting way to match regular expressions.

The paper introducing this concept is [1] but was long forgotten. Recently the use of derivations to implement regular expressions has become popular again, see e.g. [2]. [1] J. A. Brzozowski's, "Derivatives of Regular Expressions", https://dl.acm.org/citation.cfm?id=321249 [2] https://www.cl.cam.ac.uk/~so294/documents/jfp09.pdf

>Recently the use of derivations to implement regular expressions has become popular again

And they're not limited to regular languages; with the right computational tricks (lazy evaluation, coinduction, whatever you want to call it), it can be used with context-free languages in general: http://matt.might.net/papers/might2011derivatives.pdf

Post reply on HN