The Algebra of Algebraic data types • Hacker News Board

Re: The Algebra of Algebraic data types

#21

Post by kahirsch » Thu, Jun 25, 2015, 2:36 PM UTC

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…

It may be helpful to think about this as a table.

9 functions from 2 to 3 - How many 2 digit numbers in base 3?

Each row represents a function from {True,False} to {A,B,C}.

    False  True
    -----  -----
      A      A      Function 1   f₁(False)=A   f₁(True)=A
      A      B      Function 2   f₂(False)=A   f₂(True)=B
      A      C      Function 3   etc.
      B      A      Function 4
      B      B      Function 5
      B      C      Function 6
      C      A      Function 7
      C      B      Function 8
      C      C      Function 9

8 functions from 3 to 2 - How many 3 digit numbers in base 2?

      A      B      C
    -----  -----  -----
    False  False  False   Function 1   f₁(A)=False f₁(B)=False f₁(C)=False
    False  False  True    Function 2   f₂(A)=False f₂(B)=False f₂(C)=True
    False  True   False   Function 3   etc.
    False  True   True    Function 4
    True   False  False   Function 5
    True   False  True    Function 6
    True   True   False   Function 7
    True   True   True    Function 8

Re: The Algebra of Algebraic data types

#22

Post by [deleted] » Thu, Jun 25, 2015, 3:42 PM UTC

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

[deleted]

Re: The Algebra of Algebraic data types

#23

Post by bweitzman » Thu, Jun 25, 2015, 4:27 PM UTC

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…

I love that 0^0 = 1 since you can define voidToVoid :: Void -> Void = id

Re: The Algebra of Algebraic data types

#24

Post by bweitzman » Thu, Jun 25, 2015, 4:39 PM UTC

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…

Actually I just realized that the law does not hold, the type `Void -> Maybe Void` has two inhabitants, not one:

f1 x = Nothing

f2 x = Just x

Re: The Algebra of Algebraic data types

#25

Post by yummyfajitas » Thu, Jun 25, 2015, 5:22 PM UTC

bweitzman wrote: post #24

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…

Actually I just realized that the law does not hold, the type `Void -> Maybe Void` has two inhabitants, not one: f1 x = Nothing f2 x = Just x

`Just x` cannot be constructed since there is no `x` which is has type `Void`.

Re: The Algebra of Algebraic data types

#26

Post by alex-g » Thu, Jun 25, 2015, 5:23 PM UTC

gjm11 wrote: post #12

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…

Just as a breadcrumb for readers who are curious about the generating function stuff: https://en.wikipedia.org/wiki/Combinatorial_species (see also https://www.cis.upenn.edu/~byorgey/pub/species-pearl.pdf for a nice FP-flavoured tutorial)

Re: The Algebra of Algebraic data types

#27

Post by tel » Thu, Jun 25, 2015, 5:23 PM UTC

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…

Not to detract from your point, but you don't need the expansion for that. Directly substituting 𝟏 in the definitional equation works just fine:

    L a = 𝟏 + a × (L a)
    L 𝟏 = 𝟏 + 𝟏 × (L 𝟏)
    L 𝟏 = 𝟏 +     (L 𝟏)
    L 𝟏 = 𝟏 + 𝟏 + 𝟏 + 𝟏 + 𝟏 + 𝟏 + ...
    ℕ   = 𝟏 + 𝟏 + 𝟏 + 𝟏 + 𝟏 + 𝟏 + ...

The final expansion is worth writing, however, since it notes how there are unboundedly many naturals, each a different component in this infinite disjoint sum.

Re: The Algebra of Algebraic data types

#28

Post by T-R » Thu, Jun 25, 2015, 5:29 PM UTC

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…

To add another way to look at it (thinking of a function as a set of tuples):

With tuples (A,B), you're listing As uniquely paired with Bs

With functions (A -> B), you're listnig unique sets of (As non-uniquely paired with Bs), so each A can go to any value of B, with replacement.

Re: The Algebra of Algebraic data types

#29

Post by wz1000 » Thu, Jun 25, 2015, 5:34 PM UTC

bweitzman wrote: post #24

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…

Actually I just realized that the law does not hold, the type `Void -> Maybe Void` has two inhabitants, not one: f1 x = Nothing f2 x = Just x

Both of them are regarded as the same function(ignoring bottom) because there is no way to differentiate between them as you can never supply them with a value of type Void in order to see their result.

Re: The Algebra of Algebraic data types

#30

Post by tel » Thu, Jun 25, 2015, 6:09 PM UTC

yummyfajitas wrote: post #25

bweitzman wrote: post #24

Earlier quoted context omitted.

Actually I just realized that the law does not hold, the type `Void -> Maybe Void` has two inhabitants, not one: f1 x = Nothing f2 x = Just x

`Just x` cannot be constructed since there is no `x` which is has type `Void`.

Well, there's the one in context that does! Except this function can never be called in an empty context so you ultimately are stuck.