[Chinjut]

Sure, in the same sense that every set is a disjoint union over singletons of all its values. But whether you would or could naturally specify it that way or not depends on the set. You likely wouldn't sit down and specify the type "Function from natural numbers to Boolean" as a big OR over each possible such function, for example.

But yes, whether something is a sum type or a product type or whatever is not generally so interesting as a predicate about the type in itself. It's a relationship between this type and other types. The same way it is not interesting to say "7 is a sum" (everything is a sum); what's interesting is to observe "7 is the sum of 3 and 4".

[Disclaimer: In the same way that some topological spaces are connected and cannot be decomposed into separate disconnected components, one might sometimes reason that some types are connected and not reasonably represented as a disjoint unions over subtypes. So "Everything is a sum" is not always correct in all contexts. But let's ignore this sort of pedantry for now.]

[AnimalMuppet]

Here's what's bugging me: Integers are a disjoint union of values, which is (in my non-abstract-algebra mind) something different than a disjoint union of types. That is, something like Maybe Integer is a "sum type" in a completely different way from the way that Integer is a "sum type". To me, this is different enough that a different term should be used.

I'm sure you're going to tell me that I'm not thinking abstractly enough...

[tel]

There are sums at the type and value level. If I define Color = Red | Blue | Green, that’s not a use of a type which sums types together, but instead just is a type composed of a sum of values.

So a “sum type” can be any type which is the sum of different values. On the other hand, Either is a canonical “sum type (constructor)” which sums two types together (via the summation of their vaues).

[Chinjut]

If it weren't for finiteness restrictions, you could write the following in Haskell and it'd make a natural number type that acted basically as expected.

data Zero = Zero data One = One data Two = Two ... data NaturalNumber = Zero | One | Two | Three | ...

Whatever you would say about sets, you might as well say the same thing about types; the distinction in terminology doesn't amount to much. The natural numbers are the disjoint union of {0}, {1}, {2}, {3}, ... . They're also the disjoint union of the even naturals and the odd naturals, or the disjoint union of {0}, {1}, primes, and composites. There are a million ways in which they are a disjoint union.

[Chinjut]

Whoops, all the newlines were lost here, oh well.

[danharaj]

I don't think it's your level of abstraction, I think it's that you are treating as unrelated two sides of the same coin. This sum type / variant / disjoint union / coproduct construction operates both at the level of types and the level of values. After all, we only care about types insofar as they tell us about values.

[AnimalMuppet]

So Integer (0 or 1 or 2 or...) is a sum type in the same sense that Maybe Integer (Nothing or 0 or 1 or 2 or...) is. I see. That makes some sense.

So if I'm in Haskell, say, and I've got a Maybe Integer, and I'm trying to walk through the options (pattern matching), I usually see the options as Nothing or Just Integer. Can I instead do Nothing or Just 0 or... "Just some other Integer"? That is, can I treat... um, not sure how to say this in light of your post... "individual values of a particular named type" the same way as I can treat "different named types"?

[danharaj]

Ah I see, so what you're talking about is the syntax for defining a sum type. This confused me too. In Haskell, a definition of a sum type looks something like:

data MaybeInteger = Nothing | Just Integer

This defines the type MaybeInteger by saying how to construct the values that inhabit it. `Nothing` is a value that is immediately of type MaybeInteger. `Just` is a way to construct a value of type MaybeInteger by feeding it an Integer. You use `Just` to construct a value by applying it to an Integer: `Just 4`, for example.

There is an alternative syntax for defining sum types that might be clearer:

  data MaybeInteger where
    Nothing :: MaybeInteger
    Just :: Integer -> MaybeInteger

When using sum types, we use a case statement:

  case x of
    Nothing -> "nothing"
    Just 1 -> "one"
    Just _ -> "something else"

[coldtea]

  data MaybeInteger where
    Nothing :: MaybeInteger
    Just :: Integer -> MaybeInteger

Doesn't this mean that Nothing (ie. MaybeInteger) is the same "type"/"supertype" however you call it, as a constructor from Integer to MaybeInteger?

How does that work, e.g. how does MaybeInteger is equivalent to Integer -> MaybeInteger? I guess ending up at the same type is crucial, but one looks to be the type directly, while the other a constructor for the type.

And how can "Just" be a constructor for MaybeInteger here, but e.g. MaybeString in some other example? Is it specially blessed? What kind of thing it is in the language?

[danharaj]

Nothing and Just are constructors. Constructors need not be the same type. The whole point of a sum type is that you can construct it in multiple ways, after all.

In this case Nothing is immediately a value of type MaybeInteger. Just on the other hand has the type of a function :: Integer -> MaybeInteger.

So they don't have the same type, but Nothing and Just 5 have the same type, MaybeInteger.

For pedagogical purposes I pretended to work with MaybeInteger instead of Maybe from Haskell. The definition of Maybe is:

  data Maybe a = Nothing | Just a

or alternatively

  data Maybe a where
    Nothing :: Maybe a
    Just :: a -> Maybe a

I didn't want to simultaneously explain polymorphism and sum types, but the way you can combine them is vastly more useful than either feature alone.

[Quekid5]

You can think of Nothing and Just as functions that construct a MaybeInteger.

Nothing takes no parameters because there's no value there, so why would it?

Just takes an integer and gives you a MaybeInteger containing the integer you supplied to it.

There is only a single type here, namely MaybeInteger.

[AnimalMuppet]

Thanks!

[WorldMaker]

It's rarely useful (though there are some interesting examples) but it certainly is possible represent the naturals entirely in the type system as Church encodings [1] or Peano naturals [2] entirely in the Haskell type system. You'll see some references to such things elsewhere in these threads.

You can have a "type" for 4 in peano naturals and use that as a type guard on a function that can only physically take the number 4, and the Haskell type checking system will enforce that.

Here's one very clear implementation of Peano naturals as Haskell sum type: https://github.com/kenbot/church/blob/master/PeanoNat.hs

It's rare that you need that granular of a type, though, and as pointed out in sibling response it's easy enough to do with runtime pattern matching of Integer values. But it does illustrate that type abstraction "can go deeper".

[1] https://en.wikipedia.org/wiki/Church_encoding

[2] https://en.wikipedia.org/wiki/Peano_axioms