LAWS.bend source
LAWS.bend on the hub · documented module
import Baseimport ./lib.bend as N# When from_list succeeds on a Cons, the payload is that Cons as NE.law from_list_cons: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.from_list(a, A, h <> t) == Some{N.NE{h, t}} : Maybe<a, N.NonEmpty<a, A>> }# from_list on Nil is None.law from_list_nil: for -a: Quant for -A: Kind(a) { N.NonEmpty.from_list(a, A, Nil{}) == None{} : Maybe<a, N.NonEmpty<a, A>> }# to_list undoes the NE encoding: recovers head <> tail.law to_list_ne: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.to_list(a, A, N.NE{h, t}) == h <> t : List<a, A> }# to_list(one(x)) is the singleton list.law to_list_one: for -a: Quant for -A: Kind(a) for x: A { N.NonEmpty.to_list(a, A, N.NonEmpty.one(a, A, x)) == x <> Nil{} : List<a, A> }# from_list ∘ to_list recovers Some{NE{h,t}}.law from_to_list_ne: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.from_list(a, A, N.NonEmpty.to_list(a, A, N.NE{h, t})) == Some{N.NE{h, t}} : Maybe<a, N.NonEmpty<a, A>> }# length(NE{h,t}) is always Succ of List.length(t) (hence ≥ 1).law length_succ_tail: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.length(a, A, N.NE{h, t}) == 1n+List.length(a, A, t) : Nat }# length(one(x)) is 1.law length_one: for -a: Quant for -A: Kind(a) for x: A { N.NonEmpty.length(a, A, N.NonEmpty.one(a, A, x)) == 1n : Nat }# head(one(x)) is x.law head_one: for -a: Quant for -A: Kind(a) for x: A { N.NonEmpty.head(a, A, N.NonEmpty.one(a, A, x)) == x : A }# head/tail project the NE constructor.law head_ne: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.head(a, A, N.NE{h, t}) == h : A }law tail_ne: for -a: Quant for -A: Kind(a) for h: A for t: List<a, A> { N.NonEmpty.tail(a, A, N.NE{h, t}) == t : List<a, A> }# tail(one(x)) is Nil.law tail_one: for -a: Quant for -A: Kind(a) for x: A { N.NonEmpty.tail(a, A, N.NonEmpty.one(a, A, x)) == Nil{} : List<a, A> }# one(x) is NE{x, Nil}.law one_is_ne: for -a: Quant for -A: Kind(a) for x: A { N.NonEmpty.one(a, A, x) == N.NE{x, Nil{}} : N.NonEmpty<a, A> }# cons(x, one(y)) prepends x.law cons_one: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y)) == N.NE{x, y <> Nil{}} : N.NonEmpty<a, A> }# head(cons(x, one(y))) is x.law head_cons_one: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.head(a, A, N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y))) == x : A }# to_list(cons(x, one(y))) is x <> y <> Nil.law to_list_cons_one: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.to_list(a, A, N.NonEmpty.cons(a, A, x, N.NonEmpty.one(a, A, y))) == x <> (y <> Nil{}) : List<a, A> }# snoc(one(x), y) appends y.law snoc_one: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.snoc(a, A, N.NonEmpty.one(a, A, x), y) == N.NE{x, y <> Nil{}} : N.NonEmpty<a, A> }# length(snoc(one(x), y)) is 2.law length_snoc_one: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.length(a, A, N.NonEmpty.snoc(a, A, N.NonEmpty.one(a, A, x), y)) == 2n : Nat }# append(one(x), one(y)) is NE{x, y <> Nil}.law append_ones: for -a: Quant for -A: Kind(a) for x: A for y: A { N.NonEmpty.append(a, A, N.NonEmpty.one(a, A, x), N.NonEmpty.one(a, A, y)) == N.NE{x, y <> Nil{}} : N.NonEmpty<a, A> }