The algebra and calculus of algebraic data types
codewords.recurse.com
The algebra and calculus of algebraic data types
1–10 of 49 posts
Re: The algebra and calculus of algebraic data types
#2One 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).
Re: The algebra and calculus of algebraic data types
#3One 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).
Such functions can’t exist.
The “C” void is expressed by the unit singleton.
So it is |a|^1.
Re: The algebra and calculus of algebraic data types
#4One 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).
Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
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?
Re: The algebra and calculus of algebraic data types
#5Earlier quoted context omitted.
Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
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…
This one typechecks but loops forever:
f :: Void -> a
f _ = let x = x in xRe: The algebra and calculus of algebraic data types
#6Earlier quoted context omitted.
Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
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…
It is the so-called empty function, which diverges, e.g. throws an exception if called.
Re: The algebra and calculus of algebraic data types
#7One 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).
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.
Re: The algebra and calculus of algebraic data types
#8Earlier quoted context omitted.
Such functions can’t exist. The “C” void is expressed by the unit singleton. So it is |a|^1.
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.
Re: The algebra and calculus of algebraic data types
#9Earlier 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.
That makes sense, thanks!
Re: The algebra and calculus of algebraic data types
#10Earlier 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.
Where does an instance of a come from in that case? A function of that type has no way to construct one.