Ah, I guess I misunderstood. From the tutorial:

> Pony often uses the primitive None to indicate that something has "no value".

So that is not a special value that we can assign to any variable.

"None" would seem to be pretty pointless all by itself, but I guess we could do a union of any old type with "None", to get a result much like Haskell's "Maybe". And then the Pony type system would give us much the same guarantees as Haskell's would; so we get a nullable variable that still allows for typesafe operations -- e.g., dereferencing, if applicable. (I guess ....)

Yeah, when I read the parent comment, I thought that None was part of a type like Maybe, but the next sentence describes it as a unit type:

  > Of course, it does have a value, so that you can check what it is, and the value is the single instance of None.

Yes, but, as I noted, Pony has type unions (http://tutorial.ponylang.org/types/type-expressions/). So you can roll your own Maybe types.

From the page I linked above:

> var x: (String | None)

> Here we have an example of using a union to express an optional type, where x might be a String, but it also might be None.

That's pretty clearly a Maybe.

Maybe (at least in Haskell/Rust) is a sum type, not a union type, though.

EDIT: Ugh, sorry, those are the same, I was thinking of sum vs _product_ type, ignore me.

Is a union type (at least in Haskell/Rust) structured like a union in C, where alternative types of values (e..g. int, float, char) occupy the same bytes, just not at the same time? Or is separate space allocated for the different types of values? Asking because, if a function returns a union type, with one type within it representing an integer (which can have any value), and if the function also wants to return an error condition, then no valid integer value can be used to indicate the error, because all integer values are valid return values from the function. In this case I would think that a union type should have separate space allocated for the integer value and the error-signalling value. (Something like what golang does with its return values?)

There are two major forms of sum type implementations that I'm aware of: tagged and untagged. What you're describing is a tagged union, for exactly the reason you state: there's an extra field for a discriminant which lets you choose the tag. Untagged unions are C's unions, where there's no discriminant, and you just have to know which type is valid at a given time.

Rust supports tagged unions, but can also optimize them to untagged in certain circumstances. We will probably add some kind of untagged union as well, mostly for FFI, but they're very unsafe, for the above reasons.

Got it, thanks. Interesting about Rust's design goals and tradeoffs.

Similarly, Pony's union (ie sum) type implementation always optimises to untagged, but required "boxing" raw machine-words when they're in a union type.

Actually, I think you've noted a significant issue: Pony looks to have been designed, at least in part, based on a sound theoretical foundation provided by modern type theory, semantics, etc. However, the documentation does not use the standard terminology of these fields. As a result, it is difficult to evaluate some of the claims that are made.

The Haskell void type () is also a None, and it's pretty helpful. The easiest example is `putStrLn :: String -> IO ()`.

you may be safe from "dereferencing null", but you'll still have to check for those edge cases, whether it's called Null or None

No, because random values cannot be None. The only thing that can be None is something with the type "None".

I see many examples where they do exactly what I described, checking for "None" as a parameter value. Sure, it's explicitly named as a possible value, but you STILL have to make the check yourself.

http://tutorial.ponylang.org/pattern-matching/match/#matchin...

I see how it can be used in new and different ways, and is definitely safer, but it's not like the idea of "that thing you want isn't here" goes away by introducing a None type.

I think I prefer the Option type to using a union with None here, for the reason that you state. I'm coming at this from a type theory / language design perspective: unit types are very different than nullable types, though if you write a union type with unit as one of the possibilities, well...

EDIT: Sorry, I was thinking of sum vs product here, union types are sum types. So this is the same thing as Option. Sounds good. The advantage of using a union type is that you _have_ to check. This is significantly better than nulls.

They're both sums, but Pony (and e.g. Typed Racket) has unlabelled unions, while Haskell/ML have labelled unions. Pony's (X | None) is not like Haskell's Maybe X in that in Haskell, X could be unit, while in Pony that would collapse the type to just None. In other words, in Haskell, Maybe (Maybe X) makes sense; in Pony and Typed Racket, it doesn't.

Yet another terminology issue: do you mean tagged vs untagged? IE, there's an extra field for the discriminant. Or rather, Pony does _not_ have a discriminant, but Haskell/ML do?

(I am 99% sure that's what you mean, but since I already screwed up terms once in this thread...)

That's roughly it. I was referring to a difference at the type system level, rather than the runtime level, though.

Disjoint unions aka sum types (as seen in Haskell/ML etc) entail some runtime way of keeping track which side of the sum any given inhabitant lies on. Tags are one way to do this, but e.g. in a language where pointers/references are never the zero machine word, and unit is represented as the zero word, no tag would be needed for the type Maybe String.

Union types (as seen in Pony, apparently, and also in Typed Racket), by contrast, /don't/ preserve information about which side of the union an inhabitant came from.

So, disjoint types: A + A ≠ A but union types: A ∪ A = A

So expanding (Maybe X) into (X + 1), we have that (Maybe (Maybe X)) = ((X + 1) + 1) ≠ X + 1,

but if instead (Maybe X) expands to (X ∪ 1), we have that (Maybe (Maybe X)) = ((X ∪ 1) ∪ 1) = X ∪ 1 = (Maybe X).

This is one of the problems with uses of null in languages that have it.