3 ms·

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 𝟏 = 𝟏 + �

by sjolsen 11y ago

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 http://www.cl.cam.ac.uk/~sd601/papers/semirings.pdf

hiker 11y ago
The "Analytic Combinatorics"[1] book by Flajolet and Sedgewick is also relevant here. [1] http://algo.inria.fr/flajolet/Publications/book.pdf http://algo.inria.fr/flajolet/Publications/book.pdf
bweitzman 11y ago
I love that 0^0 = 1 since you can define voidToVoid :: Void -> Void = id
- sjolsen 11y ago
  You have to be careful when using Haskell for this sort of thing, because you can, for example, have a term of type Void: inhabitantOfZero :: Void inhabitantOfZero = fix id (Side note: the empty type can also be interpreted as the type of non-terminating computations, and in fact typing 'fix id' into ghci will cause it to hang) It turns out that 𝟎⁰ = 𝟏 is true, though, and if I'm not mistaken, this is true of semirings in general (where the exponent has a natural interpretation; of course you can define exponentiation this way for any semiring you like). This sole inhabitant is the empty function, which is easiest to explain in set-theoretic terms: if you define a function from A to B to be a subset of A × B such that each a ∈ A appears exactly once (for example, the negation function on Bool would be the set {(true, false), (false, true)}), it's clear that there's exactly one function from the empty set to the empty set, because there is only one subset of ∅ × ∅ (i.e., ∅) and for this set the above property is vacuously true. For completeness, here's what the empty function looks like in Agda, which treats types much more carefully than Haskell (to understand why, look up intuitionistic logic/type theory and the Curry-Howard isomorphism): module EmptyFunction where data ⊥ : Set where -- No constructors, since ⊥ is empty inhabitant-of-𝟎⁰ : ⊥ → ⊥ inhabitant-of-𝟎⁰ ()
  - bweitzman 11y ago
    Yeah, things start to break down when you include bottom (and fix id = _|_ since it diverges). I'm not sure exactly how to work with polymorphism in the function as subset model you described, but I'm guessing it would be something like this: Let id_A ⊆ A x A s.t for all a ∈ A, (a, a) ∈ id_A. If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue. > the empty type can also be interpreted as the type of non-terminating computations This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_
    - sjolsen 11y ago
      >If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue. The issue isn't with the example you gave, but with the idea in general that being able to produce a term of a given type in Haskell means that that type is necessarily inhabited. >This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_ Well, ⊥ is empty, so naturally every type is itself plus ⊥. In fact, that leads to an important observation, which is that any computation in Haskell could potentially be non-terminating, not just those with type Void—and so it's really not the inclusion of the bottom type that causes things to break down, but the ability to produce non-terminating computations (more specifically, non-coterminating, i.e. non-productive "lazy" computations). Unfortunately, the alternative—making it impossible to produce non-terminating computations—is more than anything a matter of rejecting everything the compiler can't prove terminates, which is kind of limiting, termination being undecidable in the general case. On the other hand, the sorts of computations humans design are generally much more well-structured than an arbitrary Turing machine, and so probably much easier to prove (co)termination for.
bweitzman 11y ago
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
- yummyfajitas 11y ago
  `Just x` cannot be constructed since there is no `x` which is has type `Void`.
  - tel 11y ago
    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.
  - bweitzman 11y ago
    `Just x` can be constructed given an `x`. The fact that no `x` can be given is somewhat irrelevant to the definition of the function.
- wz1000 11y ago
  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.
  - bweitzman 11y ago
    They are similar in that they cannot be applied to any non-bottom value, but they are definitely not the same function.
    - sjolsen 11y ago
      >they are definitely not the same function This depends on what equivalence you're using, and the only one in which it's true (definitional equality) isn't very interesting. Extensionally, the functions are identical.
tel 11y ago
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.
- sjolsen 11y ago
  >Not to detract from your point, but you don't need the expansion for that I just used the expansion given in the parent. It also makes it apparent that List is the closure.
  - tel 11y ago
    That's true!

