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