31–40 of 42 posts
The "algebraic" in algebraic data types refers to this notion of "algebra": https://en.wikipedia.org/wiki/Initial_algebra#Use_in_Compute...
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`.
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
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.
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 i…
I just used the expansion given in the parent. It also makes it apparent that List is the closure.
Earlier quoted context omitted.
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.
They are similar in that they cannot be applied to any non-bottom value, but 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.
Earlier quoted context omitted.
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 i…
>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.
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
inhabitantOfZero :: Void
inhabitantOfZero = fix id
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-𝟎⁰ ()Earlier quoted context omitted.
I love that 0^0 = 1 since you can define voidToVoid :: Void -> Void = id
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 semir…
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 _|_
Earlier quoted context omitted.
They are similar in that they cannot be applied to any non-bottom value, but they are definitely not the same function.
>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.
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…