7 ms·

The algebra and calculus of algebraic data types

170 points by alex_hirner 8y ago

Sharlin 8y ago
One thing I’ve been wondering is how to interpret the function types `Void -> a` and `a -> Void`, where Void is the uninhabited type (unique up to isomorphism). The number of inhabitants of those types should be |a|^0=1 and 0^|a|=0, respectively, but what does that mean? In real world, function(s) of type a->Void certainly exist, such functions being those that diverge (loop forever or halt via some non-local means).
- jpfr 8y ago
  Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
  - Sharlin 8y ago
    Yes, C void is a kinda-sorta unit type. But I’m talking about the real uninhabited type, ie. Void in Haskell, Nothing in Scala, ! (Never) in Rust. Real-world languages including Haskell are not total, so all functions a->b are in reality a->(b|Void). And for a good reason, as totality means loss of Turing completeness. In a total language, a function `a->Void` does not exist, but what about `Void->a`, then? What is the single inhabitant of that type?
    - erdeszt 8y ago
      This one typechecks but loops forever: f :: Void -> a f _ = let x = x in x
    - amboo7 8y ago
      It is the so-called empty function, which diverges, e.g. throws an exception if called.
    - tpush 8y ago
      Since one can prove anything if you're assuming nonsense, a function of the type 'Void -> a' should be able to just return its argument. And assuming the theory is consistent(so no infinite loops etc.) this is the only instance of that function, so the cardinality is 1.
      - Sharlin 8y ago
        That makes sense, thanks!
      - maweki 8y ago
        Where does an instance of a come from in that case? A function of that type has no way to construct one.
        theoh 8y ago
        Yes, there are no possible return values. But there is a unique vacuous total function because no return values are ever needed. A function can be considered as a set of ordered pairs, one for each value in the domain. Since there are no values in the domain, no pairs need exist. Another way to look at it is as a constrained subset of the Cartesian product of domain and codomain. In this case the domain is the empty set, so the Cartesian product is empty too.
        tpush 8y ago
        The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to logic in that a proof of nonsense can be used as a proof of anything. Take this Haskell code that passes the type checker: bottom = bottom f :: Int -> a f _ = bottom Here 'bottom' has the conceptual type Void/Bottom and checks successfully against the 'a'. So assuming we have this Void type in Haskell (I don't know if Haskell has it or not), this should also type check: f :: Void -> a f x = x Just like bottom (of type Void) checked against the 'a' earlier, an argument of that type should also type check.
      - Sharlin 8y ago
        And correspondingly `a->Void` must be empty because you can’t prove a contradiction given a true proposition in a consistent system? Makes sense from the Curry-Howard point of view.
- Quekid5 8y ago
  AFAIUI: "Void -> a" means that the function cannot be called, because there no way to conjure a Void value. In Haskell, you can do it by (ab)using 'undefined', but that's kind of cheating. However, if you're using Idris with totality checking, I don't think you'll actually get any code calling such a function compile. The "a -> Void" means that the function can never return.
  - matt-noonan 8y ago
    `Void -> a` is inhabited by the slightly weird empty-case construct in (GHC) Haskell: `\x -> case x of {}` has type `Void -> a`
    - uryga 8y ago
      Also known as the `absurd` function IIRC?
- contravariant 8y ago
  In mathematics, assuming 'void' is the empty set, the function void -> a exists, but is kind of trivial because it never returns anything, however functions a -> void can't exist because they'd have to return an element of void, which don't exist, the one exception being the function void -> void. Denoting A -> B as B^A this translates to: a^0 = 1 0^a = 0 0^0 = 1 The fact that there's precisely 1 function void -> a is considered rather special in category theory, and means that 'void' is the so called 'initial object' for the category (which is automatically unique up to isomorphism).
  - Sharlin 8y ago
    Yeah, it makes sense now. Thanks.
- hiker 8y ago
  `Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition. `a -> Void` get interpreted as "not a" or "from a follows contradiction" or equivalently "a is uninhabited". Combinatorially it's `0 ^ a` which for non-empty a is zero but is equal to 1 when a is empty (0^0=1). In other words there are no functions of type `a -> Void` for non-empty a and there's exactly one such function for uninhabited a (id :: Void -> Void). `Void -> a` is interpreted "from falsehood, anything (follows)" https://en.wikipedia.org/wiki/Principle_of_explosion https://en.wikipedia.org/wiki/Principle_of_explosion. Combinatorially a^0 = 1 for all a so there's exactly one such function. An easy way to define it is by induction on Void (which has no cases and you're done).
  - uryga 8y ago
    Yeah, Void makes for great for inductive definitions ;)
vajrabum 8y ago
That's fun and a bit surprising, but maybe it shouldn't be. I'm reminded that Dana Scott with Christopher Strachey showed that by using lattices or complete partial orders with a bit of topology to model graphs of possible computations of a program you could, just as in analysis, define least upper and lower bounds and a notion of continuity to derive a construction of limit for a computation which is analogous to a limit in analysis. They called this model a domain. That bit of of math is the basis of denotational semantics of programming languages and is necessary because sets are largely sufficient as the basis for algebra and analysis but not for programs which have evils like partial functions, side effects and variable assignment. I believe that Christopher Strachey with Scott also introduced the formal notions of sum, product and recusive types. They also showed how definitions or models of recursive types and functions could be well founded through their construction of limits on domains. An early tech report on it can be found here: https://www.cs.ox.ac.uk/files/3228/PRG06.pdf https://www.cs.ox.ac.uk/files/3228/PRG06.pdf and here's a more recent free book from David Schmidt on the topic: http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf
- evincarofautumn 8y ago
  Another interesting area of program semantics that hasn’t seen much attention afaik is in the design of languages whose programs form some algebraic structure. My area of research is concatenative programming, where concatenation of two programs denotes the composition of those programs, and the empty program is the identity function (on the “program state”, which is usually a stack). That means that the syntax and semantics of the language both form monoids, and there’s a homomorphism from the syntax onto the semantics. Several years ago, I was trying to come up with languages with other more interesting algebraic structures, so you could apply theorems from those structures to programs. A particular challenge is a language whose structure forms a nontrivial ring¹, in particular a Euclidean ring—then you could find the greatest common divisor of two programs, and because a Euclidean ring is a unique factorisation domain, you could also factor a program into prime subprograms. I was fascinated by what that might mean and whether it could be useful. Unfortunately, it was that “nontrivial” aspect that I could never get past. The language always ended up insufficiently powerful to express anything of interest, its algebraic structure was trivial (e.g. there’s only one program), or it ended up having a weaker structure (e.g. an idempotent semiring). Chris Pressey also worked on this concept a bunch around 2007, and produced some results like Cabra² and Burro³, but ran into similar dead ends like Potro⁴. ¹ https://en.wikipedia.org/wiki/Ring_(mathematics) https://en.wikipedia.org/wiki/Ring_(mathematics) ² http://catseye.tc/article/Languages.md#cabra http://catseye.tc/article/Languages.md#cabra ³ http://catseye.tc/article/Languages.md#burro http://catseye.tc/article/Languages.md#burro ⁴ https://github.com/catseye/Chrysoberyl/blob/master/article/List%20of%20Unfinished%20Interesting%20Esolangs.md#potro https://github.com/catseye/Chrysoberyl/blob/master/article/L...
tromp 8y ago
Very neat insights into data type differentiation! Minor nitpick: the article uses data Unit = Unit but the Haskell standard Prelude already has the empty tuple type (), with single element (), functioning as the standard unit type.
arithma 8y ago
A cool aspect is how this algebra/calculus sheds light that maps(/dictionary/associative-arrays) have an equivalent cardinality to functions and that they are in many ways the same.
- notduncansmith 8y ago
  In Clojure, maps can be called as functions (equivalent to `get`). This isomorphism is also reflected in K.
hyperpallium 8y ago
Does distributivity hold? a x (b + c) = a x b + a x c
- danharaj 8y ago
  Not literally, but there is a 1-1 correspondence between terms of the former and terms of the latter. Modulo technicalities in the presence of non-termination.
- evincarofautumn 8y ago
  Up to isomorphism, yes. That is, you can write a pair of functions that are mutual inverses that witness the fact that those two types are isomorphic: distl :: (a, Either b c) -> Either (a, b) (a, c) distl (a, b_c) = case b_c of Left b -> Left (a, b) Right c -> Right (a, c) factl :: Either (a, b) (a, c) -> (a, Either b c) factl ab_ac = case ab_ac of Left (a, b) -> (a, Left b) Right (a, c) -> (a, Right c) With the “TypeOperators” feature enabled (and “UnicodeSyntax” for pretty arrows and such, because why not), you can write it more literally: type (×) a b = (a, b) infixl 7 × type (+) a b = Either a b infixl 6 + distl ∷ a × (b + c) → a × b + a × c factl ∷ a × b + a × c → a × (b + c)
- yawaramin 8y ago
  Logically, it would seem to. If you can have an apple and either a ball or a cat, that's logically the same as having either an apple and a ball, or an apple and a cat. In terms of types, they are the same.
benrbray 8y ago
I once tried to take the Taylor series idea further and define the "cosine" of a type as the Taylor expansion of cos(x), but didn't get anywhere with it. Can you do anything else weird with ADTs?
- abecedarius 8y ago
  Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to be 2^x -- that is, x -> Bool -- because it's isomorphic to the characteristic function of a set, and a function type is an exponential (https://bartoszmilewski.com/2015/03/13/function-types/ https://bartoszmilewski.com/2015/03/13/function-types/). But 2^x differs from exp(x) by a constant factor. So I seem to be messing with surface-level analogies without real understanding.
  - etatoby 8y ago
    You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set x = x → Bool Cardinality: 2^x Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be surprised if it was not possible, or if the expansion turned out to have a strange cardinality such as e^x
    - abecedarius 8y ago
      Thanks, I forgot about repetitions of the same element. How could I miss that?
vignesh_m 8y ago
This is almost identical to the study of combinatorial species (https://en.wikipedia.org/wiki/Combinatorial_species https://en.wikipedia.org/wiki/Combinatorial_species)
rfw 8y ago
Nat = Nat + 1 does end up being meaningful: since ultimately the numbers that fall out (e.g. Bool = 2) end up describing the sizes of sets, an interpretation of Nat is some infinite cardinal (aleph-null), which is the size of the set of natural numbers.
- firethief 8y ago
  That makes sense, but this case shows that apparently arbitrary algebraic simplifications aren't allowed because otherwise we could subtract Nat from each side and have trouble.
carapace 8y ago
If you like this you'll want to look at "semiring programming" (just search on that phrase) and Categorical Programming, e.g.: "Compiling to categories" Conal Elliott http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/
- etatoby 8y ago
  I found the paper linked inside the article very interesting. It explores (one possible) meaning of negative and rational types. I'm still going through it: https://www.cs.indiana.edu/~sabry/papers/rational.pdf https://www.cs.indiana.edu/~sabry/papers/rational.pdf
andrzejsz 8y ago
What happened to Code Words that are not new issues?

170 points by alex_hirner 8y ago

One thing I’ve been wondering is how to interpret the function types `Void -> a` and `a -> Void`, where Void is the uninhabited type (unique up to isomorphism). The number of inhabitants of those types should be |a|^0=1 and 0^|a|=0, respectively, but what does that mean? In real world, function(s) of type a->Void certainly exist, such functions being those that diverge (loop forever or halt via some non-local means).

jpfr 8y ago
Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
- Sharlin 8y ago
  Yes, C void is a kinda-sorta unit type. But I’m talking about the real uninhabited type, ie. Void in Haskell, Nothing in Scala, ! (Never) in Rust. Real-world languages including Haskell are not total, so all functions a->b are in reality a->(b|Void). And for a good reason, as totality means loss of Turing completeness. In a total language, a function `a->Void` does not exist, but what about `Void->a`, then? What is the single inhabitant of that type?
  - erdeszt 8y ago
    This one typechecks but loops forever: f :: Void -> a f _ = let x = x in x
  - amboo7 8y ago
    It is the so-called empty function, which diverges, e.g. throws an exception if called.
  - tpush 8y ago
    Since one can prove anything if you're assuming nonsense, a function of the type 'Void -> a' should be able to just return its argument. And assuming the theory is consistent(so no infinite loops etc.) this is the only instance of that function, so the cardinality is 1.
    - Sharlin 8y ago
      That makes sense, thanks!
    - maweki 8y ago
      Where does an instance of a come from in that case? A function of that type has no way to construct one.
      - theoh 8y ago
        Yes, there are no possible return values. But there is a unique vacuous total function because no return values are ever needed. A function can be considered as a set of ordered pairs, one for each value in the domain. Since there are no values in the domain, no pairs need exist. Another way to look at it is as a constrained subset of the Cartesian product of domain and codomain. In this case the domain is the empty set, so the Cartesian product is empty too.
      - tpush 8y ago
        The key is that you can (in theory, I don't know if Haskell has a proper bottom that can act as a type) give a value of Void/Bottom to anything, analogous to logic in that a proof of nonsense can be used as a proof of anything. Take this Haskell code that passes the type checker: bottom = bottom f :: Int -> a f _ = bottom Here 'bottom' has the conceptual type Void/Bottom and checks successfully against the 'a'. So assuming we have this Void type in Haskell (I don't know if Haskell has it or not), this should also type check: f :: Void -> a f x = x Just like bottom (of type Void) checked against the 'a' earlier, an argument of that type should also type check.
    - Sharlin 8y ago
      And correspondingly `a->Void` must be empty because you can’t prove a contradiction given a true proposition in a consistent system? Makes sense from the Curry-Howard point of view.
Quekid5 8y ago
AFAIUI: "Void -> a" means that the function cannot be called, because there no way to conjure a Void value. In Haskell, you can do it by (ab)using 'undefined', but that's kind of cheating. However, if you're using Idris with totality checking, I don't think you'll actually get any code calling such a function compile. The "a -> Void" means that the function can never return.
- matt-noonan 8y ago
  `Void -> a` is inhabited by the slightly weird empty-case construct in (GHC) Haskell: `\x -> case x of {}` has type `Void -> a`
  - uryga 8y ago
    Also known as the `absurd` function IIRC?
contravariant 8y ago
In mathematics, assuming 'void' is the empty set, the function void -> a exists, but is kind of trivial because it never returns anything, however functions a -> void can't exist because they'd have to return an element of void, which don't exist, the one exception being the function void -> void. Denoting A -> B as B^A this translates to: a^0 = 1 0^a = 0 0^0 = 1 The fact that there's precisely 1 function void -> a is considered rather special in category theory, and means that 'void' is the so called 'initial object' for the category (which is automatically unique up to isomorphism).
- Sharlin 8y ago
  Yeah, it makes sense now. Thanks.
hiker 8y ago
`Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition. `a -> Void` get interpreted as "not a" or "from a follows contradiction" or equivalently "a is uninhabited". Combinatorially it's `0 ^ a` which for non-empty a is zero but is equal to 1 when a is empty (0^0=1). In other words there are no functions of type `a -> Void` for non-empty a and there's exactly one such function for uninhabited a (id :: Void -> Void). `Void -> a` is interpreted "from falsehood, anything (follows)" https://en.wikipedia.org/wiki/Principle_of_explosion https://en.wikipedia.org/wiki/Principle_of_explosion. Combinatorially a^0 = 1 for all a so there's exactly one such function. An easy way to define it is by induction on Void (which has no cases and you're done).
- uryga 8y ago
  Yeah, Void makes for great for inductive definitions ;)

