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

11–20 of 42 posts

Re: The Algebra of Algebraic data types

#11

Post by m_mueller »

sjolsen wrote: post #8
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…

Got it, thank you. The other link posted by tikhonj is also very good at explaining. Your phrase

> "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.

should IMO be included in OP's post in some form or another. Also an explanation for void would be helpful, as in do not confuse 'void' in Haskell with e.g. 'void' in C or 'None' in python, as in those types are rather corresponding to 'unit' in Haskell.

Re: The Algebra of Algebraic data types

#12

Post by gjm11 »

A few remarks on this stuff.

1. Very closely related is the pure-mathematical technique of generating functions, where you take a sequence (let's say the Fibonacci sequence 0,1,1,2,3,5,8,13,...) and use its elements as coefficients in a power series (0+1x+1x^2+2x^3+3x^4+5x^5+8x^6+13x^7+...) and then notice that (e.g.) shifting the sequence by 1 is the same as multiplying by x, so if F is the series for (f(n)) then x.F is the series for (f(n-1)) and x^2.F is the series for (f(n-2)) apart from some corrections for very small n, which gets you F=(x+x^2)F+x or F = x/(1-x-x^2), and now you can factorize that quadratic and write F in the form p/(1-ax)+q/(1-bx) which immediately gets you an explicit formula for the Fibonacci numbers (the one with all the sqrt(5)s in it).

So let's translate this into algebraic data types. We get

  F(x) = x + x F(x) + x^2 F(x)
  data FibTree a = Leaf a | Pair a (FibTree a) | Triple a a (FibTree a)
and the number of FibTrees with n "a"s in is exactly the nth Fibonacci number.

(There is a theoretically important data structure called a Fibonacci heap, but I don't believe there is any connection between these and these "Fibonacci trees" other than that in both cases there is something you can count with Fibonacci numbers.)

2. Suppose you consider a rather boring binary-tree type like this:

  data Tree = Leaf | Pair Tree Tree
whose corresponding identity is T = 1+T^2, or T^2-T+1=0. If you're a mathematician you will quickly see that the solutions (in the complex numbers!) of this are sixth roots of unity; that is, they have T^6=1. This clearly can't hold in terms of types (it would mean an equivalence between 6-tuples of trees and objects of the "unit type", there being only one such object), but it turns out that T^7=T is "true"; you can find an explicit construction for it on page 3 of http://arxiv.org/abs/math/9405205 if you like.

3. It doesn't appear that the author of the OP ever got round to writing about negative and fractional types, but other people have. For instance, this paper http://www.cs.indiana.edu/~sabry/papers/rational.pdf which I have only glanced at (it appears to do this in a more restrictive context where there aren't general ADTs with recursive definitions; negative types seem to involve running computations backwards somehow, and reciprocals are "constraints").

Apologies if I've got my Haskell syntax wrong anywhere.

Re: The Algebra of Algebraic data types

#13

Post by acbart »

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function.").

The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c

The eight inhabitants of Tri -> Bool: https://gist.github.com/acbart/c695355880a706a4ff59

Pedagogical note: If you're going to poise a question in an online presentation of material, try to have a solution (automatically checked or at least statically available). A huge part of learning is having the learner participate (which you did!) and then assessed.

[1] I got help from here, @tikhonj suggested this in another comment: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of...

Re: The Algebra of Algebraic data types

#14

Post by brudgers »

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…

Reading the article reminded me of reading about Lisp macros (which I have been doing a bit of recently]. The shift from reasoning about values to reasoning about types feels a Ltd like the shift from reasoning about runtime to reasoning about compile time.

The interesting take away for me is that smaller data types are going to make it easier to reason about the state space. In turn this reminded me of Perlis:

Epigram 34. The string is a stark data structure and everywhere it is passed there is much duplication of process. It is a perfect vehicle for hiding information.

In that the state space is so massive.

Re: The Algebra of Algebraic data types

#15

Post by jbun77 »

acbart wrote: post #13

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function."). The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c The eight inh…

Thanks - wasn't obvious to me either. Am I missing something though, I only see six inhabitants in your gist for Tri?

Re: The Algebra of Algebraic data types

#16

Post by acbart »

jbun77 wrote: post #15
acbart wrote: post #13

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function."). The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c The eight inh…

Thanks - wasn't obvious to me either. Am I missing something though, I only see six inhabitants in your gist for Tri?

You're right, I missed two cases! Thanks a bunch. Second pedagogical note: we just demonstrated the value of cooperative learning, which can really help a weak assessment. Similar to paired programming!

Re: The Algebra of Algebraic data types

#17

Post by wz1000 »

acbart wrote: post #13

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function."). The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c The eight inh…

Imagine a collection of a objects(lets call it A) and another collection of b objects(called B). A function is a set of arrows matching each object in A to an object in B. Each object in A only has one arrow originating from it.

For each object in A, you have b ways to draw an arrow to an object in B. As there are a number of objects in A, the total number of arrows you can draw is bbb*b... a times. Hence the number of functions from A -> B is b^a.

Re: The Algebra of Algebraic data types

#18

Post by cousin_it »

acbart wrote: post #13

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function."). The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c The eight inh…

Maybe that part would've been easier with Bool and Unit. It's obvious that there is only one function from Bool to Unit, and two functions from Unit to Bool.

Re: The Algebra of Algebraic data types

#19

Post by saurik »

acbart wrote: post #13

If you're like me, and you didn't immediately understand why the number of inhabitants for "a -> b" is "a^b", and needed help for the answer[1], then here's my solution to the author's question ("Why are there eight inhabitants of Tri -> Bool, but nine of Bool -> Tri? It helps to write out each possible function."). The nine inhabitants of Bool -> Tri: https://gist.github.com/acbart/5d3fdfd8d363af26a59c The eight inh…

> the number of inhabitants for "a -> b" is "a^b"

You mean "b^a". (wz1000 has it right, but he didn't point out that the original statement had them flipped.)

Re: The Algebra of Algebraic data types

#20

Post by tel »

A nice algebraic law that holds in data types is

    a -> (b, c) = (a -> b, a -> c)
    (b * c)^a = b^a * c^a
This is useful as common argument factoring and can optimize repeated function calls.

Another is the famous

     (c^b)^a = c^(b * a)
     a -> b -> c = (a, b) -> c
Which is curry/uncurry or the "product/exponential adjunction" in category theory.

Finally, consider

    a^b * a^c = a^(b + c)
    (b -> a, c -> a) = Either b c -> a
Which essentially says that given a tuple of functions we can choose which one we want to evaluate. Choose b and c to be unit and notice that `() -> a` is essentially `a` (after all, a^1 = a) and you'll have

    a * a = a^2
    (a, a) = Bool -> a
Which is the seed of a useful way of memorizing pure functions (look up memo-combinators for many more details).
Post reply on HN