by sjolsen 11y ago

hiker 11y ago

The "Analytic Combinatorics"[1] book by Flajolet and Sedgewick is also relevant here. [1] http://algo.inria.fr/flajolet/Publications/book.pdf http://algo.inria.fr/flajolet/Publications/book.pdf

bweitzman 11y ago

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

sjolsen 11y ago
You have to be careful when using Haskell for this sort of thing, because you can, for example, have a term of type Void: inhabitantOfZero :: Void inhabitantOfZero = fix id (Side note: the empty type can also be interpreted as the type of non-terminating computations, and in fact typing 'fix id' into ghci will cause it to hang) It turns out that 𝟎⁰ = 𝟏 is true, though, and if I'm not mistaken, this is true of semirings in general (where the exponent has a natural interpretation; of course you can define exponentiation this way for any semiring you like). This sole inhabitant is the empty function, which is easiest to explain in set-theoretic terms: if you define a function from A to B to be a subset of A × B such that each a ∈ A appears exactly once (for example, the negation function on Bool would be the set {(true, false), (false, true)}), it's clear that there's exactly one function from the empty set to the empty set, because there is only one subset of ∅ × ∅ (i.e., ∅) and for this set the above property is vacuously true. For completeness, here's what the empty function looks like in Agda, which treats types much more carefully than Haskell (to understand why, look up intuitionistic logic/type theory and the Curry-Howard isomorphism): module EmptyFunction where data ⊥ : Set where -- No constructors, since ⊥ is empty inhabitant-of-𝟎⁰ : ⊥ → ⊥ inhabitant-of-𝟎⁰ ()
- bweitzman 11y ago
  Yeah, things start to break down when you include bottom (and fix id = _|_ since it diverges). I'm not sure exactly how to work with polymorphism in the function as subset model you described, but I'm guessing it would be something like this: Let id_A ⊆ A x A s.t for all a ∈ A, (a, a) ∈ id_A. If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue. > the empty type can also be interpreted as the type of non-terminating computations This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_
  - sjolsen 11y ago
    >If A = ∅, then id_A = ∅, which is exactly the result we'd expect, so I don't see any issue. The issue isn't with the example you gave, but with the idea in general that being able to produce a term of a given type in Haskell means that that type is necessarily inhabited. >This is true, in a sense, but also a little bit misleading I think, since technically every type in Haskell is the set of terminating value with that type plus _|_ Well, ⊥ is empty, so naturally every type is itself plus ⊥. In fact, that leads to an important observation, which is that any computation in Haskell could potentially be non-terminating, not just those with type Void—and so it's really not the inclusion of the bottom type that causes things to break down, but the ability to produce non-terminating computations (more specifically, non-coterminating, i.e. non-productive "lazy" computations). Unfortunately, the alternative—making it impossible to produce non-terminating computations—is more than anything a matter of rejecting everything the compiler can't prove terminates, which is kind of limiting, termination being undecidable in the general case. On the other hand, the sorts of computations humans design are generally much more well-structured than an arbitrary Turing machine, and so probably much easier to prove (co)termination for.

bweitzman 11y ago

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

yummyfajitas 11y ago
`Just x` cannot be constructed since there is no `x` which is has type `Void`.
- tel 11y ago
  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.
- bweitzman 11y ago
  `Just x` can be constructed given an `x`. The fact that no `x` can be given is somewhat irrelevant to the definition of the function.
wz1000 11y ago
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.
- bweitzman 11y ago
  They are similar in that they cannot be applied to any non-bottom value, but they are definitely not the same function.
  - sjolsen 11y ago
    >they are definitely not the same function This depends on what equivalence you're using, and the only one in which it's true (definitional equality) isn't very interesting. Extensionally, the functions are identical.

tel 11y ago

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.

sjolsen 11y ago
>Not to detract from your point, but you don't need the expansion for that I just used the expansion given in the parent. It also makes it apparent that List is the closure.
- tel 11y ago
  That's true!