vajrabum 8y ago

That's fun and a bit surprising, but maybe it shouldn't be. I'm reminded that Dana Scott with Christopher Strachey showed that by using lattices or complete partial orders with a bit of topology to model graphs of possible computations of a program you could, just as in analysis, define least upper and lower bounds and a notion of continuity to derive a construction of limit for a computation which is analogous to a limit in analysis. They called this model a domain. That bit of of math is the basis of denotational semantics of programming languages and is necessary because sets are largely sufficient as the basis for algebra and analysis but not for programs which have evils like partial functions, side effects and variable assignment. I believe that Christopher Strachey with Scott also introduced the formal notions of sum, product and recusive types. They also showed how definitions or models of recursive types and functions could be well founded through their construction of limits on domains. An early tech report on it can be found here: https://www.cs.ox.ac.uk/files/3228/PRG06.pdf https://www.cs.ox.ac.uk/files/3228/PRG06.pdf and here's a more recent free book from David Schmidt on the topic: http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf

evincarofautumn 8y ago
Another interesting area of program semantics that hasn’t seen much attention afaik is in the design of languages whose programs form some algebraic structure. My area of research is concatenative programming, where concatenation of two programs denotes the composition of those programs, and the empty program is the identity function (on the “program state”, which is usually a stack). That means that the syntax and semantics of the language both form monoids, and there’s a homomorphism from the syntax onto the semantics. Several years ago, I was trying to come up with languages with other more interesting algebraic structures, so you could apply theorems from those structures to programs. A particular challenge is a language whose structure forms a nontrivial ring¹, in particular a Euclidean ring—then you could find the greatest common divisor of two programs, and because a Euclidean ring is a unique factorisation domain, you could also factor a program into prime subprograms. I was fascinated by what that might mean and whether it could be useful. Unfortunately, it was that “nontrivial” aspect that I could never get past. The language always ended up insufficiently powerful to express anything of interest, its algebraic structure was trivial (e.g. there’s only one program), or it ended up having a weaker structure (e.g. an idempotent semiring). Chris Pressey also worked on this concept a bunch around 2007, and produced some results like Cabra² and Burro³, but ran into similar dead ends like Potro⁴. ¹ https://en.wikipedia.org/wiki/Ring_(mathematics) https://en.wikipedia.org/wiki/Ring_(mathematics) ² http://catseye.tc/article/Languages.md#cabra http://catseye.tc/article/Languages.md#cabra ³ http://catseye.tc/article/Languages.md#burro http://catseye.tc/article/Languages.md#burro ⁴ https://github.com/catseye/Chrysoberyl/blob/master/article/List%20of%20Unfinished%20Interesting%20Esolangs.md#potro https://github.com/catseye/Chrysoberyl/blob/master/article/L...

