Redefining `false`, Introducing `never` and `None` for Optionals and Failures

General Feedback & Requests
, ,
1

Redefining false, Introducing never and None for Optionals and Failures

Summary

This proposal suggests a redefinition of several core semantic constructs in Verse by deprecating the current overuse of false. Specifically, it replaces false as a type and a sentinel value in optional and failure contexts with clearer, distinct concepts: never as the bottom (uninhabited) type, none as the type of unset optionals, and None as the corresponding canonical value.

Motivation

In the current Verse language design, the literal false is overloaded to represent three semantically distinct concepts:

  • A logic value (: logic = false).
  • A sentinel for unset optionals (: ?false = false).
  • The bottom type, used to represent unreachable or non-returning code : false = Err().

This overloading leads to decreased readability, difficulty in type reasoning, and ambiguity in failure handling and optional resolution.

V := array{false, option{true}, option{false}}
# V: []comparable for whatever reason
...

False := false
Optional: ?false = False #Not allowed because `False: logic`

By disentangling these responsibilities, we enhance the clarity of code, enforce type safety more effectively, and prepare the language for more expressive failure and result-handling mechanisms.

Design

Introduced Constructs

The proposal replaces and introduces the following constructs:

never := false          # `never` replaces `false` as the bottom type.
none := ?never          # `none` becomes the type of an unset optional.
None: none = false      # `None` becomes the value for an unset optional.

Optional and Failure Handling Semantics

New semantics for the ? operator allow it to propagate failure or indicate success depending on the value:

Fail()<decides><computes>: never = external{} #This function just fails

operator'?'(X: type{false})<decides><computes>: never = 		# type{false} is the singleton/literal type for `false` - not to be confused with the current bottom type. 
    Fail[] # Propagate failure

operator'?'(X: type{true})<computes>: void = 					# type{true} is the singleton/literal type for `true` - not to be confused with the current `void` alias. 
    external{} # Successful case

logic would look like this (which it basically is already):

logic := type{true} | type{false} 		# not to be confused with the current `true`(/void) and `false`(/bottom) types

Optional types are redefined with clearer semantics:

prefix'?'(t: type) := t | none 			# basically the same as `?t`

This ensures that unset optionals are typed with none rather than ambiguously typed as ?false and set to false.

Summary of Semantics

  • never is the new bottom type for unreachable code paths.
  • none := ?never serves as the canonical unset optional type.
  • None: none = false is the new canonical value for unset optionals.
  • Fail[], Err(), and false? all return never.
  • true? returns void.
  • SomeLogicVar? returns void regardless of whether its value is true or false, allowing concise logic gating.

Example: Optional Logic Value

MaybeLogic: ?logic = None  	#currently:  `MaybeLogic: ?logic = false`
MaybeLogic: ?logic = false 	#currently:  `MaybeLogic: ?logic = option{false}`
MaybeLogic: ?logic = true  	#currently:  `MaybeLogic: ?logic = option{true}`

# alternative to prefix'?'
MaybeLogic: logic | none = None  	
MaybeLogic: logic | none = false
MaybeLogic: logic | none = true

This now unambiguously represents an optional logic value without overloading false.

Drawbacks

  • Backward incompatibility: Any existing code using false to represent failure or unset optionals will need to be updated.

Alternatives or Additional Considerations

  • Retain the current overloaded use of false, accepting the semantic ambiguity and reduced expressiveness.
  • Also disambiguate true (simply get rid of it as alias for void)

Unresolved Questions

  • I don’t have anything in particular, but let me know.

Future Possibilities

  • Introduction of a result type built atop option, enabling richer and more structured error handling, potentially with an additional result type argument for Fail[FailureResult]
  • Consider some minor improvements like