Some questions about optionals

[kach]

In EData.v, what's the difference between dleft and dright vs dsuccess and derror vs dsome and dnone vs dunit? It seems that return some(10); in the REPL gives a dleft, not a dsome? At least, when it prints JSON, it's {"left": 10}. Similarly, an enforce error gives a dright.

(Also, how do you create a none in the REPL? return none(); doesn't work, not sure what else to try.)

P.S. The fact that I'm confused about this means that the REPL's match almost certainly does the wrong thing for optionals. So while this issue is a question, I guess it is actually also a bug report in disguise.

[jeromesimeon]

dleft and dright are constructor for a sum type with left and right components.

Those are used internally by the compiler in two ways:

• support for errors (e.g., a call to a statement returns either a success or an error). This is encoded using the dsuccess and derror macros over dleft and dright.
• support for optionals (e.g., an optional is either some value or none). This is encoded using the dsome and dnone macros over dleft and dright.

For a reason I cannot recall the syntax for none is nil. This probably should be changed to none for consistency.

[kach]

Okay, so it seems that dnone is equal to dright dunit. Makes more sense now. I can go fix match.

nil should definitely be renamed to none.

[kach]

Wait, no, we need separate names for dunit and dright dunit. none should be the latter, and maybe null should be dunit.

[jeromesimeon]

I like the idea of having either none be dright dunit, but I think using null for dunit is very confusing since it's completely different from the use of null in other languages. How about unit! -- I'm not even sure we need a syntax for that since you can't have a CTO type.

[kach]

none => none, i.e. dright dunit now, but nil is still dunit (#366)

[jeromesimeon]

This looks fixed:

I'm closing this issue.