tromp 8y ago

Very neat insights into data type differentiation! Minor nitpick: the article uses data Unit = Unit but the Haskell standard Prelude already has the empty tuple type (), with single element (), functioning as the standard unit type.

arithma 8y ago

A cool aspect is how this algebra/calculus sheds light that maps(/dictionary/associative-arrays) have an equivalent cardinality to functions and that they are in many ways the same.

notduncansmith 8y ago
In Clojure, maps can be called as functions (equivalent to `get`). This isomorphism is also reflected in K.

hyperpallium 8y ago

Does distributivity hold? a x (b + c) = a x b + a x c

danharaj 8y ago
Not literally, but there is a 1-1 correspondence between terms of the former and terms of the latter. Modulo technicalities in the presence of non-termination.
evincarofautumn 8y ago
Up to isomorphism, yes. That is, you can write a pair of functions that are mutual inverses that witness the fact that those two types are isomorphic: distl :: (a, Either b c) -> Either (a, b) (a, c) distl (a, b_c) = case b_c of Left b -> Left (a, b) Right c -> Right (a, c) factl :: Either (a, b) (a, c) -> (a, Either b c) factl ab_ac = case ab_ac of Left (a, b) -> (a, Left b) Right (a, c) -> (a, Right c) With the “TypeOperators” feature enabled (and “UnicodeSyntax” for pretty arrows and such, because why not), you can write it more literally: type (×) a b = (a, b) infixl 7 × type (+) a b = Either a b infixl 6 + distl ∷ a × (b + c) → a × b + a × c factl ∷ a × b + a × c → a × (b + c)
yawaramin 8y ago
Logically, it would seem to. If you can have an apple and either a ball or a cat, that's logically the same as having either an apple and a ball, or an apple and a cat. In terms of types, they are the same.

