☰
outcome
outcome
§Type Parameters
Functions
§group the elements of this sequence by a key of type K
f determines the key of an element
§
Type Parameters
Functions
§group the elements of this sequence by a key of type K
f determines the key of an element
Functions
§group the elements of this sequence by a key of type K
f determines the key of an element
§
group the elements of this sequence by a key of type K
f determines the key of an element
f determines the key of an element
outcome is a choice type that represents the result of a routine that
may either produce something useful or fail producing an error condition.
Several error conditions are needed if there are several very different
reasons for an operation to fail, e.g.
get_data (u User, t Type) outcome data IO_Error Permission_Error is
read_file t Type outcome data IO_Error is
Note that 'outcome data IO_Error' is not assignment compatible with
'outcome data IO_Error Permission_Error', it has to be unwrapped first.
This unwrapping, however, requires very little boilerplate, it is done
using the '?' on the result of the call to 'read_file': This unwraps
'outcome data IO_Error' into 'IO_Error', which would be returned abruptly,
and 'data', which would be returned normally. Both are assignment
compatible to 'outcome data IO_Error Permission_Error', so everything
is fine.