Definitions
Nearby Words

# Cat (programming language)

The Cat programming language is a functional stack-oriented programming language inspired by the Joy programming language. Joy and Cat differ from most functional languages (e.g Scheme, Haskell) and language formalisms (e.g. lambda calculus, combinatory logic) in that they are based on the composition of functions rather than function application Cat and Joy both bear more resemblance to combinatorial logic calculi (such as the SKI calculus or the B,C,K,W system) than to the lambda calculus due to the lack of names.

The Cat language was designed with static typing in mind, and as such there is somewhat less flexibility but more safety than is available in the Joy programming language.

Cat is intended as a multi-purpose language with an emphasis on usage as an intermediate language and as an educational language.

## Semantics

Like Joy, programs in Cat are constructed from existing programs using two operations: composition and quotation All Cat programs can be thought of as functions that map from one stack to another. Because Cat has no operations that refer to previous stack states, Cat can be easily implemented using a single mutable shared stack.

Two adjacent terms in Cat imply the composition of functions that generate stacks, so the Cat program `f g` is equivalent to the mathematical expressions $g circ f$ and $g\left(f\left(x\right)\right),!$, where x is the stack input to the expression.

Programs can be quoted using the begin and quotation operators `[` and `]`. A quotation has the effect of pushing a function onto the stack without evaluating it. Quotations can be thought of as anonymous functions.

Because all Cat functions map from one stack to another, what is more informative is the number and type of values that they pop and push onto the shared stack during execution. This is known respectively as the consumption and production of a function. When discussing a Cat function, the consumed values are often called the argument, and the produced values are often called the production.

Literals in the Cat language, are constant generating functions that consume no value, and push a single function.

## Type System

The Cat type system is a set of rules which unambiguously determine the configuration of types on the stack at any given point during program execution. The type system also determines the consumption and production of a function. The programmer can provide a type annotation for a function, which resembles a cross between Forth stack comments and Haskell type signatures.

Some example of type annotations are:

` `dup : ('a -> 'a 'a)``
``` pop : ('a -> ) swap : ('a 'b -> 'b 'a) true : (-> bool) add : (int int -> int) gt : (int int -> bool) apply : ('A ('A -> 'B) -> 'B) if : ('A bool ('A -> 'B) ('A -> 'B) -> 'B) ```
`` while : ('A ('A -> 'A) ('A -> 'A bool) -> 'A)``

The type annotations are incomplete type signatures because they only describe what happens on the top of the stack. To be formal what is missing is a variable to indicate the rest of the stack This is essentially an implicit stack variable. A stack variable is of a different kind than a type variable since it can refer to zero or more types simultaneously. This is a key to the compact representation of the Cat type rules

An implementation of Cat may choose whether or not to do static type-checking. Type annotations are optional, regardless if a Cat implementation is statically typed. If type annotations are absent in a typed implementation, the types are inferred automatically by the compiler. The type annotations, if present, have to agree with the types inferred by the compiler, if performed by the compiler.

The typing rules, kind system, and operational semantics for Cat are defined in the paper "Typing Functional Stack-Based Languages"

## Differences from Joy

The Cat semantics differ from Joy primarily in that every function in Cat will always produce the same number and type of results, given the same number and type of arguments. While a function such as `if` can consume and produce a different number of values, depending on the types of the function arguments that are passed to it, the actual values themselves can not influence the types consumed or produced.

For example the following is a valid Joy function:

` `DEFINE f == [is_monday] ["I don't like Mondays"] [] ifte.``

However the corresponding function in Cat is ill-typed:

`define f { is_monday ["I don't like Mondays"] [] if }`

This is because the `if` function has the following type:

` `if : ('A bool ('A -> 'B) ('A -> 'B) -> 'B)``

The 'A and 'B in the signature are stack variables. Stack variables are differentiated from type variables in that they start with an upper-case letter, and can represent a set of zero or more types. If we write the types of the arguments to the `if` function in the previous example we would get conflicting values of the stack variable 'B:

` `["I don't like Mondays"] : (-> string)``
``` => 'A == 'B == (string) [] : (-> ) ```
``     => 'A == 'B == ()``

Because the actual types assigned to the stacks disagree the type rule are violated and a type-check error should be thrown by a compiler or interpreter.

## Implementation

The primary Cat implementation is an open-source interpreter for Windows written in C# that does not currently perform type-checking or type-inference. The Cat definition and implementation is public domain. The Cat interpreter binaries and source code are hosted with the Google open-source code hosting service.

## Example

Consider a Fibonacci function which in Python can be defined recursively as:

` `def fib(n):``
``` if n <= 1: return n else: ```
``     return fib(n-1) + fib(n-2)``

A similar implementation of the Fibonacci function in Cat follows:

` `define fib {``
``` dup 1 <= [] [dup 1 - fib swap 2 - fib +] if }```