Catena scratchpad

code.catena.sh

#### Library definitions ########################
#### drop
drop2 := drop drop;
drop3 := drop drop2;
drop4 := drop drop3;
drop5 := drop drop4;

#### nip
nip   := dip [drop];

#### dup
# dup2 :: a b → a b a b
dup2  := dip [swap]
         copy
         dip [copy];

# dup3 :: a b c → a b c a b c
dup3  := dip [bury]
         copy
         dip [dup2];

# dup4 :: a b c d → a b c d a b c d
dup4  := dip [bury2]
         copy
         dip [dup3];

# swap3 :: a b c → c b a
swap3 := dig swap;

#### dip
dip2  := dip prepend [dip]  wrap;
dip3  := dip prepend [dip2] wrap;
dip4  := dip prepend [dip3] wrap;
dip5  := dip prepend [dip5] wrap;

#### dig
dig0  := swap;   # for completeness
#dig   := swap dip [swap];
dig   := twice [swap];
dig2  := swap dip [dig];
dig3  := swap dip [dig2];
dig4  := swap dip [dig3];

#### dig* (dig with save)
dig0* := dig0 dip  [copy];
dig*  := dig  dip2 [copy];
dig2* := dig2 dip3 [copy];
dig3* := dig3 dip4 [copy];
dig4* := dig4 dip5 [copy];

#### bury
bury0 := swap;   # for completeness
bury  := dip [swap]  swap;
bury2 := dip [bury]  swap;
bury3 := dip [bury2] swap;
bury4 := dip [bury3] swap;

