[knappador]

A referentially transparent, small function, has always been easy to write bug-free assuming the OS doesn't lose a page-table entry, a network interrupt isn't exploitable, and cosmic rays don't flip bits. The issue has never been that we can't write something that's correct.

Getting that correctness to propagate because of the strictness of all the tools involved and accuracy of their construction is the issue, which leaves us with needing to either automate proofs with Coq or prove things in more general ways that lead to undecidable problems etc. Still, the fact that one function can be written bug-free and known to be bug-free does indicate that it's not an inevitability of probability playing out as code grows.

We have null-pointer exceptions and no maybe type. The API's that emit nulls sometimes make me expect sewage to leak from light sockets. It's possible to do better. We just don't, and none of us love it. Rust and Kotlin are at least very exciting. I'd like to understand some Coq more in the context of x86. What routines are strictly necessary to even do Coq? A response based on some statement about how the Y-combinator enables X where X leads to Y would not surprise me.

[detrino]

Small imperative functions are just as easy to make bug free, I don't buy it.

[knappador]

Also true. Still, purity (just part of referential transparency) should be highlighted as something that helps not just with the function you're writing , but also functions that need to call that function.

[efaref]

With nicer syntax, nulls are equivalent to Maybe types. Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.

[chriswarbo]

> With nicer syntax, nulls are equivalent to Maybe types.

No they're not, since you can't nest NULLs.

Say I have a database of "Users", with "birthdates" mapping a "User" to a "DateOfBirth" and "spouses" mapping a "User" to a "User", I can look up a User's DateOfBirth either using a Maybe or by allowing NULLs:

    -- Maybe
    getDOB :: User -> Maybe DateOfBirth

    -- Nullable
    getDOB :: User -> DateOfBirth

I can also look up a User's spouse with either a Maybe or a NULL:

    -- Maybe
    getSpouse :: User -> Maybe User

    -- Nullable
    getSpouse :: User -> User

So far they're pretty much equivalent. However, what if I want to look up a spouse's DateOfBirth?

    -- Maybe
    spouseDOB :: User -> Maybe (Maybe DateOfBirth)
    spouseDOB u = fmap getDOB (getSpouse u)

    -- Nullable
    spouseDOB :: User -> DateOfBirth
    spouseDOB u = let s = getSpouse u
                   in if s == NULL then NULL
                                   else getDOB s

These are no longer equivalent. In the Maybe case we can distinguish between three kinds of values:

- `Nothing` indicates that we can't find the spouse

- `Just Nothing` indicates that we can find the spouse but not the DOB

- `Just (Just x)` indicates that we found both the spouse and the DOB

In the nullable case we can only distinguish between two kinds of values:

- `NULL` indicates that either we couldn't find the spouse or we couldn't find the DOB, but we don't know which

- Anything else indicates that we found the spouse and the DOB

The Maybe approach gives us strictly more information; although we can choose to ignore it if we like, either by using `join` or by replacing `fmap` with `>>=` (AKA "bind", which is a combination of `fmap` and `join`).

[david-given]

Yeah, but you're comparing apples and oranges. The nullable case isn't preserving the information you want, because you haven't written the code to preserve it, while in your Maybe case, you have. The two examples you give aren't doing the same thing.

Your nullable example is better compared to this, which also discards the required information:

    spouseDOB :: User -> Maybe DateOfBirth
    spouseDOB u = case getSpouse u in
                    s -> getDOB s
                    Nothing -> Nothing

Likewise, the nullable case, modified to preserve it (in a language which actually has nulls this time):

    DateOfBirth* spouseDOB(User& user) {
      Spouse* spouse = getSpouse(user);
      if (spouse)
        return &spouse->dateOfBirth;
      return NULL;
    }

Maybes are just pointers. There's nothing magic about them.

[chriswarbo]

> Your nullable example is better compared to this, which also discards the required information:

Exactly. Your version is just doing what `join` or `>>=` would do, which I mentioned at the end; ie.

    mySpouseDB u = fmap getDOB (getSpouse u)

    -- Using join
    yourSpouseDOB u = join (mySpouseDOB u)

    -- Using >>=
    yourSpouseDOB u = getSpouse u >>= getDOB

> Maybes are just pointers. There's nothing magic about them.

Of course there's nothing magic; `Maybe` just increments types. I was phrasing myself in the context of a language like Java, which has NULL but no pointer manipulation.

[dragonwriter]

> With nicer syntax, nulls are equivalent to Maybe types.

In a language that lacks maybes, but has nulls, what is the equivalent of the type Maybe (Maybe Int)?

> Recent C# for example has the ?. and ?? operators, which are flatMap and orElse.

Even ignoring the lack of composability, flatMap is an operation on a broad category of which Maybe is one example; that generality is a key part of its utility. ?. is a special-case operation on nullables, if you want to use it on any of the other things that flatMap works on (e.g., lists), you need a different operation, so you can't build generic algorithms. So, its not substantively the equivalent of what Maybe provides in languages where maybe is part of some broader category of operations on which flatMap can be applied.

[efaref]

> In a language that lacks maybes, but has nulls, what is the equivalent of the type Maybe (Maybe Int)?

    int **

> Even ignoring the lack of composability, flatMap is an operation on a broad category of which Maybe is one example; that generality is a key part of its utility.

While it's certainly part of it, I would disagree that it's the key part. The ?. operator is flatMap in the context of Maybes, and Maybes alone are useful for preventing a class of bug (NullPointerExceptions) even without the rest of Monadkind.

> ?. is a special-case operation on nullables, if you want to use it on any of the other things that flatMap works on (e.g., lists), you need a different operation, so you can't build generic algorithms.

Being able to use generic algorithms like sort() on Maybes-as-collections-of-arity-[0,1], while very cute, isn't actually that useful in real code. Particularly real C# or Java code.

Don't get me wrong, I've written code in Scala, and I love the generality of Maybe and related collection types, even though I have hit some interesting issues where I've needed to call .toSeq on my Maybe in order to get the right thing to happen, because they're not quite equivalent. But being pragmatic, and given that C# (and Java) don't have proper Monadic Maybe, and are unlikely to ever get them, I'd quite like the ?. and ?? operators, please.

[skrebbel]

Equivalent at runtime, yes, but with less static type checking.