[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