benrbray 8y ago

I once tried to take the Taylor series idea further and define the "cosine" of a type as the Taylor expansion of cos(x), but didn't get anywhere with it. Can you do anything else weird with ADTs?

abecedarius 8y ago
Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to be 2^x -- that is, x -> Bool -- because it's isomorphic to the characteristic function of a set, and a function type is an exponential (https://bartoszmilewski.com/2015/03/13/function-types/ https://bartoszmilewski.com/2015/03/13/function-types/). But 2^x differs from exp(x) by a constant factor. So I seem to be messing with surface-level analogies without real understanding.
- etatoby 8y ago
  You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set x = x → Bool Cardinality: 2^x Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be surprised if it was not possible, or if the expansion turned out to have a strange cardinality such as e^x
  - abecedarius 8y ago
    Thanks, I forgot about repetitions of the same element. How could I miss that?

vignesh_m 8y ago

This is almost identical to the study of combinatorial species (https://en.wikipedia.org/wiki/Combinatorial_species https://en.wikipedia.org/wiki/Combinatorial_species)

rfw 8y ago

Nat = Nat + 1 does end up being meaningful: since ultimately the numbers that fall out (e.g. Bool = 2) end up describing the sizes of sets, an interpretation of Nat is some infinite cardinal (aleph-null), which is the size of the set of natural numbers.

firethief 8y ago
That makes sense, but this case shows that apparently arbitrary algebraic simplifications aren't allowed because otherwise we could subtract Nat from each side and have trouble.

carapace 8y ago

If you like this you'll want to look at "semiring programming" (just search on that phrase) and Categorical Programming, e.g.: "Compiling to categories" Conal Elliott http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/

etatoby 8y ago
I found the paper linked inside the article very interesting. It explores (one possible) meaning of negative and rational types. I'm still going through it: https://www.cs.indiana.edu/~sabry/papers/rational.pdf https://www.cs.indiana.edu/~sabry/papers/rational.pdf

andrzejsz 8y ago

What happened to Code Words that are not new issues?