void.fz

# This file is part of the Fuzion language implementation.
#
# The Fuzion language implementation is free software: you can redistribute it
# and/or modify it under the terms of the GNU General Public License as published
# by the Free Software Foundation, version 3 of the License.
#
# The Fuzion language implementation is distributed in the hope that it will be
# useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License along with The
# Fuzion language implementation.  If not, see <https://www.gnu.org/licenses/>.


# -----------------------------------------------------------------------
#
#  Tokiwa Software GmbH, Germany
#
#  Source code of Fuzion standard library feature void
#
#  Author: Fridtjof Siebert (siebert@tokiwa.software)
#
# -----------------------------------------------------------------------

# void -- the default empty type
#
# NOTE: For a counterpart to void in C, Java, etc., see unit.fz
#
# void is the bottom type in Fuzion, the default empty type that is a subtype of all
# other types.
#
# It is impossible to create any values of this type, consequently, it is impossible
# to assign anything to a field of void type.
#
# If used as the type of an argument field for a feature, the feature can never be
# called since no value assignable to that argument could ever be produced.  This
# produces an absurd feature.
#
# If used as the result type of a routine, the routine can never return.
#
# void is the result type of the endless loop
#
#   do { <loop body> }
#
# If used as the result type of a field, the field can never be assigned a value,
# since no such value can be produced, and the field can never be read since it
# remains not initialized forever.
#
# Type void is assignable to all other types, e.g, we can assign void to a value
# of type i32:
#
#   i i32 := exit 1
#
# Since no value of type void can ever be produced, the assignment is dead code that
# will be removed by the fuzion implementation.
#
# Type void may be used as an actual type argument for a type parameter.  If this
# is done, it will turn all features that have arguments of that type into absurd
# features.  Also, this will ensure that any feature that produces a result of that
# type to never return a result (typically to not be callable in the first place as
# well).  An example could be a stack of capacity zero: stack void 0 with an
# absurd
#
#   stack.push(void)
#
# and a pop function with a precondition that is always false
#
#   pop void
#     pre size > 0
#
# The memory required to store a value of void type is not defined since these
# values do not exist.  The Fuzion code generators typically will not generate
# any code for features receiving arguments of void type or for code following
# a feature call that returns void.
#
#
public void : choice  # an empty union, so this type has no value
is