=* := = dip [copy];
+* := + dip [copy];
-* := - dip [copy];
** := * dip [copy];
/* := / dip [copy];

#### Testing area ###############################
if   := unwrap choose;
sub  := - swap;
sub1 := sub 1;
+1   := + 1;

# not :: Bool → Bool
not  := choose false true;

# != :: a a → Bool
!= := not =;

# Tail-recursion combinator (calls `code` until `pred*` holds)
# tprec :: [*A → *B] [*A → Bool *A] *A → *B
tprec := if   # TODO: Simplify
         dip [ [] ]
         dip [unwrap]
         prepend [tprec]
         twice [push]
         dup2;

# while :: [*A → Bool *A] [*A → *B] *A → *B
while := tprec swap;

# if [] `[,tprec f pred' ,f] (pred' *Input)

# dip copy :: [*A → *B] *A → [*A → *B] *B
# unwrap dip copy :: [*A → *A] *A → *A

call* := dip copy;
# ([*A → *B] b *A → [*A → *B] b *B)

keep  := dip [unwrap] dig0*;
keep2 := dig dip2 [unwrap] dig* dig*;

twice := unwrap dip2 copy;

# accumulateN code pred acc0 =
#   drop
#   while [pred copyN]
#         code
#   swapN acc0;

# [*A] [*B] → [*B *A]
append := prepend swap;

# code pred acc0 a b c
# accumulate :: [a a b → a b] [a → Bool] b a → b
accumulate := drop
              tprec
              twice [append [copy]]
              dip2 [swap];

#x xs
#x (x:xs)
iota := accumulate [ sub1
                     dip [push] ]
                   [ != 0 ]
                   [];

# foldl :: [a b → a] a [*:b] → a
# foldl f y0 xs; f y0 x
foldl := nip drop
         while [ not empty? dig* ]
               [ call*
                 dip2 [pop] ];

## Hypothetical, but `begin` is untypeable?
# foldl := begin [[while [not empty? dig*]
#                        [call*
#                         dip2 [pop]]]
#                 [drop]
#                 [nip]]

# reverse :: [a → b] [*:a] → [*:b]
# reverse xs
reverse := foldl [ push swap ] [];

# map :: [a → b] [*:a] → [*:b]
# map f xs; f x
map := reverse
       nip
       foldl [ push swap
               dip [unwrap dig*] ]
             []
       swap;

# filter :: [a → Bool] [*:a] → [*:a]
# filter f xs; f x
#choose [] [x] acc xs f
filter := reverse
          foldl [ prepend  # FIXME
                  choose swap [] wrap
                  swap3
                  dip [unwrap dig2* copy] ]
                []
          swap;

#### *BROKEN* version -- to test the future typechecker!
# filter := reverse
#           foldl [ prepend
#                   choose swap [] wrap
#                   swap3
#                   dip [unwrap dig2* copy] ]
#                 []
#           swap;

# fac :: Num → Num
fac := accumulate [ sub1
                    dip [*] ]
                  [ != 1 ]
                  1;

length  := foldl [+1 nip] 0;

sum     := foldl [+] 0;
product := foldl [*] 1;


#fac 5;
#product iota 5;


# vim: set ft=catena:

scratchpad.md

Catena Scratchpad

Catena is an experimental statically-typed, concatenative programming language. This file consists of random scribblings and notes related to the same.

Type signatures of some functions

copy   ::   a → a a                       ::     a  *R →  a a  *R
swap   :: a b → b a                       ::   a b  *R →  b a  *R
drop   ::   a →                           ::     a  *R →       *R
  { 'pop'? }

wrap   ::   a  → [a]                      ::     a  *R → [→ a] *R
unwrap :: [*A] → *A                       :: [→ *A] *R →   *A  *R
clean  ::  *A  →                          ::    *A  *R →       *R

apply  ::   [*A → *B] *A → *B
  (= `unwrap` with tighter type?) (no: with wider type!)
bind   :: [a *A → *B]  a → [*A → *B]      :: [a *A → *B] a *R → [*A → *B] *R
  { unneeded? maybe concat replaces this? }
partial-results :: [*A → b *B] → [*A → b [*B]]
  {needs better name}

pop    :: [a *A:a] → a [*A:a]
push   :: a [*A:a] → [a *A:a]
concat :: [*A:a] [*B:b] → [*A:a *B:b]
  { are these even needed? type propagation → if input is homogenous, then
    output is too }

pop'   :: [a *A] → a [*A]
push'  :: a [*A] → [a *A]
concat':: [*A] [*B] → [*A *B]

choose :: a a Bool → a

dip    :: [*A → *B] a     *A → a     *B
dip2   :: [*A → *B] a b   *A → a b   *B
dip3   :: [*A → *B] a b c *A → a b c *B

foldl  :: [a b → a] a [*B:b] → a
foldr  :: [b a → a] a [*B:b] → a
map    :: [a → b] [*A:a] → [*B:b]

Type unification

TODO: Step-by-step algorithm detailing how unification between various (A,B) type-vector pairs should work.

(Should Bound be its own "sort"?)

(Bound,  Bound)   → succeed if equal in value
(Bound,  `$`)     → fail
(Single, Bound)   → bind A←B (substitute Single for Bound)
(Single, Single)  → link A=B
(Single, `$`)     → fail
(Vector, Bound)   → substitute Vector for (Bound, Vector)
(Vector, Single)  → substitute Vector for (Single, Vector)
(Vector, Vector)  → link A=B  {??}
(Vector, `$`)     → substitute Vector for nothing (empty match)
(Quot,   Quot)    → unify A.from with B.from; A.to with B.to
(Quot,   `_`)     → fail
(`$`,    `$`)     → succeed
(`$`,    `_`)     → fail
Otherwise, unify (b,a)

1      ::        *R → Num *R
wrap   ::      a *R → [a] *R
unwrap :: [→ *A] *R → *A  *R

unwrap wrap 1 1

Grammar

The formal grammar of the type system and of valid programs themselves.

Type grammar

# stack-effect      ← type-vector "*R" "→" type-vector "*R"
function          ← type-vector "→" type-vector
# type-vector       ← (single-type)* (type-vector-var)*
type-vector       ← (single-type)* (type-vector-var)?
type-vector-var   ← type-vector-ho / type-vector-he
type-vector-ho    ← type-vector-var' type-clarifier
type-vector-he    ← type-vector-var'
type-clarifier    ← ":" single-type
single-type       ← concrete-type / single-type-var / quotation
quotation         ← "[" function "]"

concrete-type     ← UppercaseLetter LetterOrDigit+
single-type-var   ← LowercaseLetter LetterOrDigit+
type-vector-var'  ← "*" UppercaseLetter LetterOrDigit+

LetterOrDigit     ← UppercaseLetter / LowercaseLetter / Digit
UppercaseLetter   ← (defined by Unicode)
LowercaseLetter   ← (defined by Unicode)
Digit             ← (defined by Unicode)

Language grammar

(Doesn't include types yet)

program       ← program-part? (";" program-part)*
program-part  ← assignment / phrase
assignment    ← separator? identifier ":=" program separator?
phrase        ← separator? ((word / quotation) separator)*
word          ← !reserved-word IdentifierChar+
quotation     ← "[" phrase "]"
separator     ← WhiteSpace+

reserved-word ← ":="

WhiteSpace    ← (defined by Unicode)
WordChar      ← (Any character not in WhiteSpace, which is not "[", "]" or ";")