effect.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 effect
#
# Author: Fridtjof Siebert (siebert@tokiwa.software)
#
# -----------------------------------------------------------------------
# effect -- abstract parent feature for effects
#
# effect provides a means to perform effectful operations. Instances
# of effect are instated in the current environment while their code is
# executed. The code may perform operations of the instated effect
# via <type>.env. These operations may either return normally (resume) or
# abort the current computation, i.e., return directly to the call that
# instated the effect.
#
# Effects are identified by their type, including any actual type parameters.
# Effect instances must be assignable to the effect type. This means that if
# the effect type is a value type, the instance must be an instance of exactly
# that type while if the effect type is a ref type, the instance might be of
# a type that inherits from the effect type that is --possibly after boxing--
# assignable to that type.
#
# Effect operations may replace an instated instance by a new value.
# This gives operations a means to become stateful.
#
# In case an effect performs an abort, the code the effect was instated for
# will be abandoned and the function passed via tha `def` argument to
# `instate` will be used to produce a result from the last effect instance.
#
# Effects may redefine the `finally` feature that is executed directly after
# an instated effect was removed, independent of the reason why it is removed.
# This means, finally is executed after code running in the effect returns
# normally, after a call to an operation that results in an abort or when
# a surrounding effect is aborted.
#
public effect is
# -------------------- effect intrinsics --------------------
# get this effect from env
#
public type.from_env effect.this => intrinsic
# set default effect in the current context to this if none is
# installed
#
type.default0(e effect.this) unit => intrinsic
# instate e for effect type effect.this in the current environment.
#
# execute code provided by `code` while this effect `e` is instated in the
# current environment and remove the instated effect after `code` returned.
#
# In case of an abort, run `def` on the latest value instated or replaced
# for `effect.this` after removing that instated effect value.
#
# Note the use of `_ : Function ...` instead of just `Function ...`: This
# introduces type parameters. This has several important implications:
#
# - First, it permits `code` and `def` to be of value types, and
# - second, it simplifies the backends since calls to `code.call` or
# `def.call` are statically defined by that value type, no need for
# dynamic binding.
#
# As a neat side-effect this avoids heap allocation of the lambdas.
#
type.instate0(e effect.this,
code _ : Function unit,
def _ : Function unit effect.this) unit => intrinsic
# replace existing effect of type `E` in the new effect value `e`
#
type.replace0(e effect.this) unit => intrinsic
# Intrinsic version of abort. For all surrounding instated effects,
# remove the effect and run `finally` until we have reached an
# effect of this type. Then return from that effect's `instate0` call
# with the rsult produced by calling `def` on the currently instated
# value.
#
type.abort0 void => intrinsic
# has an effect of this type been instated?
#
type.is_instated0 bool => intrinsic
# -------------------- default effects --------------------
# set default instance for effect type `effect.this` to `e`
#
# NYI: UNDER DEVELOPMENT: This is a manual work-around to automatically install
# default effects. It should be replaced by a effect configuration file that
# is defined locally to a fuzion project or globally to the fuzion installation
# the defines the default effects to be used. The DFA should then automatically
# determine the required effects and create code to instate them at the beginning
# of an application.
#
public type.default(e effect.this) => default0 e
# convenience version of `type.default` for effect values whose type is
# exactly the effect type (i.e., the value type does not inherit
# from the effect type).
#
# set default instance for effect type `effect.this` to value `effect.this`.
#
# NYI: UNDER DEVELOPMENT: See type.default
#
public default unit
=>
effect.this.type.default effect.this
# -------------------- effect instation --------------------
# execute 'code' in a context where the effect instance `e` has been
# installed for effect type `effect.this`.
#
# In case `f` returns normally, this will return `f`'s result.
#
# In case `f` aborts this effect, return `def()`.
#
public type.instate(# result type
R type,
# the effect value to instate
e effect.this,
# the code to execute with `e` instated.
code () -> R,
# the lazy default result to use if effect aborts
def effect.this -> R
) R
=>
x := instate_helper R effect.this e code def
instate0 e x.call_code x.call_def
x.res.get
# execute 'code' in a context where the effect instance `e` has been
# installed for effect type `effect.this`.
#
# In case `f` returns normally, this will return `f`'s result.
#
# In case `f` aborts this effect, this will panic.
#
public type.instate(# result type
R type,
# the effect value to instate
e effect.this,
# the code to execute with `e` instated.
code () -> R
) R
=>
instate R e code (_ -> panic "unexpected abort in {effect.this.type}")
# convenience version of `instate` for effect values whose type is
# exactly the effect type (i.e., the value type does not inherit
# from the effect type).
#
# Execute 'code' in a context where this effect instance has been
# instated for effect type `effect.this`.
#
# In case `f` returns normally, this will return `f`'s result.
#
# In case `f` aborts this effect, this will panic.
#
public instate_self(# result type
R type,
# the code to execute with `e` instated.
code () -> R
) R
=>
effect.this.instate R effect.this code
# infix variant instate_self
#
# use it like this:
#
# effect_instance ! ()->code
#
public infix !(# result type
R type,
# the code to execute with `e` instated.
code () -> R
) R
=>
instate_self code
# infix variant of effect.instate
#
# use it like this:
#
# effect_type <- effect_instance ! code
#
public type.infix <- (E type : effect, e E) =>
effect0 e
# has an effect of this type been instated?
#
public type.is_instated bool => is_instated0
# has an effect of the given type been instated?
public type.get_if_instated option effect.this
=>
if effect.this.is_instated
unsafe_from_env
else
nil
# internal helper to perform `E.env` without producing an error
# in case static analysis fails to verify that `effect.this` is
# actually instated.
#
type.unsafe_from_env effect.this => intrinsic
# -------------------- replacing effect instances --------------------
# replace existing effect for type `effect.this` by the new effect value `e`.
#
# For effects that model the outside world (e.g., i/o, time, sensors and actuators, etc.),
# the effect might be a unit type, so the replace is effectively a no-operation. However,
# the call to `replace` is used ot model the change of the outside world and must be
# included for analysis tools to appreciate this.
#
# replace may only be called during the execution of an operation of a currently instated
# effect of the same effect type.
#
# NYI: BUG: It is currently not enforced that replace is only called during the execution
# of an operation of a currenlty instated effect of the same effect type.
#
public type.replace(e effect.this)
=>
replace0 e
# replace existing effect of type `effect.this` by the new effect value `effect.this`.
#
# This is a convenience feature for value type effects for which the type of
# the effect instance equals the effect type. `ref` type effects typically have
# values that may be children of the effect type that are of a different type, so
# `effect_type.replace new_value` must be used.
#
# replace may only be called during the execution of an operation of a currently instated
# effect of the same effect type.
#
public replace
=>
effect.this.type.replace effect.this
# -------------------- aborting code execution --------------------
# replace existing effect for type `effect.this` by the new effect value `e`
# and abort code execution to return to the point where the effect was instated.
#
public type.abort(e effect.this) void
pre
safety: effect.this.is_instated
safety: effect.this.env.abortable
=>
replace0 e
abort0
# Abort code execution for the instated effect.this.env and return to the point
# where the effect was instated.
#
public type.abort void
pre
safety: effect.this.is_instated
safety: effect.this.env.abortable
=>
effect.this.abort0
# does this effect support abort?
#
# Redefining this to return `false` helps to detect unexptected calls to
# `abort` at runtime and ensure that the static analysis finds that the
# code executed with this effect will always return normally and produce
# a result. This is used, e.g, in `mutate` to avoid static analysis
# reporting `panic` as an effect of the use of a local mutate instance.
#
public abortable => true
# abort the current execution and return from the surrounding call to
# `instate`.
#
# NYI: CLEANUP: `return` is the same as `abort`. The term `return` seems
# common for algebraic effects, but is confusing since it is different to
# returning from a call. We need to decide to break with algebraic effect
# jargon (and remove `return`) or to stick with it (and rename `abort` as
# `return`).
#
public type.return void
pre
safety: effect.this.is_instated
safety: effect.this.env.abortable
=>
abort
# -------------------- resource cleanup --------------------
# feature that will be called on the final instance of this effect
# after it has been de-instated.
#
# This happens either on a normal return form the code passed to
# `instate`, on an abort perfomed on this effect or on an abort
# performed on an effect instated prior to this effect's instation.
#
# This can be used to perform actions when leaving an effect such
# a cleanup up resources that were created or opened by operations
# of this effect.
#
public finally =>
# internal feature that will be called on the instance of this effect
# when it will be de-instated.
#
# This is just a trampoline for compiler convenience such that when
# generating code for the instate0 intrinsic the compiler does
# not need to care about dynamic binding if the current effect is a
# `ref`.
#
static_finally => finally
# instante helper to hold the result of the effect
#
instate_helper(# result type
R type,
# effect type
ET type: effect,
# the effect value
e ET,
# the code to execute with `e` instated.
code () -> R,
# the lazy default result to use if effect aborts
def ET -> R) is
# we replace `code`/`def` by functions with unit type result
# to reduce complexity of the `instate0` intrinsic. We
# collect the result in this field
res := option R nil
# wrapper to call `code` and store result in 'res`
call_code : Function unit is
redef call =>
set res := code()
# wrapper to call `def` on final effect value and store result in 'res`
call_def : Function unit ET is
redef call(cur_e ET) =>
set res := def cur_e
# a constructor for holding an effect type and instance
#
# this allows defining operators
#
public effect0(E type : effect, e E) is
# infix variant of effect.instate
#
# use it like this:
#
# effect_type <- effect_instance ! code
#
public infix !(# result type
R type,
# the code to execute with `e` instated.
code () -> R
) R
=>
E.instate R e code
