Preface_specs.Arrow_choiceAn Arrow_choice is an Arrow with conditional capabilities. It is a kind of Selective in the arrow hierarchy. And an Arrow_choice is also Arrow.
To have a predictable behaviour, the instance of Arrow_choice must obey some laws.
Arrow lawsleft (arrow f) = arrow (f ++ id)left (f >>> g) = left f >>> left gf >>> arr Left = arr Left >>> left fleft f >>> arrow (Fun.id +++ g) = arrow (Fun.id +++ g) >>> left fleft (left f) >>> arrow assocsum = arrow assocsum >>> left fmodule type WITH_CHOOSE = sig ... endMinimal definition using choose operation without Arrow.
module type WITH_LEFT_AND_CHOOSE = sig ... endMinimal definition using choose and left without Arrow.
module type WITH_ARROW_AND_FST_AND_CHOOSE = sig ... endMinimal definition using arrow and fst and choose.
module type WITH_ARROW_AND_FST_AND_LEFT = sig ... endMinimal definition using arrow and fst and left.
module type WITH_ARROW_AND_SPLIT_AND_CHOOSE = sig ... endMinimal definition using arrow and fst and choose.
module type WITH_ARROW_AND_SPLIT_AND_LEFT = sig ... endMinimal definition using arrow and fst and left.
module type CORE = sig ... endBasis operations.
module type OPERATION = sig ... endAdditional operations.
module type ALIAS = Arrow.ALIASAliases of some operations functions.
module type INFIX = sig ... endInfix operators.
module type API = sig ... endThe complete interface of an Arrow_choice.