~/bend-docscommunity

maybe.bend checks

raw source on the hub · import bend-mathlib@0.7.1.0/maybe.bend as MMaybe

bend-mathlib/maybe.bend: Maybe monad and map laws over &2.

1 import
import Base

Laws

law maybe_pure_bind provedsource · line 5 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-x:A -> {Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) == f(x) : Maybe<&2, B>}

Left identity: binding a pure value applies the function.

law maybe_bind_pure provedsource · line 16 · raw

@-A:Data -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) == m : Maybe<&2, A>}

Right identity: binding pure is the identity.

law maybe_bind_assoc provedsource · line 29 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-g:(@_:B -> Maybe<&2, C>) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) == Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) : Maybe<&2, C>}

Bind is associative.

law maybe_map_pure provedsource · line 46 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @-x:A -> {Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) == Maybe.pure(&2, B, f(x)) : Maybe<&2, B>}

Mapping a pure value is pure of the mapped value.

law maybe_map_compose provedsource · line 57 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> B) -> @-g:(@_:B -> C) -> @m:Maybe<&2, A> -> {Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) == Maybe.map(&2, A, C, x => g(f(x)), m) : Maybe<&2, C>}

Mapping a composition maps the composition.

law maybe_map_id provedsource · line 74 · raw

@-A:Data -> @m:Maybe<&2, A> -> {Maybe.map(&2, A, A, x => x, m) == m : Maybe<&2, A>}

Mapping the identity gives the value back.

law maybe_bind_none provedsource · line 87 · raw

@-A:Data -> @-B:Data -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, B, m, x => None{}) == None{} : Maybe<&2, B>}

Binding a function that always fails gives None.

law maybe_map_eq_bind provedsource · line 101 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.map(&2, A, B, f, m) == Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) : Maybe<&2, B>}

Mapping is binding the function followed by pure.

law maybe_is_some_map provedsource · line 116 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_some(&2, A, m) : Bool}

Mapping keeps whether a value is present.

law maybe_is_none_map provedsource · line 131 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) == Maybe.is_none(&2, A, m) : Bool}

Mapping keeps whether a value is absent.

law maybe_default_map provedsource · line 146 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> @-d:A -> {Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) == f(Maybe.default(&2, A, m, d)) : B}

The default of a map, with the mapped default, is the mapped default of the original.

law maybe_or_none provedsource · line 162 · raw

@-A:Data -> @m:Maybe<&2, A> -> {Maybe.or(&2, A, m, None{}) == m : Maybe<&2, A>}

None is a right identity for or.

law maybe_or_assoc provedsource · line 175 · raw

@-A:Data -> @m:Maybe<&2, A> -> @-n:Maybe<&2, A> -> @-k:Maybe<&2, A> -> {Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) == Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) : Maybe<&2, A>}

Or is associative.

law maybe_bind_map provedsource · line 190 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> B) -> @-g:(@_:B -> Maybe<&2, C>) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) == Maybe.bind(&2, A, C, m, x => g(f(x))) : Maybe<&2, C>}

Binding after a map binds the composition.

law maybe_map_bind provedsource · line 207 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-g:(@_:B -> C) -> @m:Maybe<&2, A> -> {Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) == Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) : Maybe<&2, C>}

Mapping after a bind maps inside the bound function.

law maybe_pure_bind_sym provedsource · line 226 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-x:A -> {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}

Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.

law maybe_bind_pure_sym provedsource · line 237 · raw

@-A:Data -> @m:Maybe<&2, A> -> {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}

Right identity: binding pure is the identity, reversed to rewrite toward the simple side.

law maybe_bind_assoc_sym provedsource · line 246 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-g:(@_:B -> Maybe<&2, C>) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) == Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) : Maybe<&2, C>}

Bind is associative, reversed to rewrite toward the simple side.

law maybe_map_pure_sym provedsource · line 259 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @-x:A -> {Maybe.pure(&2, B, f(x)) == Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) : Maybe<&2, B>}

Mapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.

law maybe_map_compose_sym provedsource · line 270 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> B) -> @-g:(@_:B -> C) -> @m:Maybe<&2, A> -> {Maybe.map(&2, A, C, x => g(f(x)), m) == Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) : Maybe<&2, C>}

Mapping a composition maps the composition, reversed to rewrite toward the simple side.

law maybe_map_id_sym provedsource · line 283 · raw

@-A:Data -> @m:Maybe<&2, A> -> {m == Maybe.map(&2, A, A, x => x, m) : Maybe<&2, A>}

Mapping the identity gives the value back, reversed to rewrite toward the simple side.

law maybe_bind_none_sym provedsource · line 292 · raw

@-A:Data -> @-B:Data -> @m:Maybe<&2, A> -> {None{} == Maybe.bind(&2, A, B, m, x => None{}) : Maybe<&2, B>}

Binding a function that always fails gives None, reversed to rewrite toward the simple side.

law maybe_map_eq_bind_sym provedsource · line 302 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, B, m, x => Maybe.pure(&2, B, f(x))) == Maybe.map(&2, A, B, f, m) : Maybe<&2, B>}

Mapping is binding the function followed by pure, reversed to rewrite toward the simple side.

law maybe_is_some_map_sym provedsource · line 313 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.is_some(&2, A, m) == Maybe.is_some(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}

Mapping keeps whether a value is present, reversed to rewrite toward the simple side.

law maybe_is_none_map_sym provedsource · line 324 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> {Maybe.is_none(&2, A, m) == Maybe.is_none(&2, B, Maybe.map(&2, A, B, f, m)) : Bool}

Mapping keeps whether a value is absent, reversed to rewrite toward the simple side.

law maybe_default_map_sym provedsource · line 335 · raw

@-A:Data -> @-B:Data -> @-f:(@_:A -> B) -> @m:Maybe<&2, A> -> @-d:A -> {f(Maybe.default(&2, A, m, d)) == Maybe.default(&2, B, Maybe.map(&2, A, B, f, m), f(d)) : B}

The default of a map, with the mapped default, is the mapped default of the original, reversed to rewrite toward the simple side.

law maybe_or_none_sym provedsource · line 347 · raw

@-A:Data -> @m:Maybe<&2, A> -> {m == Maybe.or(&2, A, m, None{}) : Maybe<&2, A>}

None is a right identity for or, reversed to rewrite toward the simple side.

law maybe_or_assoc_sym provedsource · line 356 · raw

@-A:Data -> @m:Maybe<&2, A> -> @-n:Maybe<&2, A> -> @-k:Maybe<&2, A> -> {Maybe.or(&2, A, m, Maybe.or(&2, A, n, k)) == Maybe.or(&2, A, Maybe.or(&2, A, m, n), k) : Maybe<&2, A>}

Or is associative, reversed to rewrite toward the simple side.

law maybe_bind_map_sym provedsource · line 367 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> B) -> @-g:(@_:B -> Maybe<&2, C>) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, C, m, x => g(f(x))) == Maybe.bind(&2, B, C, Maybe.map(&2, A, B, f, m), g) : Maybe<&2, C>}

Binding after a map binds the composition, reversed to rewrite toward the simple side.

law maybe_map_bind_sym provedsource · line 380 · raw

@-A:Data -> @-B:Data -> @-C:Data -> @-f:(@_:A -> Maybe<&2, B>) -> @-g:(@_:B -> C) -> @m:Maybe<&2, A> -> {Maybe.bind(&2, A, C, m, x => Maybe.map(&2, B, C, g, f(x))) == Maybe.map(&2, B, C, g, Maybe.bind(&2, A, B, m, f)) : Maybe<&2, C>}

Mapping after a bind maps inside the bound function, reversed to rewrite toward the simple side.