Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The algebra and calculus of algebraic data types

codewords.recurse.com

Post reply on HN
Print view View original

11–20 of 49 posts

Re: The algebra and calculus of algebraic data types

#11

Post by theoh »

maweki wrote: post #10
tpush wrote: post #8

Earlier quoted context omitted.

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.

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.

Re: The algebra and calculus of algebraic data types

#12

Post by tpush »

maweki wrote: post #10
tpush wrote: post #8

Earlier quoted context omitted.

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.

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.

Re: The algebra and calculus of algebraic data types

#13

Post by vajrabum »

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

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

Re: The algebra and calculus of algebraic data types

#15

Post by Sharlin »

tpush wrote: post #8
Sharlin wrote: post #4

Earlier 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.

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.

Re: The algebra and calculus of algebraic data types

#16

Post by contravariant »

Sharlin wrote: post #2

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).

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).

Re: The algebra and calculus of algebraic data types

#17

Post by Sharlin »

contravariant wrote: post #16
Sharlin wrote: post #2

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).

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 i…

Yeah, it makes sense now. Thanks.

Re: The algebra and calculus of algebraic data types

#18

Post by hiker »

Sharlin wrote: post #2

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).

`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. 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).

Re: The algebra and calculus of algebraic data types

#20

Post by matt-noonan »

Quekid5 wrote: post #7
Sharlin wrote: post #2

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).

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`
Post reply on HN