Let's reduce the operations on rank-1 arrays (lists) down to very basic functions.
Two views on lists:
- A list is a function from indices to values
- A list is a free monoid
The first view gives ↕n
, i⊑x
and x⊏y
, which correspond to the identity function, application
and composition, and also gives f¨x
and x f¨ y
.
The second view gives ⟨⟩
and x∾y
, ⋈x
and f´x
which are identity and multiplication of the monoid
and unit and counit of the adjunction.
Extra: f⍟n x
is directly related to the universal property of natural numbers.
Using this, let's implement some other functions:
≠x
is+´1¨x
n⥊x
isn {𝕩⊏˜(≠𝕩)|↕𝕨} x
∾x
is∾´x
x⋈y
is∾○⋈
n↑x
(for n≥0) isn {(d∾𝕩) ⊏˜ (≠𝕩)⊸≥⊸× 1+↕𝕨} x
, whered
is the default value ofx
n↓x
(for n≥0) is{𝕩 ⊏˜ 𝕨+↕𝕨-˜≠𝕩}
⌽x
is(↕∘≠-˜1-˜≠)⊸⊏ x
andn⌽x
isn {𝕩⊏˜(≠𝕩)|𝕨+↕≠𝕩} x
m/l
ism (∾⥊⟜⋈¨) x
x⊐y
isx {(⊑/∾≠)¨<˘𝕩≡⌜𝕨} y
(table could be replaces with eaches)∊x
is{∨˝∧⟜(¬·»∨`)˘≡⌜˜𝕩} x
K does not have that many primitives. Basic are:
!n
,x.i
andx@y
, alsof'x
()
,x,y
,,x
andf/x
Deriving the implementation of other verbs and adverbs is left to the reader as an exercise.