Algebraic modules and specifications
npm install algebraic
A set of specifications of signatures on algebraic modules and an
implementation of a standard library built to match.
Algebraic is a set of Javascript objects which are known as algebraic modules
or modules when it's clear that I'm not referring to CommonJS, AMD, or ES6
import/export modules. A module contains a set of related behaviors operating
over a set of types which the module pertains to.
For instance, there is a module Array which contains operations over the
standard JS array type.
``javascript`
> var A = require("algebraic");
> A.Array.of(1)
[ 1 ]
> A.Array.plus(A.Array.of(1), A.Array.of(2))
[ 1, 2 ]
Seasoned OO-ers might find this awkward and backward—we should be doing
something like [1].concat([2]). Algebraic intentionally eschews this design
with its modular design. (If the noisy imports bother you then consider ES6
destructuring)
`javascript
import { Array } from "algebraic";
const { plus, of } = Array;
const x = plus(of(1), of(2));
`
The fastest way to describe modular design in OO-terms is to say that a module
is a class with only static methods. They, however, can also be much, much more.
A driving principle of Algebraic's design is behavior before state. What
this means is that libraries and programs should be first designed against a
specification of behavior and oblivious to the state required to pull the
behavior off. The advantage of this adage is increased modularity driven by a
clearer line between interface and implementation.
Unfortunately, standard OO practice conflates behavior and state
heavily---indeed some take the definition of an object to be the conflation of
behavior and state.
In most cases module objects themselves are completely state free. Indeed, in
any case where they are not the observation of that state ought to be severely
restricted and the intended behavior favored. Instead all of the state of
Algebraic arises from the arguments passed to and received from module
behaviors.
Immutability vastly reduces the state space of a program improving the ability
for the author to correctly reason about it's behavior. It's also assumed in
most descriptions of algebraic structures. For these reasons, Algebraic
eschews behaviors which mutate values opting instead to return new copies as
often as possible. This also provides standard sharing tricks like pre-emptive
O(1) equality checks (which Algebraic uses by default) useful for
comparison-driven programs like React-style UIs.
Note: Algebraic-style immutability is dangerous when mixed with mutable
JS code. Algebraic does not attempt to freeze or seal values and also
maximizes sharing, so mutation of an object involved in Algebraic behaviors
can have long range effects.
Algebraic takes its design inspiration heavily from two other languages and
their associated communities: ML and Haskell. Modular design of programs is
extraordinarily well done in ML languages like OCaml and SML where the static
type system helps ensure that your interfaces are well-defined and properly
used. Algebraic specifications of operations is extraordinarily well done in
Haskell where laziness, purity, and the Haskell "typeclass" mechanism drove the
use of algebraic laws over immutable values out of both necessity and splendor.
Why not OO?* Other FP-in-JS libraries (Fantasy Land, Ramda, Sanctuary, etc)
provide FP-like functionality by attaching methods to objects so that a value
x is, e.g., a Monoid when x.plus is a partially-applied monoid operation.algebraic
eschews this by placing all functionality in an object externalx
to called a module.
Immutable by default.* (Obvious cache invalidation)
Names, operations, and laws from algebra.* Programming is an exercise in
naming things. Algebra provides a large set of useful, consistent names along
with well-defined expectations for what they mean.
* Why ES6 and not something like Typescript? Three reasons.
* This is a packaging of some code originally written for a real project using
ES6, so using Typescript was not an option initially.
* I'm not confident that I like the design decisions of Typescript's type
system sufficiently to want to endorse it. An untyped system is arguably
worse, but it gives me the freedom to write exactly the code intended.
* I am writing some functions which could be well-typed but certainly would
not be in most standard type systems. Lacking a real type checker I can
introduce semi-formal notation for thee ideas and work with them.
: Decidable$3
* [X] String: Decidable, Hashable, Decidable Monoid,
Least, Total Order
* [X] Boolean
* [X]
* [X]
* [X] $3
* [X] : Decidable Monoid, Covariant, Foldable,
Traversable, Monad, Reflects Decidability
* [X] Set.OfDecidable
* [X]
* [ ]
* [X]
* [X]
* [X] * [X]
* [ ]
Specifications
$3
* Decidable {
}
definitions*
* X : Type
*
notation*
* When unambiguous, is written to mean eq(x, y).
laws*
* reflexivity: for all (a : X) a = a
* symmetry: for all a = b implies b = a.
* transitivity: for all (a b c : X) a = b and b = c implies a = c.* Hashable {
X}
definitions*
include* Decidable {X}
definitions*
* hash : X -> Int
laws*
* identity compatibility: for all if a = b then hash(a) = hash(b).$3
* Preorder {
X}
definitions*
* X : Type
*
*
*
*
*
notation*
* Where unambiguous, is written to mean leq(x, y)
laws*
* reflexivity: for all a <= a
* transitivity: for all a <= b and b <= c implies a <= c* Partial Order {
} or Poset {X}
include* Preorder {X}
implies unique* Decidable {X = X}
define* eq(a, b) = indistinguishable(a, b)
laws*
* antisymmetry: is an equivalence relation* Weak Order {
X}
include* Poset {X}
laws*
* incomparable is transitive* Total Order {
X}
include* Poset {X}
implies unique* Weak Order {X = X}
* proof: totality implies that incomparable is the empty relation
laws*
* totality: for all (a b : X) either a <= b or b <= a$3
* Least {
}
definitions*
* X : Type
* * Greatest {
}
definitions*
* X : Type
* * Bounded {
}
include* Least {X} and Greatest {X}$3
* Join {
X} / Meet {X}
include* Decidable {X}
definitions* (one of, called op)
* join : (X, X) -> X
*
notation*
* Where unambiguous, is written |
* Where unambiguous, is written &
laws*
* associativity of
* commutativity of
* idempotence of : for all (a : X) op(a, a) = a
implies unique*
* Semigroup {} with
* define plus(a, b) = op(a, b)
* Poset {} with
* define leq(a, b) = eq(a | b, b) or
* define leq(a, b) = eq(a, a & b) or* Join★ {
X} / Meet★ {X}
include* Join {X} / Meet {X} as op
definitions*
* or
* meetN : [X] -> X
laws*
* is a Monoid morphism from arrays to X
* operation compatibility: for all op(a, b) = opN([a, b])
implies unique* Least {} / Greatest {X}
* define bottom() = joinN([]) or
* define top() = meetN([])
implies unique* Monoid {}
* define zero() = opN([]]) * Lattice
include* Decidable {
X}
definitions*
* join : (X, X) -> X and
* meet : (X, X) -> X
notation*
* Where unambiguous, is written |
* Where unambiguous, is written &
laws*
implies unique* Join {X}
meet implies unique* Meet {X}
* absorption: for all (a b : X) if q = a | (a & b) and p = a & (a | b) then eq(q, p) and q = a and p = a
* Poset {} via Join {X} is compatible with Poset {X} via Meet {X}
implies unique* Poset {X}
* defined via either Join {X} or Meet {X}
projects*
* Semigroup {X} via Join {X}
* Semigroup {X} via Meet {X}* Lattice★
include* Decidable {
X}
definitions*
* join : (X, X) -> X and
* meet : (X, X) -> X
* and
* meetN : (X, X) -> X
notation*
* Where unambiguous, is written |
* Where unambiguous, is written &
implies* Bounded {}
* via implication of Least {X} and Greatest {X} from Join★ {X} and Meet★ {X} respectively
laws*
joinN implies unique* Join★ {X}
meetN implies unique* Meet★ {X}
* absorption: for all (a b : X) if q = a | (a & b) and p = a & (a | b) then eq(q, p) and q = a and p = a
* Poset {} via Join {X} is compatible with Poset {X} via Meet {X}
projects*
* Monoid {X} via Join★ {X}
* Monoid {X} via Meet★ {X} * Distributive {
X}
include* Lattice {X}
laws*
* distributivity
for all (a b c : X) let p = a & (b | c)) and q = (a & b) | (a & c) then eq(p, q) or*
dually*, for all (a b c : X) let p = a | (b & c) and q = (a | b) & (a | c) then p = q$3
* Magma {
}
definitions*
* X : Type
*
notation*
* Where unambiguous, is written x + y* Semigroup {
}
include* Magma {X} and Decidable {X = X}
laws*
* associativity of plus: for all (a b c : X) eq(plus(a, plus(b, c)), plus(plus(a, b), c))* Monoid {
}
include* Semigroup {X}
definitions*
* zero : () -> X
*
*
notation*
* Where unambiguous, is written 0
laws*
* is a zero: for all (a : X) a + 0 = a and 0 + a = a* Decidable Monoid {
}
include* Monoid {X}
definitions*
* isZero : X -> Bool
laws*
* isZero: isZero(zero())* Group {
}
include* Monoid {X}
definitions*
* negate : X -> X
*
*
notation*
* Where unambiguous, is written -x
* Where unambiguous, is written x - y
laws*
* undoes plus: for all (a : X) x - x = 0 and -x + x = 0The following 3 are very close to one another such that Ring {
} subsumes both Semiring {X} and Rng {X} but those two are incomparable.* Semiring {
X}
include* Decidable {X}
definitions*
* zero : () -> X
*
*
*
projects*
* and plus form the zero-plus Monoid {X}
* one and times form the one-times Monoid {X}
notation*
* Where unambiguous, zero() is written 0
* Where unambiguous, is written 1
* Where unambiguous, is written x + y
Where unambiguous, is written x y
laws*
* the zero-plus Monoid {} is commutative
* times-plus distributivity: for all (a b c : X)
left distributivity:
right distributivity:
annihilation: for all (a : X) 0 a = 0 and a * 0 = 0* Rng
include* Decidable {
}
definitions*
* zero : () -> X
*
*
*
*
*
notation*
* Where unambiguous, is written 0
* Where unambiguous, is written x + y
Where unambiguous, is written x y
* Where unambiguous, is written -x
* Where unambiguous, is written as x - y
projects*
* , plus, and negate form the zero-plus Group {X}
* times forms the times Semigroup {X}
laws*
* the zero-plus Group {X} is commutative
* times-plus distributivity: for all (a b c : X)
left distributivity:
right distributivity: * Ring
include* (all compatible)
* Decidable {
}
* Semiring {X}
* Rng {X}
definitions*
* zero : () -> X
*
*
*
*
*
*
notation*
* Where unambiguous, is written 0
* Where unambiguous, is written 1
* Where unambiguous, is written x + y
Where unambiguous, is written x y
* Where unambiguous, is written -x
* Where unambiguous, is written as x - y
projects*
* , plus, and negate form the zero-plus Group {X}
* one-times form the one-times Monoid {X}
laws*
* the zero-plus Group {X} is commutative
* times-plus distributivity: for all (a b c : X)
left distributivity:
right distributivity: $3
Three notational shorthands are used in this section:
, f . g = x => f(g(x)), and . = f => g => x => f(g(x)).* Parametric {
F}
definitions*
* F : Type -> Type* Reflects decidability {
}
include* Parametric {F}
implications*
* Decidable {X} implies Decidable {F X}* Covariant {
F}
include* Parametric {F}
definitions*
* map : ∀ a b . (a -> b) -> (F a -> F b)
notation*
* Where unambiguous is written [f]
laws* (category morphism)
* for all , Decidable {F X}, (fa : F X), fa = id
* for all , Decidable {F X}, (fx : F X), (g : X -> Y), (f : Y -> Z) f) = f . g* Contravariant {
}
include* Parametric {F}
definitions*
* comap : ∀ a b . (b -> a) -> (F a -> F b)
laws* (category morphism)* Apply {
}
include* Covariant {F}
notation*
When unambiguous, f x is written to mean ap(f, x).
definitions*
* ap : ∀ a b . F (a -> b) -> (F a -> F b)
*
*
*
*
laws*
composition reassociates: for all , Decidable {F Z}, (f : F (Y -> Z)), (g : F (X -> Y)), (a : F x), we let (. g) a = f (g * a).
notes*
* can be used to traverse non-empty structures* Applicative {
F}
include* Apply {F}
defintions*
* of : ∀ a . a -> F a
* traversals of "container-like" structures
*
*
notation*
* Where unambiguous, is written {x}
laws*
identity reflection:
application reflection:
interchange: * Bind {
}
include* Apply {F}
definitions*
* bind : ∀ a b . (a -> F b) -> (F a -> F b)
*
*
*
*
*
*
notation*
* Where unambiguous is written m >>= k
* Where unambiguous is written m1 >> m2
* Where unambiguous is written f1 >=> f2
projects*
* Apply {} via
* define ap(mf, mx) = mf >>= (f => f)
laws*
* associativity: * Monad {
}
include* (compatibly)
* Bind {F}
* Applicative {F}
laws*
* left identity: of >=> f = f
* right identity: * Foldable {
}
include* Covariant {F}
definitions*
* foldMap : ∀ a x . (Monoid {x}, a -> x) -> (F a -> x)
*
* defined using the universal Monoid available for all X
*
* defined by passing through arrays
*
* defined by passing through arrays
*
* defined by passing through arrays
laws*
* "seek and find": for all , all functions F a -> a?, and all
values x : F a, if f(x) exists then f(x) is in the array
toArray(x)* Traversable {
}
include* Foldable {F}
definitions*
* traverse : ∀ a b k . (Applicative {k}, a -> k b) -> (F a -> t (F b))
laws*
* See Haskell documentation$3
* Cons {
}
include* Foldable {F}
definitions*
* cons : ∀ a . (a, F a) -> F a
laws*
* "place and find": for all with Decidable {a}, for all
c : F a and x : a, we have contains(x, toArray(cons(x, c))References
* tel/ocaml-cats: An attempt to bring
statically typed algebraic interfaces to OCaml.
* fantasyland/fantasy-land: A
specification of objects which provide suitable algebraic operations. It's
another, somewhat popular point in the design space of algebraic FP in
Javascript.
* Ramda.js: An implementation of some algebraic and some
higher-order functional techniques via object-oriented Javascript.
* plaid/sanctuary: An implementation of
more advanced algebraic data types and associated functionality written For
compatibility with Ramda.
License
Copyright 2015, Reify Health ()Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.