title: APL
author: Keith A. Lewis
institute: KALX, LLC
classoption: fleqn
fleqn: true
abstract: A Programming Language
...
\newcommand\bm{\mathbf}
\newcommand\BB{\bm{B}}
\newcommand\CC{\bm{C}}
\newcommand\NN{\bm{N}}
\newcommand\RR{\bm{R}}
\newcommand\ZZ{\bm{Z}}
\newcommand\MM{\bm{M}}
\newcommand\FF{\bm{R}}
\newcommand\st{\mid}
\newcommand\scan{\backslash}
\newcommand\fold{/}
\newcommand\add{+}
\newcommand\sub{-}
\newcommand\mul{×}
\renewcommand\div{÷}
\newcommand\exec{!}
\renewcommand\stop{'}
\newcommand\uniq{ν}
\newcommand{\f}{\square}
\renewcommand{\t}{\blacksquare}
\newcommand{\take}{\uparrow}
\newcommand{\drop}{\downarrow}
\newcommand{\dom}{\operatorname{dom}}
\newcommand{\ran}{\operatorname{ran}}
\renewcommand{\ker}{\operatorname{ker}}
Let's give names to things.
The primitive types are
booleans $\BB$,
integers $\ZZ$,
non-negative integers $\NN$,
real numbers $\RR$,
and characters $\CC$.
We have $\BB\subseteq\NN\subseteq\ZZ\subseteq\RR$ as rings.
We assume $u\colon\CC\to\NN$ is an encoding of the set of characters. (E.g., UTF-8 codepoints)
Primitive types are classified by mathematical objects: set, monoid, group, ring, field:
boolean (field),
integer (commutative ring),
natural number (monoid),
real number (field),
character (set).
We write $\BB = {\f,\t}$ where $\f$ represents false and $\t$ represents true.
$(A\times B)\to C\cong A\to (B\to C)$ by $f(a,b) = c \leftrightarrow f,(a)b = c$ or $f,(a)b = f(a,b)$.
$A\to (B\to C) \cong (A\times B)\to C$ by $g(a)b = c \leftrightarrow g(a,b) = c$ or $g(a,b) = g(a)b$.
$\pi(a,b) = (a,b)$, $\pi_0(a,b) = a$, $\pi_1(a,b) = b$.
If $X$, $X_i$ are types
array $x = [x_1,\ldots,x_n]\in X^n\cong n\to X$, $x[i] = x_i$.
$(I\times n)^A x (-n\times I)^A \to I^A$
tuple $x = \langle x_1,\ldots,x_n\rangle\in\prod X_{i\in\NN}$, $n\to(\prod X_i\to X_i)$,
$n\mapsto π_i$,
$x\langle i\rangle = π_i(x) = x_i$.
union $x = {\ldots,x_i,\ldots} = \langle i,x_i\rangle\in\coprod_{i\in n} X_i$, $n\to(X_i\to\coprod X_i)$,
$n\mapsto ν_i$, $x{i} = ν_i(x) = \langle i,x_i\rangle$.
sequence $x = (x_0,\ldots,x_{n-1}) \in X^* = \coprod_{n\in\NN} X^n$ and define
$*x = x_0$,
$+x = (x_1,\ldots,x_{n-1})$, $?x$ if and only if $n\ge 0$, i.e., $x$ is not empty.
Note $x\in\dom *$ iff $?x$.
Define $x = y$ if $*x = *y$ and $+x = +y$ or if $x$ and $y$ are both empty.
The function concatenate $,\colon X^\times X^\to X^$
written $,(x,y) = x,y$
is defined by $(x,y) = *x$ if $?x$ and $y$ if not $?x$,
$+(x,y) = (+x,y)$ if $?x$ and $(x,+y)$ if not $?x$,
$?(x,y) = ?x\vee ?y$ where $\vee$ is logical or.
Note $x,() = x$ and $(),y = y$ for $x,y\in X^$ so
sequences are a monoid under concatenation with unit the empty sequence.
If $x = (x_0,\ldots,x_{n-1})$ is a sequence let
$[x] = [x_0,\ldots,x_{n-1}]\in X^n$ be the array it determines
and $\langle x\rangle = \langle x_0,\ldots,x_{n-1}\rangle$ be the (homogeneous) tuple
it determines.
exponential $f\in Y^X = {f\colon X\to Y}$ is the set of all functions from $X$ to $Y$.
We also write $X\to Y$ for $Y^X$.
relation $R\subseteq X\times Y$. Write $xRy$ for $\langle x,y\rangle\in R$
and $R' = {\langle y, x\rangle \st xRy}\subseteq Y\times X$ for its transpose.
The domain of $R$ is $\dom R = π_X(R)\subseteq X$ and
the range is $\ran R = π_Y(R)\subseteq Y$.
The right coset $xR = {y\in Y \st xRy}\subseteq Y$ for $x\in X$,
the left coset $Ry = {x\in X \st xRy}\subseteq X$ for $y\in Y$.
The right cosets ${xR \st x\in X}$
parition $\ran R$ and the left cosets ${Ry \st y\in Y}$ partition $\dom R$.
The graph of a function $f\in Y^X$ is
${\langle x,y\rangle \st f(x) = y}\subseteq X\times Y$. A relation $R$ is a function if the
right coset $xR$ is a singleton for all $x\in X$ and we
write $R(x)$ for that unique element.
itoa is $ι = (0,1,2,\ldots)\in\NN^*$
The function take is $\take\colon\NN\times X^\to X^$
defined by $\take(n,x) = (*x), \take(n - 1, +x))$, $\take(0,x) = ()$, $\take(n,()) = ()$,
where $(x_0, ()) = x_0$.
The function drop is $\drop\colon\NN\times X^\to X^$
defined by $\drop(n,x) = \drop(n - 1, +x)$, $\drop(0,x) = x$, $\drop(n,()) = ()$.
The function itoa is $ι\colon\NN\to \NN^*$ $ι\mapsto (0,\ldots,n-1)$.
The evaluation function $ε_Y^X = ε\colon (X\to Y)\times X\to Y$
is $ε(f,x) = f(x)\in Y$, $f\in Y^X$, $x\in X$.
monoid folds $\star\colon X\times X\to X$
left fold $(\star\colon X^n\to X$, $(\star(x_0,\ldots,x_n) = x_0\star(x_1\dots x_n)$
right fold $)\star\colon X^n\to X$, $)\star(x_0,\ldots,x_n) = (x_0\dots x_{n-1})\star x_n$
The curry function $γ\colon ((X\times Y)\to Z)\to (X\to(Y\to Z))$ is
$(γ(f)(x))(y) = f(x,y)\in Z$, $f\in X\times Y\to Z$, $x\in X$, $y\in Y$.
The uncurry function $γ^\colon ((X\to (Y\to Z))\to (X\times Y\to Z)$
is $(γ^(f))(x,y) = f(x,y)\in Z$, $f\in X\to(Y\to Z)$, $x\in X$, $y\in Y$.
Use $.$ for composition. If $f\colon X\to Y$ identify $x$ with the constant function $K_x$.
Interpret $f.x$ as $f.K_x$ so $f.x(y) = f.K_x(y) = f(K_x(y)) = f(x)$ for all $y$.
If $x\in X$, $y\in Y$ write $x,y$ for $(x,y)\in X\times Y$.
The shape function is $ρ\colon\NN^k\to (\NN^{k-1}\to\NN)$, $ρ\mapsto(n \mapsto n)$,
$ρ(n,\ldots)\mapsto ((i,\ldots) \mapsto i + n ρ(\ldots)(\ldots))$
A function $p\colon X\to\iota n$ determines a partition on $X$ where $i\sim i'$ iff $p(i) = p(i')$.
Example: s = "a,bc,def" is a string in $\CC^{\iota 8}$. Using cyclic arrays
$= "," s$ is $\f\t\f\f\t\f\f\f$ so $\add\scan = "," s$ is $0111222$.
Define $\uniq\colon X^n\to X^m$ by $\uniq x_0 x_1 \ldots = x_0 \nu x_2 \ldots$
if $x1 = x0$ and $\uniq x_0 x_1 \ldots = x_0 \nu x_1 \ldots$ if $x_1 \not= x_0$.