Does distributivity hold? a x (b + c) = a x b + a x c
The algebra and calculus of algebraic data types
21–30 of 49 posts
Re: The algebra and calculus of algebraic data types
#22Does distributivity hold? a x (b + c) = a x b + a x c
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.
Re: The algebra and calculus of algebraic data types
#23Does distributivity hold? a x (b + c) = a x b + a x c
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)
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)Re: The algebra and calculus of algebraic data types
#24Earlier quoted context omitted.
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 t…
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.
The "should be able to just return its argument" part is wrong; the types pretty clearly don't match, yeah? It is true that there is a unique function of type `Void -> a` for each `a`, but that isn't it.
Re: The algebra and calculus of algebraic data types
#25That'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…
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)
² http://catseye.tc/article/Languages.md#cabra
³ http://catseye.tc/article/Languages.md#burro
⁴ https://github.com/catseye/Chrysoberyl/blob/master/article/L...
Re: The algebra and calculus of algebraic data types
#26One 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).
`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…
Yeah, Void makes for great for inductive definitions ;)
Re: The algebra and calculus of algebraic data types
#27Earlier quoted context omitted.
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.
`Void -> a` is inhabited by the slightly weird empty-case construct in (GHC) Haskell: `\x -> case x of {}` has type `Void -> a`
Also known as the `absurd` function IIRC?
Re: The algebra and calculus of algebraic data types
#28Does distributivity hold? a x (b + c) = a x b + a x c
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.
Re: The algebra and calculus of algebraic data types
#29I 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?
Re: The algebra and calculus of algebraic data types
#30A 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.
In Clojure, maps can be called as functions (equivalent to `get`). This isomorphism is also reflected in K.