Why do Maybe/Optional types use a Just/Some type instead of the actual type?

Question

In Idris, the Maybe type is defined as followed:

data Maybe a = Just a | Nothing  

It's defined similarly in Haskell:

 data Maybe a = Just a | Nothing
     deriving (Eq, Ord)

Here's the ML version:

datatype 'a option = NONE | SOME of 'a

What are the benefits of using Just and Some?
Why not define the type without them?

example:

data Maybe a = a | Nothing

Answer 1

What would then be the difference between

Maybe a

and

Maybe (Maybe a)

?

There's supposed to be a difference between Nothing and Just Nothing.

Answer 2

The key problem of allowing any value to be null (the "billion-dollar mistake") is that interfaces receiving a value of a type T have no way to declare whether or not they can handle a null, and interfaces that provide one have no way to declare whether or not they might produce null. This means that all of the operations that are usable on T essentially "might not work" when you pass them a T, which is a pretty gaping hole in all of the guarantees supposedly provided by compile-time type-checks.

The Maybe/Optional solution to this is to say that the type T does not contain a null value (in languages that had this from the beginning, that's literal; in languages adopting an Optional type later without removing support for null, then that's only a convention that requires discipline). So now all of the operations whose type says they accept a T should work when I pass them a T, regardless of where I got the T (if you haven't managed to design to "make illegal states unrepresentable" then there will of course be other reasons why an object can be in an invalid state and cause failure, but at least when you pass a T there'll actually be something there).

Sometimes we do need a value that can be "either a T or nothing". It's such a common case that pervasive null seemed like a good idea at the time, after all. Enter the Maybe T type. But to avoid falling back into exactly the same old trap, where I get a possibly-null T value and pass it to something that can't handle null, we need that none of the operations on T can be used on a Maybe T directly. Getting a type error from trying to do that is the entire point of the exercise. So my T values can't be directly members of Maybe T; I need to wrap them up inside a Maybe T, so that if I have a Maybe T I'm forced to write code that handles both cases (and only in the case for actually having a T can I call operations that work on T).

Whether this makes a word like Just or Some appear in the source code, and whether or not this is actually implemented with additional boxing/indirection in memory (some languages do represent a Maybe T as a nullable pointer to T internally), all of that is irrelevant. But the Just a case must be different from simply having an a value.