PLaMo翻訳の markdown 翻訳 (日本語→英語) でマークアップが崩れた例

translated_TUTORIAL_ja.md

CPL Tutorial

Introduction

CPL (Categorical Programming Language) is a programming language designed based on concepts from category theory. In CPL, what are typically referred to as "data types" and "functions" in conventional programming languages are instead treated as "objects" and "morphisms" in category theory.

Set Theory	Functional Programming	CPL
Set	Data Type	Object
Mapping	Function	Morphism

Key Features of CPL

• Category-theoretic data type definition: All data types are defined using category theory concepts, specifically F,G-dialgebras—a generalization of adjunctions and F-(co)algebras
• Type safety: A robust type system grounded in category theory principles
• Functional programming: Only total functions are supported, ensuring pure computation without side effects
• Duality: Symmetric design using both left objects (initial structure) and right objects (terminal structure)

Prerequisite Knowledge

For optimal understanding, familiarity with the following:

• Basic programming concepts
• Experience with functional programming languages like Haskell (though not mandatory)

No prior knowledge of category theory is required. Through this tutorial, you'll learn both CPL usage and fundamental category theory concepts.

What You'll Learn from This Tutorial

• Basic CPL operations: REPL usage, data type definition, and function definition
• Fundamental category theory concepts: Terminal/initial objects, products/coproducts, exponential objects, etc.
• The distinction between left objects and right objects, and the concept of duality in category theory
• Practical programming examples: Natural numbers, lists, infinite lists, etc.

Table of Contents

• Introduction

• Basic Commands

• Initial Screen Display

• Defining Terminal Objects

• Defining Cartesian Products

• Defining Exponential Objects

• Defining the Natural Numbers Object

• Defining Coproducts

• Displaying Types

• Composing Arrows and Identity Arrows

• Assigning Names to Expressions

• Computation

• List Types

• Infinite Lists

• Category Theory Background: Left vs. Right

• Summary

• References

Basic Commands

The CPL REPL (Read-Eval-Print Loop) supports the following commands. This section provides only an overview, with detailed usage examples to be learned through practical application.

• edit: Enters multi-line editing mode. Use this for defining data types. End editing mode by pressing semicolon (;)

• show <expression>: Displays the type (domain and codomain) of an arrow (function)

• show object <functor>: Displays detailed information about an object (data type)

• show function <function>: Displays the type of a factorizer (higher-order function) or user-defined function

• let <name> = <expression>: Defines an arrow by assigning it a name

• let <name>(<arguments>) = <expression>: Defines an arrow with parameters

• simp <expression>: Simplifies (computes) the given expression

• simp full <expression>: Fully simplifies the expression (use when simp alone cannot complete simplification)

• it: Refers to the result from the previous computation

• load <filename>: Loads definitions from a file

• help: Displays help information

• exit: Exits the CPL environment

Initial Screen

Upon startup, the interface appears as follows:

Categorical Programming Language (Haskell version)
version 0.1.0

Type 'help' for assistance

cpl> 

Defining the Terminal Object

CPL has no built-in data types, and all data types must be explicitly defined.

Since every operation requires the terminal object—corresponding to the unit type in other functional programming languages—we begin by defining this fundamental concept.

In category theory, a terminal object 1 is defined as "an object such that for every object X, there is exactly one arrow from X to 1." It serves as an "endpoint" representing an object with no information (or containing only one value). The single arrow is written as !.

Visually, this corresponds to the following situation:

Correspondences to programming concepts:

• Haskell's () type (unit type)
• void or unit types in other languages
• The concept of "a type containing exactly one value"

Now, let's define the terminal object in CPL. Using the edit command, enter multi-line editing mode, input your data type definition, and exit multi-line editing mode by pressing semicolon ;.

cpl> edit
| right object 1 with !
| end object;
right object 1 defined

The output "right object 1 defined" confirms that the terminal object 1 has been successfully defined.

`

Detailed information about a defined object can be viewed using show object.

cpl> show object 1
right object 1
- natural transformations:
- factorizer:
    
    ----------
    !: *a -> 1
- equations:
    (RFEQ): 1=!
    (RCEQ): g=!
- unconditioned: yes
- productive: ()

When object 1 is defined, a special arrow ! is also defined from any object to the terminal object.

The show command can also be used to display the arrow's type (domain and codomain). Here, *a is a variable representing an object, so this represents an arrow from any object to the terminal object 1.

cpl> show !
!
    : *a -> 1

Defining the Product

Next, we'll define the product. In category theory, the product operation combines two objects into a single object.

In category theory, the product A × B (prod(a,b) in CPL) is defined as "an object that preserves the information of both objects A and B." It satisfies the following properties:

• Existence of projection arrows π₁: A × B → A and π₂: A × B → B
  • For any object X with arrows f: X → A and g: X → B to A and B respectively, there exists a unique arrow ⟨f,g⟩: X → A × B such that π₁ ∘ ⟨f,g⟩ = f and π₂ ∘ ⟨f,g⟩ = g (this is referred to as the universal property).

Visually represented as a diagram:

Correspondences with programming concepts:

• Haskell's (a, b) type (tuple)
• Pairs or structures in other languages
• The concept of "a type that combines two values"

Now, let's define the product in CPL:

cpl> edit
| right object prod(a,b) with pair is
|   pi1: prod -> a
|   pi2: prod -> b
| end object;
right object prod(+,+) defined

(Note in the definition of pi1 and pi2 that the object prod we're defining now is omitted from the arguments. This is intended as "we define prod(a,b) as the most universal x equipped with x -> a and x -> b," but think of it as reusing the name prod instead of introducing a new name x)

.

Unlike in the case of terminal objects, the product prod(a,b) is an object that takes parameters, and the resulting definition displays as prod(+,+). The + indicates covariance, and we can see that prod takes two arguments and is covariant with respect to both arguments. Use show object to display detailed information.

cpl> show object prod
right object prod(+,+)
- natural transformations:
    pi1: prod(*a,*b) -> *a
    pi2: prod(*a,*b) -> *b
- factorizer:
    f0: *a -> *b  f1: *a -> *c
    ------------------------------
    pair(f0,f1): *a -> prod(*b,*c)
- equations:
    (REQ1): pi1.pair(f0,f1)=f0
    (REQ2): pi2.pair(f0,f1)=f1
    (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
    (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
- unconditioned: yes
- productive: (yes,yes)

Unlike terminal objects, in the case of products, both projection arrows pi1 and pi2 are defined simultaneously (you can also check their types using the show command).

Additionally, a function (factorizer) pair is also defined, which constructs pair(f,g): a -> prod(b,c) from f: a -> b and g: a -> c. The arrow previously written as ⟨f,g⟩ in this context is now denoted as pair(f,g) in the defined product. The factorizer pair itself is not an arrow and cannot be displayed using show; instead, use show function to display its type.

cpl> show function pair
f0: *a -> *b  f1: *a -> *c
------------------------------
pair(f0,f1): *a -> prod(*b,*c)

Furthermore, while prod maps objects a and b to the object prod(a,b), it also maps arrows f: a -> c and g: b -> d to prod(a,b) -> prod(b,d). In category theory, a functor maps objects to objects and arrows between objects to arrows between mapped objects. Using show function prod, you can verify the type of prod's action on arrows.

cpl> show function prod

f0: *a -> *c  f1: *b -> *d
---------------------------------------
prod(f0,f1): prod(*a,*b) -> prod(*c,*d)

Furthermore, examining equations reveals that the following four equalities hold. Here, the . notation represents arrow composition, meaning g.f means "first apply f, then apply g" (corresponding to the mathematical notation g ∘ f).

• (REQ1): pi1.pair(f0,f1)=f0
  • (As stated earlier as a property of the product)
• (REQ2): pi2.pair(f0,f1)=f1
  • (Same as above)
• (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
  • (Definition of prod in terms of pair and pi1, pi2)
• (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
  • (If g satisfies the same conditions as pair(f0,f1), then g=pair(f0,f1), i.e., pair(f0,f1) is unique)

Definition of Exponential Object

Next, we define the exponential object, which is a structure for treating functions as values.

**

The exponential object Bᴬ (denoted as exp(a,b) in CPL) represents "the object that encodes all arrows from A to B." It possesses the following properties:

• An evaluation arrow eval: Bᴬ × A → B exists, allowing functions to be applied to values
  • (While we call it eval here, in functional programming contexts, apply would be a more natural name)
• For any arrow f: X × A → B, there exists a unique curried arrow curry(f): X → Bᴬ satisfying eval ∘ (curry(f) × I) = f
  • (Here, I: A → A represents the identity arrow, and × denotes the product arrow operation)

Visualized as a diagram, it appears as follows:

Why Is the Exponential Object Called a "Function Space"? Let's consider this concretely in the context of the category of sets.

• Bᴬ is the set of all functions from A to B — In the category of sets, the exponential object Bᴬ becomes the set {f | f: A → B} of functions itself.

**

• eval represents function application — eval(f, a) = f(a). In other words, it performs the operation of "taking a pair of a function f and its argument a, and returning the result of applying f to a."
• curry represents argument separation — For f: X × A → B, curry(f)(x) returns the function a ↦ f(x, a). In other words, currying transforms a two-argument function into a one-argument function that returns another function — this is precisely the operation of converting a function into a function that returns functions.
• Universality characterizes the function space — The commutativity of the diagram above — the property that "functions from X × A → B are in one-to-one correspondence with functions from X → Bᴬ" — is what uniquely characterizes Bᴬ as a function space. This correspondence is exactly the relationship between currying and function application in programming.

Correspondences with programming concepts:

• Haskell's a -> b type (function type)
• Currying and function application
• The concept of "treating functions as first-class values"

A category equipped with terminal objects, product objects, and exponential objects is called a Cartesian Closed Category, which forms the theoretical foundation for lambda calculus and functional programming.

Now, let's define the exponential object in CPL:

cpl> edit
| Define right object exp(a,b) with curry as:
|   eval: prod(exp,a) -> b
| end object;
right object exp(-,+) defined

We can display detailed information using show object:

cpl> show object exp
right object exp(-,+)
- Natural transformations:
    eval: prod(exp(*a,*b),*a) -> *b
- Factorizer:
    f0: prod(*a,*b) -> *c
    ---------------------------
    curry(f0): *a -> exp(*b,*c)
- Equations:
    (REQ1): eval.prod(curry(f0),I)=f0
    (RFEQ): exp(f0,f1)=curry(f1.eval.prod(I,f0))
    (RCEQ): eval.prod(g,I)=f0 => g=curry(f0)
- Unconditioned: yes
- Productive: (no,no)

We can see definitions for:

• eval, which performs function application

• curry, which performs currying

• The conditions required for an exponential object in category theory

• Other relevant properties

Using show function, let's examine how the functor exp operates on its morphisms:

cpl> show function exp
f0: *c -> *a  f1: *b -> *d
------------------------------------
exp(f0,f1): exp(*a,*b) -> exp(*c,*d)

Note the directionality of the morphisms as arguments to exp, and how the parameters of exp change from domain to codomain:

• For f0 with function direction *c -> *a, the resulting parameter changes direction from *a to *c
• For f1 with function direction *b -> *d, the resulting parameter changes direction from *b to *d

This indicates that exp is a contravariant functor with respect to the first argument and a covariant functor with respect to the second argument. The notation exp(-,+) used during definition and in show object exp is a concise representation of this property.

Definition of the Natural Numbers Object

A natural numbers object is an inductively defined structure characterized by the number 0 and the successor function.

**

The natural numbers object ℕ is uniquely characterized by the following elements:

• Zero 0: 1 → ℕ (the initial value)
• Successor function s: ℕ → ℕ (also denoted as succ, the function that increments by 1)
• For any object X and morphisms z: 1 → X and f: X → X, there exists a unique morphism pr(z,f): ℕ → X defined recursively such that pr(z,f) ∘ 0 = z and pr(z,f) ∘ s = f ∘ pr(z,f)

This pr operation corresponds to mathematical induction and serves as the fundamental method for defining functions over the natural numbers.

Visualized graphically, this structure appears as follows:

Correspondences to programming concepts:

• The definition of natural numbers according to Peano's axioms

• Equivalent to Haskell data types such as:

  data Nat = Zero | Succ Nat

• Recursive computations (folding, convolution)

Now, let's define the natural numbers object in CPL:

cpl> edit
| left object nat with pr is

| 0: 1 -> nat | s: nat -> nat | end object; left object nat defined

To display the defined information, use `show object nat`:

cpl> show object nat left object nat

• Natural transformations: 0: 1 -> nat s: nat -> nat

• Factorizer: f0: 1 -> *a f1: *a -> *a

  pr(f0,f1): nat -> *a
• Equations: (LEQ1): pr(f0,f1).0=f0 (LEQ2): pr(f0,f1).s=f1.pr(f0,f1) (LFEQ): nat=pr(0,s) (LCEQ): g.0=f0 & g.s=f1.g => g=pr(f0,f1)
• Unconditioned: no
• Productive: ()

Here, `0` and `s` represent the zero and successor functions respectively, while `pr` corresponds to mathematical induction, along with the conditions they must satisfy.

## Defining the Coproduct

**The coproduct** is a structure representing "either-or," serving as the dual concept to the direct product.

The coproduct `A + B` (denoted as `coprod(a,b)` in CPL) is an object that can hold one of two values, either from object `A` or `B`:

- It includes two injection morphisms `in₁: A → A + B` and `in₂: B → A + B` (which "inject" values into the coproduct)

- For any objects `X` and functions `f: A → X` and `g: B → X`, there exists a unique morphism `case(f,g): A + B → X` that combines them case-by-case, satisfying `case(f,g) ∘ in₁ = f` and `case(f,g) ∘ in₂ = g`

This represents the "reversed arrows" dual concept to the direct product, demonstrating a good example of symmetry in category theory.

Visualized graphically, it appears as follows: (Compare with the direct product diagram to verify the reversed arrows):

![](./doc-images/coproduct.png)

Correspondences to programming concepts:

- Haskell's `Either a b` type
- `variant` types or other languages' `union` types with tags
- Branching logic using pattern matching

Now let's define the coproduct in CPL:

cpl> edit | left object coprod(a,b) with case is | in1: a -> coprod | in2: b -> coprod | end object; left object coprod(+,+) defined

cpl> show object coprod left object coprod(+,+)

• Natural transformations:

  in1: *a -> coprod(*a,*b) in2: *b -> coprod(*a,*b)

• Factorizer: f0: *b -> *a f1: *c -> *a

  case(f0,f1): coprod(*b,*c) -> *a

• Equations: (LEQ1): case(f0,f1).in1=f0 (LEQ2): case(f0,f1).in2=f1 (LFEQ): coprod(f0,f1)=case(in1.f0,in2.f1) (LCEQ): g.in1=f0 & g.in2=f1 => g=case(f0,f1)

• Unconditioned: yes

• Productive: (no,no)

## Displaying Type Information

The `show` command can be used to display the types of morphisms (their domains and codomains).

cpl> show pair(pi2,eval) pair(pi2,eval) : prod(exp(*a,*b),*a) -> prod(*a,*b)

Here, `*a` and `*b` are variable representations of objects, and such morphisms actually denote families of functions with various types (domains and codomains). When these families satisfy certain conditions, they are called **natural transformations**, which correspond to **polymorphic functions** in typical functional programming languages.

In the above example, `pair(pi2,eval)` is an arrow that works for any objects `*a` and `*b`, and can be viewed as a natural transformation from the functor `F(*a,*b) = prod(exp(*a,*b),*a)` to the functor `G(*a,*b) = prod(*a,*b)`.


**

## Morphism Composition and Identity Morphisms

The `.` symbol appearing in the equations above refers to fundamental operations on morphisms, which we will now review.

### Morphism Composition

`.` represents **morphism composition**. Given morphisms `f: A → B` and `g: B → C`, the composed morphism `g.f: A → C` is the arrow that "first applies `f`, then applies `g`". This corresponds to the mathematical notation `g ∘ f` (the Unicode symbol `∘` is also usable in CPL).

For example, we can represent natural numbers by composing the successor function `s: nat → nat` with the zero `0: 1 → nat`:

cpl> show s.0 s.0 : 1 -> nat cpl> show s.s.s.0 s.s.s.0 : 1 -> nat

`s.s.s.0` represents the "arrow obtained by composing `s` (successor function) three times with `0`", which corresponds to the natural number **3**. Similarly, `s.s.0` represents **2**, and `s.0` represents **1**.

### Identity Morphisms

The **identity morphism** `I` is the "do-nothing" arrow, with `I: A → A` existing for any object `A`:

cpl> show I I : *a -> *a

An identity morphism satisfies `f.I = f` and `I.f = f`. While it may seem trivial at first glance, we frequently use it in conjunction with functors to "transform only one of the components while leaving the other unchanged":

cpl> show prod(s, I) prod(s,I) : prod(nat,*a) -> prod(nat,*a)

Here, `prod(s, I)` represents the arrow that "applies `s` to the first component of the product while leaving the second component unchanged."

## Naming Expressions

The `let` command allows us to assign names to morphisms, enabling subsequent reference by name. This enables us to construct complex morphisms step by step.

As our first example, let's define the natural number addition `add: prod(nat, nat) → nat`. This would be a function typically written as follows:

```haskell
add 0 y = y
add (x + 1) y = add x y + 1

In CPL, we express this using primitive recursion pr combined with currying curry. Let's break it down step by step.

1. Strategy: We want to use primitive recursion pr on the first argument, but pr(f0, f1): nat → X can only define unary morphisms. Therefore, we curry the second argument by encapsulating it within the function.

2. Curried addition add':

   • add': nat → exp(nat, nat) — An arrow that takes a natural number n and returns a "function that adds n"
   • This can be defined in the form of pr(f0, f1)

3. f0 = curry(pi2) (zero case):

   • add'(0) returns "the function that adds 0" = the identity function
   • pi2: prod(1, nat) → nat is an arrow that extracts the second component of a product, which here functions as "discarding the first component (the unique value of the terminal object) while returning the second argument unchanged"
   • curry(pi2): 1 → exp(nat, nat) serves as the base case for the zero case

4. f1 = curry(s.eval) (successor case):

   • add'(n+1) returns "a function that applies s to the result of add'(n)"
   • eval: prod(exp(nat,nat), nat) → nat represents function application

• s.eval: prod(exp(nat,nat), nat) → nat performs "function application followed by taking the successor"
  • curry(s.eval): exp(nat,nat) → exp(nat,nat) represents the recursive step

5. Uncurrying: Revert add' = pr(curry(pi2), curry(s.eval)) back to eval and prod:
   • prod(add', I): prod(nat, nat) → prod(exp(nat,nat), nat) — Applies add' to the first argument
   • eval.prod(add', I): prod(nat, nat) → nat — Applies the resulting function to the second argument

Putting it all together:

cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)
add : prod(nat,nat) -> nat  defined

In the let construct, we can also define arrows with parameters.

cpl> let uncurry(f) = eval . prod(f, I)
f: *a -> exp(*b,*c)
-----------------------------
uncurry(f): prod(*a,*b) -> *c

Computation

In CPL, computation is performed through simplification of arrow expressions using the simp command. Let's simplify an arrow using our previously defined addition function add.

  cpl> simp add.pair(s.s.0, s.0)
  s.s.s.0
    : 1 -> nat

The result s.s.s.0 represents applying the successor function s three times, corresponding to the natural number 3. This demonstrates the calculation 2 + 1 = 3.

Similar to addition, let's define and compute multiplication and factorial.

Multiplication mult: prod(nat, nat) → nat can be defined using the same pattern as addition (currying + primitive recursion + uncurrying):

cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)
mult : prod(nat,nat) -> nat

The differences from add lie only in the zero case and the recursive step:

• Zero case curry(0.!) — 0 × y = 0 (0.! is an arrow that returns zero regardless of input)
• Successor case curry(add.pair(eval, pi2)) — (n+1) × y = n × y + y (adds the recursive result eval to y itself pi2)

Factorial fact: nat → nat uses a slightly different approach. It carries the state of prod(nat, nat) (a pair of accumulator and counter) using pr:

cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2)) fact : nat -> nat defined

• Initial value pair(s.0, 0) — (1, 0), i.e. "0! = 1, counter = 0"
• Recursive step pair(mult.pair(s.pi2, pi1), s.pi2) — computes (acc, k) to ((k+1) × acc, k+1)
• Final result pi1 extracts the accumulator value (the factorial result)

Let's compute it:

cpl> simp fact.s.s.s.s.0 s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.0 : 1 -> nat

Since s has been applied 24 times, we obtain the correct result 4! = 24.

List Type

Next, we'll define a list type—a data structure that's very similar to natural numbers but slightly more complex.

Lists, like natural numbers, have an inductive structure, but they differ in that their element type is parameterized:

• Empty list nil: 1 → list(a)

• Element prepend cons: a × list(a) → list(a) (adds an element to the front)

• Convolution prl(z,f): list(a) → b for recursively processing lists

Visualized graphically:

This represents a classic example of an inductive data type that describes finite structures.

Correspondence with programming:

• Haskell's [a] type (lists)
• Convolution using foldr

Now let's define lists in CPL:

cpl> edit | left object list(p) with prl is | nil: 1 -> list | cons: prod(p,list) -> list | end object; left object list(+) defined

cpl> show function list f0: *a -> *b

list(f0): list(*a) -> list(*b) cpl> show object list left object list(+)

• natural transformations: nil: 1 -> list(*a) cons: prod(*a,list(*a)) -> list(*a)

• factorizer: f0: 1 -> *a f1: prod(*b,*a) -> *a

  prl(f0,f1): list(*b) -> *a

• equations: (LEQ1): prl(f0,f1).nil=f0 (LEQ2): prl(f0,f1).cons=f1.prod(I,prl(f0,f1))

  (LFEQ): list(f0)=prl(nil,cons.prod(f0,I)) (LCEQ): g.nil=f0 & g.cons=f1.prod(I,g) => g=prl(f0,f1)

• unconditioned: no

• productive: (no)

The list is also a parameterized object and a functor, just like other objects. Let's examine its action on list morphisms. In functional programming, this action of a list functor on morphisms is often referred to as `map`.

cpl> show function list
f0: *a -> *b
------------------------------
list(f0): list(*a) -> list(*b)

Next, let's express some familiar functions using the list type.

Concatenation (append):

cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)
append : prod(list(*a),list(*a)) -> list(*a)  defined

Reversal (reverse):

cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))
reverse : list(*a) -> list(*a)  defined

head / tail:

cpl> let hd = prl(in2, in1.pi1)

hd : list(*a) -> coprod(*a,1) defined cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil))) tl : list(*a) -> coprod(list(*a),1) defined

We've chosen `hd` / `tl` here because we'll later need to use these names when working with infinite lists. In CPL, since only total functions exist and no partial functions are allowed, the codomain is a disjoint union with `1` (equivalent to the `Maybe` or `Option` types in other languages).

For convenience, we've also defined versions that lift the domain to the disjoint union with `1`, allowing us to recursively apply `head` / `tail` to the results of these operations.

cpl> let hdp=case(hd,in2) hdp : coprod(list(*a),1) -> coprod(*a,1) defined cpl> let tlp = case(tl, in2) tlp : coprod(list(*a),1) -> coprod(list(*a),1) defined

Sequential numbers `[n-1, n-2, ..., 1, 0]`:

cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons)) seq : nat -> list(nat) defined

Now, let's perform some computations.

Some calculations require `simp full` instead of just `simp` to proceed with reduction.

cpl> simp seq.s.s.s.0 cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil) : 1 -> list(nat) cpl> simp full seq.s.s.s.0 cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil))) : 1 -> list(nat)

While `simp` alone stops at an intermediate form, `simp full` completes the full reduction. The result `cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))` represents list notation in CPL. In other languages, this corresponds to the list `[2, 1, 0]`:

| CPL Representation | Meaning |
|---|---|
| `nil` | Empty list `[]` |
| `cons.pair(x, xs)` | Prepend `x`: `x : xs` |
| `cons.pair(s.s.0, cons.pair(s.0, cons.pair(0, nil)))` | `[2, 1, 0]` |

Let's examine the results of computing with other functions as well:

cpl> simp hdp.tl.seq.s.s.s.0 in1.s.0 : 1 -> coprod(nat,*a)

Since `seq.s.s.s.0` equals `[2, 1, 0]`, applying `tl` to remove the head yields `[1, 0]`, and then applying `hdp` to get the head results in `in1.s.0` (which equals `Just 1`).

cpl> simp full append.pair(seq.s.s.0, seq.s.s.s.0) cons.pair(s.0,cons.pair(0,cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil))))) : 1 -> list(nat) cpl> simp full reverse.it cons.pair(0,cons.pair(s.0,cons.pair(s.s.0,cons.pair(0,cons.pair(s.0,nil.!))))) : 1 -> list(nat)

`append.pair(seq.s.s.0, seq.s.s.s.0)` concatenates `[1, 0]` and `[2, 1, 0]` to form `[1, 0, 2, 1, 0]`, while `reverse.it` reverses this to produce `[0, 1, 2, 0, 1]`.

In the final example `simp full reverse.it`, we use `it` to reference the result of the previous computation (`append.pair(seq.s.s.0, seq.s.s.s.0)`). `it` is a useful feature that automatically stores the result of the immediately preceding `simp` command.

### Differences Between `simp` and `simp full`

CPL provides two reduction commands:

- **`simp`**: Performs basic reduction. Fast but may stop prematurely
- **`simp full`**: Performs more thorough reduction. Use when a completely reduced form is required


## Infinite Lists

In addition to finite data types like natural numbers and lists, we can also define data types for **infinite lists**.

Unlike finite lists, infinite lists are defined as a `right object`. This is an example of a **coinductive data type**:

- `head: inflist(a) → a` (extracts the head element)
- `tail: inflist(a) → inflist(a)` (obtains the remaining infinite list)
- `fold(h,t): x → inflist(a)` allows unfolding the infinite list (note that while named `fold`, in modern functional programming conventions this would more appropriately be called `unfold`)

While finite lists operate by "building up and then consuming," infinite lists have the contrasting structure of "unfolding from state."

Visualized graphically:

![](./doc-images/inflist.png)

Corresponding to programming concepts:

- Haskell's lazy evaluation-based infinite lists

- Streams and iterators
- Generation via `unfold`

Now let's define an infinite list in CPL.

cpl> edit | right object inflist(a) with fold is | head: inflist -> a | tail: inflist -> inflist | end object; right object inflist(+) defined

cpl> show object inflist right object inflist(+)

• natural transformations: head: inflist(*a) -> *a tail: inflist(*a) -> inflist(*a)

• factorizer: f0: *a -> *b f1: *a -> *a

  fold(f0,f1): *a -> inflist(*b)
• equations: (REQ1): head.fold(f0,f1)=f0 (REQ2): tail.fold(f0,f1)=fold(f0,f1).f1 (RFEQ): inflist(f0)=fold(f0.head,tail) (RCEQ): head.g=f0 & tail.g=g.f1 => g=fold(f0,f1)
• unconditioned: no
• productive: (no)

Now, let's define and compute with arrows using infinite lists.

First, we create an ascending sequence 0, 1, 2, 3, ...:

cpl> let incseq=fold(I,s).0 incseq : 1 -> inflist(nat) defined

`fold(I,s)` represents the unfolding rule that "outputs the current state as the `head` (`I`), then applies `s` to the state to proceed." Starting from the initial state `0`, this produces the infinite sequence 0, 1, 2, 3, ...

cpl> simp head.incseq 0 : 1 -> nat cpl> simp head.tail.tail.tail.incseq s.s.s.0 : 1 -> nat

We can extract the first element 0 using `head`, and the fourth element 3 using `head.tail.tail.tail`.

Next, we define the `alt` function that alternates between two infinite lists:

cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1)) alt : prod(inflist(*a),inflist(*a)) -> inflist(*a) defined

`alt` uses the product `prod(inflist, inflist)` as its state, with `head.pi1` outputting the head of the first list, and `pair(pi2, tail.pi1)` swapping the roles of the two lists (outputting the second list first, followed by the first list's tail).

cpl> let infseq=fold(I,I).0 infseq : 1 -> inflist(nat) defined cpl> simp head.tail.tail.alt.pair(incseq, infseq) s.0 : 1 -> nat

`infseq` is a constant sequence 0, 0, 0, ... The expression `alt.pair(incseq, infseq)` produces an alternating sequence 0, 0, 1, 0, 2, 0, 3, ... Therefore, the third element (index 2 starting from 0) is `s.0` (= 1).


## Category-Theoretic Background: left and right

When defining data types in CPL, there are two types of declarations: `left object` and `right object`. This reflects the important concept of **duality** in category theory.

### right object (terminal structure)

A `right object` is a structure based on **limits** in category theory. Limits are characterized by their property of being "defined by **incoming** morphisms from other objects."

- **Key characteristic**: Morphisms from other objects to this one (incoming morphisms) are crucial
- **Role in factorization**: Creates new morphisms by **combining** multiple morphisms
- **Examples in CPL**:
  - Terminal object `1`: The unique morphism `!` from any object to `1`
  - Product `prod(a,b)`: Creates morphism `pair(f,g): x -> prod(a,b)` from two morphisms `f: x -> a` and `g: x -> b`
  - Exponent object `exp(a,b)`: Creates morphisms through currying
  - Infinite list `inflist`: Expands infinite structures using `fold`

- **Correspondence to programming**: Coinductive types, types whose values are determined by behavior, lazy evaluation

### left object (initial structure)

A `left object` is a structure based on **colimits** in category theory. Colimits are characterized by their property of being "defined by **outgoing** morphisms from this object to others."

- **Key characteristic**: Morphisms from this object to other objects (outgoing morphisms) are crucial
- **Role in factorization**: **Breaks down and consumes** multiple cases
- **Examples in CPL**:
  - Natural numbers `nat`: Consumes (folds) natural numbers defined recursively by `pr`
  - Coproduct `coprod(a,b)`: Branches into two cases using `case`
  - List `list`: Folds recursive list structures using `prl`
- **Correspondence to programming**: Inductive types, types whose values are determined by structure, pattern matching


### Which one should be used?

General guidelines:

- **Finite data structures**: Use `left object` (constructed recursively)
- **Infinite data structures**: Use `right object` (expanded corecursively)

However, the symmetry between left and right in category theory is profound, and being able to experience this duality while using CPL is one of the language's key features.

### Correspondence to category theory

This left/right distinction corresponds to the following:

| CPL           | Category Theory       | Property                      |
|---------------|-----------------------|-------------------------------|
| right object  | Limit                 | Unifies "incoming" morphisms via universal morphisms |
| left object   | Colimit               | Unifies "outgoing" morphisms via couniversal morphisms |

In CPL, these concepts are treated symmetrically, allowing you to learn how category theory concepts are applied in practical programming.


## Summary

Through this tutorial, you've learned both the basic usage of CPL and fundamental category theory concepts.

### What you've learned

**CPL usage:**

- Command operations in the REPL (`edit`, `show`, `let`, `simp`, etc.)
- Defining data types (objects and functors) using `left object` and `right object`
- Defining and combining morphisms
- Performing computation through expression simplification

**Category theory concepts:**

- **Initial/terminal objects**: The concept of "a point where all paths converge"
- **Products/coproducts**: The dual operations of "combining/selecting multiple pieces of information"
- **Exponential objects**: Structures that treat functions as values (Cartesian closed categories)
- **Limits/colimits**: Foundational concepts behind `right object` and `left object`
- **Inductive/corecursive data types**: The contrast between finite and infinite structures
- **Duality**: The symmetrical relationship between left and right in category theory

### Unique features of CPL

In CPL, structures that would typically be "built-in" in other programming languages (such as numbers, lists, and functions) are all explicitly defined using category theory concepts. This results in:


- Direct connections between fundamental programming concepts and category theory theory
  - Hands-on experience with left/right duality through actual code
  - Understanding the mathematical structure underlying the type system

### Next steps

To deepen your understanding of CPL, we recommend trying the following:

1. **Exploring sample files**
   - The `samples/` directory contains various program examples
   - Try loading and executing samples using `load "samples/examples.cpl"`

2. **Writing more complex programs**
   - The Ackermann function (see `samples/ack.cpl`)
   - Other recursive functions and data structures

3. **Studying category theory**
   - Use the concepts learned in CPL as a starting point to read category theory textbooks
   - You'll gain deeper understanding of concepts like limits, colimits, and adjoints

4. **Exploring other category-theoretic programming**
   - Revisit the type systems of other functional languages like Haskell from a category theory perspective

   - Applications to dependent type theory and proof assistants (Coq, Agda, etc.)

## References

### Theoretical foundations of CPL

- **Tatsuya Hagino**, "A Categorical Programming Language", PhD Thesis, University of Edinburgh, 1987
  - The doctoral thesis that established the theoretical foundations of CPL
- **Tatsuya Hagino**, "Categorical Functional Programming Language", Computer Software Vol 7 No.1, 1992
  - A paper explaining CPL's overview in Japanese

### Introductions to category theory

- **Bartosz Milewski**, "Category Theory for Programmers"
  - An introductory category theory textbook for programmers. Available free online.
- **Steve Awodey**, "Category Theory" (Oxford Logic Guides)
  - A more mathematically rigorous textbook on category theory

### Online resources

- **CPL WebAssembly version**: <https://msakai.github.io/cpl/>
  - Allows you to try CPL directly in your browser
- **GitHub repository**: <https://github.com/msakai/cpl>
  - Contains source code, samples, and documentation

### Related concepts

- **Cartesian closed category**: A category with products and exponential objects. The categorical model of lambda calculus.

- **Adjunction**: The central concept underlying left and right objects.
  - **Universal property**: A key characteristic property in category theory that defines objects and morphisms.

---

We hope this tutorial serves as your first introduction to the world of CPL and category theory. Happy programming!

translated_TUTORIAL_jaをClaudeCodeで修正したもの.md

CPL Tutorial

Introduction

CPL (Categorical Programming Language) is a programming language designed based on concepts from category theory. In CPL, what are typically referred to as "data types" and "functions" in conventional programming languages are instead treated as "objects" and "morphisms" in category theory.

Set Theory	Functional Programming	CPL
Set	Data Type	Object
Mapping	Function	Morphism

Key Features of CPL

• Category-theoretic data type definition: All data types are defined using category theory concepts, specifically F,G-dialgebras—a generalization of adjunctions and F-(co)algebras
• Type safety: A robust type system grounded in category theory principles
• Functional programming: Only total functions are supported, ensuring pure computation without side effects
• Duality: Symmetric design using both left object (initial structure) and right object (terminal structure)

Prerequisite Knowledge

For optimal understanding, familiarity with the following:

• Basic programming concepts
• Experience with functional programming languages like Haskell (though not mandatory)

No prior knowledge of category theory is required. Through this tutorial, you'll learn both CPL usage and fundamental category theory concepts.

What You'll Learn from This Tutorial

• Basic CPL operations: REPL usage, data type definition, and function definition
• Fundamental category theory concepts: Terminal/initial objects, products/coproducts, exponential objects, etc.
• The distinction between left objects and right objects, and the concept of duality in category theory
• Practical programming examples: Natural numbers, lists, infinite lists, etc.

Table of Contents

• Introduction
• Basic Commands
• Initial Screen Display
• Defining Terminal Objects
• Defining Cartesian Products
• Defining Exponential Objects
• Defining the Natural Numbers Object
• Defining Coproducts
• Displaying Types
• Composing Arrows and Identity Arrows
• Assigning Names to Expressions
• Computation
• List Types
• Infinite Lists
• Category Theory Background: Left vs. Right
• Summary
• References

Basic Commands

The CPL REPL (Read-Eval-Print Loop) supports the following commands. This section provides only an overview, with detailed usage examples to be learned through practical application.

• edit: Enters multi-line editing mode. Use this for defining data types. End editing mode by pressing semicolon (;)
• show <expression>: Displays the type (domain and codomain) of an arrow (function)
• show object <functor>: Displays detailed information about an object (data type)
• show function <function>: Displays the type of a factorizer (higher-order function) or user-defined function
• let <name> = <expression>: Defines an arrow by assigning it a name
• let <name>(<arguments>) = <expression>: Defines an arrow with parameters
• simp <expression>: Simplifies (computes) the given expression
• simp full <expression>: Fully simplifies the expression (use when simp alone cannot complete simplification)
• it: Refers to the result from the previous computation
• load <filename>: Loads definitions from a file
• help: Displays help information
• exit: Exits the CPL environment

Initial Screen

Upon startup, the interface appears as follows:

Categorical Programming Language (Haskell version)
version 0.1.0

Type help for help

cpl> 

Defining the Terminal Object

CPL has no built-in data types, and all data types must be explicitly defined.

Since every operation requires the terminal object—corresponding to the unit type in other functional programming languages—we begin by defining this fundamental concept.

In category theory, a terminal object 1 is defined as "an object such that for every object X, there is exactly one arrow from X to 1." It serves as an "endpoint" representing an object with no information (or containing only one value). The single arrow is written as !.

Visually, this corresponds to the following situation:

Correspondences to programming concepts:

• Haskell's () type (unit type)
• void or unit types in other languages
• The concept of "a type containing exactly one value"

Now, let's define the terminal object in CPL. Using the edit command, enter multi-line editing mode, input your data type definition, and exit multi-line editing mode by pressing semicolon ;.

cpl> edit
| right object 1 with !
| end object;
right object 1 defined

The output "right object 1 defined" confirms that the terminal object 1 has been successfully defined.

Detailed information about a defined object can be viewed using show object.

cpl> show object 1
right object 1
- natural transformations:
- factorizer:
    
    ----------
    !: *a -> 1
- equations:
    (RFEQ): 1=!
    (RCEQ): g=!
- unconditioned: yes
- productive: ()

When object 1 is defined, a special arrow ! is also defined from any object to the terminal object.

The show command can also be used to display the arrow's type (domain and codomain). Here, *a is a variable representing an object, so this represents an arrow from any object to the terminal object 1.

cpl> show !
!
    : *a -> 1

Defining the Product

Next, we'll define the product. In category theory, the product operation combines two objects into a single object.

In category theory, the product A × B (prod(a,b) in CPL) is defined as "an object that preserves the information of both objects A and B." It satisfies the following properties:

• Existence of projection arrows π₁: A × B → A and π₂: A × B → B
• For any object X with arrows f: X → A and g: X → B to A and B respectively, there exists a unique arrow ⟨f,g⟩: X → A × B such that π₁ ∘ ⟨f,g⟩ = f and π₂ ∘ ⟨f,g⟩ = g (this is referred to as the universal property).

Visually represented as a diagram:

Correspondences with programming concepts:

• Haskell's (a, b) type (tuple)
• Pairs or structures in other languages
• The concept of "a type that combines two values"

Now, let's define the product in CPL:

cpl> edit
| right object prod(a,b) with pair is
|   pi1: prod -> a
|   pi2: prod -> b
| end object;
right object prod(+,+) defined

(Note in the definition of pi1 and pi2 that the object prod we're defining now is omitted from the arguments. This is intended as "we define prod(a,b) as the most universal x equipped with x -> a and x -> b," but think of it as reusing the name prod instead of introducing a new name x)

Unlike in the case of terminal objects, the product prod(a,b) is an object that takes parameters, and the resulting definition displays as prod(+,+). The + indicates covariance, and we can see that prod takes two arguments and is covariant with respect to both arguments. Use show object to display detailed information.

cpl> show object prod
right object prod(+,+)
- natural transformations:
    pi1: prod(*a,*b) -> *a
    pi2: prod(*a,*b) -> *b
- factorizer:
    f0: *a -> *b  f1: *a -> *c
    ------------------------------
    pair(f0,f1): *a -> prod(*b,*c)
- equations:
    (REQ1): pi1.pair(f0,f1)=f0
    (REQ2): pi2.pair(f0,f1)=f1
    (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
    (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
- unconditioned: yes
- productive: (yes,yes)

Unlike terminal objects, in the case of products, both projection arrows pi1 and pi2 are defined simultaneously (you can also check their types using the show command).

Additionally, a function (factorizer) pair is also defined, which constructs pair(f,g): a -> prod(b,c) from f: a -> b and g: a -> c. The arrow previously written as ⟨f,g⟩ in this context is now denoted as pair(f,g) in the defined product. The factorizer pair itself is not an arrow and cannot be displayed using show; instead, use show function to display its type.

cpl> show function pair
f0: *a -> *b  f1: *a -> *c
------------------------------
pair(f0,f1): *a -> prod(*b,*c)

Furthermore, while prod maps objects a and b to the object prod(a,b), it also maps arrows f: a -> c and g: b -> d to prod(a,b) -> prod(b,d). In category theory, a functor maps objects to objects and arrows between objects to arrows between mapped objects. Using show function prod, you can verify the type of prod's action on arrows.

cpl> show function prod
f0: *a -> *c  f1: *b -> *d
---------------------------------------
prod(f0,f1): prod(*a,*b) -> prod(*c,*d)

Furthermore, examining equations reveals that the following four equalities hold. Here, the . notation represents arrow composition, meaning g.f means "first apply f, then apply g" (corresponding to the mathematical notation g ∘ f).

• (REQ1): pi1.pair(f0,f1)=f0
  • (As stated earlier as a property of the product)
• (REQ2): pi2.pair(f0,f1)=f1
  • (Same as above)
• (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
  • (Definition of prod in terms of pair and pi1, pi2)
• (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
  • (If g satisfies the same conditions as pair(f0,f1), then g=pair(f0,f1), i.e., pair(f0,f1) is unique)

Definition of Exponential Object

Next, we define the exponential object, which is a structure for treating functions as values.

The exponential object Bᴬ (denoted as exp(a,b) in CPL) represents "the object that encodes all arrows from A to B." It possesses the following properties:

• An evaluation arrow eval: Bᴬ × A → B exists, allowing functions to be applied to values
  • (While we call it eval here, in functional programming contexts, apply would be a more natural name)
• For any arrow f: X × A → B, there exists a unique curried arrow curry(f): X → Bᴬ satisfying eval ∘ (curry(f) × I) = f
  • (Here, I: A → A represents the identity arrow, and × denotes the product arrow operation)

Visualized as a diagram, it appears as follows:

Why Is the Exponential Object Called a "Function Space"? Let's consider this concretely in the context of the category of sets.

• Bᴬ is the set of all functions from A to B — In the category of sets, the exponential object Bᴬ becomes the set {f | f: A → B} of functions itself.
• eval represents function application — eval(f, a) = f(a). In other words, it performs the operation of "taking a pair of a function f and its argument a, and returning the result of applying f to a."
• curry represents argument separation — For f: X × A → B, curry(f)(x) returns the function a ↦ f(x, a). In other words, currying transforms a two-argument function into a one-argument function that returns another function — this is precisely the operation of converting a function into a function that returns functions.
• Universality characterizes the function space — The commutativity of the diagram above — the property that "functions from X × A → B are in one-to-one correspondence with functions from X → Bᴬ" — is what uniquely characterizes Bᴬ as a function space. This correspondence is exactly the relationship between currying and function application in programming.

Correspondences with programming concepts:

• Haskell's a -> b type (function type)
• Currying and function application
• The concept of "treating functions as first-class values"

A category equipped with terminal objects, product objects, and exponential objects is called a Cartesian Closed Category, which forms the theoretical foundation for lambda calculus and functional programming.

Now, let's define the exponential object in CPL:

cpl> edit
| right object exp(a,b) with curry is
|   eval: prod(exp,a) -> b
| end object;
right object exp(-,+) defined

We can display detailed information using show object:

cpl> show object exp
right object exp(-,+)
- natural transformations:
    eval: prod(exp(*a,*b),*a) -> *b
- factorizer:
    f0: prod(*a,*b) -> *c
    ---------------------------
    curry(f0): *a -> exp(*b,*c)
- equations:
    (REQ1): eval.prod(curry(f0),I)=f0
    (RFEQ): exp(f0,f1)=curry(f1.eval.prod(I,f0))
    (RCEQ): eval.prod(g,I)=f0 => g=curry(f0)
- unconditioned: yes
- productive: (no,no)

We can see that eval for function application, curry for currying, and the conditions for an exponential object in category theory are all defined.

Using show function, let's examine how the functor exp operates on morphisms:

cpl> show function exp
f0: *c -> *a  f1: *b -> *d
------------------------------------
exp(f0,f1): exp(*a,*b) -> exp(*c,*d)

Note the directionality of the morphisms as arguments to exp, and how the parameters of exp change from domain to codomain:

• For f0 with function direction *c -> *a, the resulting parameter changes direction from *a to *c
• For f1 with function direction *b -> *d, the resulting parameter changes direction from *b to *d

This indicates that exp is a contravariant functor with respect to the first argument and a covariant functor with respect to the second argument. The notation exp(-,+) used during definition and in show object exp is a concise representation of this property.

Definition of the Natural Numbers Object

A natural numbers object is an inductively defined structure characterized by the number 0 and the successor function.

The natural numbers object ℕ is uniquely characterized by the following elements:

• Zero 0: 1 → ℕ (the initial value)
• Successor function s: ℕ → ℕ (also denoted as succ, the function that increments by 1)
• For any object X and morphisms z: 1 → X and f: X → X, there exists a unique morphism pr(z,f): ℕ → X defined recursively such that pr(z,f) ∘ 0 = z and pr(z,f) ∘ s = f ∘ pr(z,f)

This pr operation corresponds to mathematical induction and serves as the fundamental method for defining functions over the natural numbers.

Visualized graphically, this structure appears as follows:

Correspondences to programming concepts:

• The definition of natural numbers according to Peano's axioms

• Equivalent to Haskell data types such as:

  data Nat = Zero | Succ Nat

• Recursive computations (folding)

Now, let's define the natural numbers object in CPL:

cpl> edit
| left object nat with pr is
|   0: 1 -> nat
|   s: nat -> nat
| end object;
left object nat defined

To display the defined information, use show object nat:

cpl> show object nat
left object nat
- natural transformations:
    0: 1 -> nat
    s: nat -> nat
- factorizer:
    f0: 1 -> *a  f1: *a -> *a
    -------------------------
    pr(f0,f1): nat -> *a
- equations:
    (LEQ1): pr(f0,f1).0=f0
    (LEQ2): pr(f0,f1).s=f1.pr(f0,f1)
    (LFEQ): nat=pr(0,s)
    (LCEQ): g.0=f0 & g.s=f1.g => g=pr(f0,f1)
- unconditioned: no
- productive: ()

Here, 0 and s represent the zero and successor functions respectively, while pr corresponds to mathematical induction, along with the conditions they must satisfy.

Defining the Coproduct

The coproduct is a structure representing "either-or," serving as the dual concept to the direct product.

The coproduct A + B (denoted as coprod(a,b) in CPL) is an object that can hold one of two values, either from object A or B:

• It includes two injection morphisms in₁: A → A + B and in₂: B → A + B (which "inject" values into the coproduct)
• For any objects X and functions f: A → X and g: B → X, there exists a unique morphism case(f,g): A + B → X that combines them case-by-case, satisfying case(f,g) ∘ in₁ = f and case(f,g) ∘ in₂ = g

This represents the "reversed arrows" dual concept to the direct product, demonstrating a good example of symmetry in category theory.

Visualized graphically, it appears as follows: (Compare with the direct product diagram to verify the reversed arrows):

Correspondences to programming concepts:

• Haskell's Either a b type
• variant types or other languages' union types with tags
• Branching logic using pattern matching

Now let's define the coproduct in CPL:

cpl> edit
| left object coprod(a,b) with case is
|   in1: a -> coprod
|   in2: b -> coprod
| end object;
left object coprod(+,+) defined

cpl> show object coprod
left object coprod(+,+)
- natural transformations:
    in1: *a -> coprod(*a,*b)
    in2: *b -> coprod(*a,*b)
- factorizer:
    f0: *b -> *a  f1: *c -> *a
    --------------------------------
    case(f0,f1): coprod(*b,*c) -> *a
- equations:
    (LEQ1): case(f0,f1).in1=f0
    (LEQ2): case(f0,f1).in2=f1
    (LFEQ): coprod(f0,f1)=case(in1.f0,in2.f1)
    (LCEQ): g.in1=f0 & g.in2=f1 => g=case(f0,f1)
- unconditioned: yes
- productive: (no,no)

Displaying Type Information

The show command can be used to display the types of morphisms (their domains and codomains).

cpl> show pair(pi2,eval)
pair(pi2,eval)
    : prod(exp(*a,*b),*a) -> prod(*a,*b)

Here, *a and *b are variable representations of objects, and such morphisms actually denote families of functions with various types (domains and codomains). When these families satisfy certain conditions, they are called natural transformations, which correspond to polymorphic functions in typical functional programming languages.

In the above example, pair(pi2,eval) is an arrow that works for any objects *a and *b, and can be viewed as a natural transformation from the functor F(*a,*b) = prod(exp(*a,*b),*a) to the functor G(*a,*b) = prod(*a,*b).

Morphism Composition and Identity Morphisms

The . symbol appearing in the equations above refers to fundamental operations on morphisms, which we will now review.

Morphism Composition

. represents morphism composition. Given morphisms f: A → B and g: B → C, the composed morphism g.f: A → C is the arrow that "first applies f, then applies g". This corresponds to the mathematical notation g ∘ f (the Unicode symbol ∘ is also usable in CPL).

For example, we can represent natural numbers by composing the successor function s: nat → nat with the zero 0: 1 → nat:

cpl> show s.0
s.0
    : 1 -> nat
cpl> show s.s.s.0
s.s.s.0
    : 1 -> nat

s.s.s.0 represents the "arrow obtained by composing s (successor function) three times with 0", which corresponds to the natural number 3. Similarly, s.s.0 represents 2, and s.0 represents 1.

Identity Morphisms

The identity morphism I is the "do-nothing" arrow, with I: A → A existing for any object A:

cpl> show I
I
    : *a -> *a

An identity morphism satisfies f.I = f and I.f = f. While it may seem trivial at first glance, we frequently use it in conjunction with functors to "transform only one of the components while leaving the other unchanged":

cpl> show prod(s, I)
prod(s,I)
    : prod(nat,*a) -> prod(nat,*a)

Here, prod(s, I) represents the arrow that "applies s to the first component of the product while leaving the second component unchanged."

Naming Expressions

The let command allows us to assign names to morphisms, enabling subsequent reference by name. This enables us to construct complex morphisms step by step.

As our first example, let's define the natural number addition add: prod(nat, nat) → nat. This would be a function typically written as follows:

add 0 y = y
add (x + 1) y = add x y + 1

In CPL, we express this using primitive recursion pr combined with currying curry. Let's break it down step by step.

1. Strategy: We want to use primitive recursion pr on the first argument, but pr(f0, f1): nat → X can only define unary morphisms. Therefore, we curry the second argument by encapsulating it within the function.

2. Curried addition add':

   • add': nat → exp(nat, nat) — An arrow that takes a natural number n and returns a "function that adds n"
   • This can be defined in the form of pr(f0, f1)

3. f0 = curry(pi2) (zero case):

   • add'(0) returns "the function that adds 0" = the identity function
   • pi2: prod(1, nat) → nat is an arrow that extracts the second component of a product, which here functions as "discarding the first component (the unique value of the terminal object) while returning the second argument unchanged"
   • curry(pi2): 1 → exp(nat, nat) serves as the base case for the zero case

4. f1 = curry(s.eval) (successor case):

   • add'(n+1) returns "a function that applies s to the result of add'(n)"
   • eval: prod(exp(nat,nat), nat) → nat represents function application
   • s.eval: prod(exp(nat,nat), nat) → nat performs "function application followed by taking the successor"
   • curry(s.eval): exp(nat,nat) → exp(nat,nat) represents the recursive step

5. Uncurrying: Revert add' = pr(curry(pi2), curry(s.eval)) back to eval and prod:

   • prod(add', I): prod(nat, nat) → prod(exp(nat,nat), nat) — Applies add' to the first argument
   • eval.prod(add', I): prod(nat, nat) → nat — Applies the resulting function to the second argument

Putting it all together:

cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)
add : prod(nat,nat) -> nat  defined

In the let construct, we can also define arrows with parameters.

cpl> let uncurry(f) = eval . prod(f, I)
f: *a -> exp(*b,*c)
-----------------------------
uncurry(f): prod(*a,*b) -> *c

Computation

In CPL, computation is performed through simplification of arrow expressions using the simp command. Let's simplify an arrow using our previously defined addition function add.

cpl> simp add.pair(s.s.0, s.0)
s.s.s.0
    : 1 -> nat

The result s.s.s.0 represents applying the successor function s three times, corresponding to the natural number 3. This demonstrates the calculation 2 + 1 = 3.

Similar to addition, let's define and compute multiplication and factorial.

Multiplication mult: prod(nat, nat) → nat can be defined using the same pattern as addition (currying + primitive recursion + uncurrying):

cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)
mult : prod(nat,nat) -> nat

The differences from add lie only in the zero case and the recursive step:

• Zero case curry(0.!) — 0 × y = 0 (0.! is an arrow that returns zero regardless of input)
• Successor case curry(add.pair(eval, pi2)) — (n+1) × y = n × y + y (adds the recursive result eval to y itself pi2)

Factorial fact: nat → nat uses a slightly different approach. It carries the state of prod(nat, nat) (a pair of accumulator and counter) using pr:

cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))
fact : nat -> nat  defined

• Initial value pair(s.0, 0) — (1, 0), i.e. "0! = 1, counter = 0"
• Recursive step pair(mult.pair(s.pi2, pi1), s.pi2) — computes (acc, k) to ((k+1) × acc, k+1)
• Final result pi1 extracts the accumulator value (the factorial result)

Let's compute it:

cpl> simp fact.s.s.s.s.0
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.0
    : 1 -> nat

Since s has been applied 24 times, we obtain the correct result 4! = 24.

List Type

Next, we'll define a list type—a data structure that's very similar to natural numbers but slightly more complex.

Lists, like natural numbers, have an inductive structure, but they differ in that their element type is parameterized:

• Empty list nil: 1 → list(a)
• Element prepend cons: a × list(a) → list(a) (adds an element to the front)
• Fold prl(z,f): list(a) → b for recursively processing lists

Visualized graphically:

This represents a classic example of an inductive data type that describes finite structures.

Correspondence with programming:

• Haskell's [a] type (lists)
• Folding using foldr

Now let's define lists in CPL:

cpl> edit
| left object list(p) with prl is
|   nil: 1 -> list
|   cons: prod(p,list) -> list
| end object;
left object list(+) defined

cpl> show function list
f0: *a -> *b
------------------------------
list(f0): list(*a) -> list(*b)
cpl> show object list
left object list(+)
- natural transformations:
    nil: 1 -> list(*a)
    cons: prod(*a,list(*a)) -> list(*a)
- factorizer:
    f0: 1 -> *a  f1: prod(*b,*a) -> *a
    ----------------------------------
    prl(f0,f1): list(*b) -> *a
- equations:
    (LEQ1): prl(f0,f1).nil=f0
    (LEQ2): prl(f0,f1).cons=f1.prod(I,prl(f0,f1))
    (LFEQ): list(f0)=prl(nil,cons.prod(f0,I))
    (LCEQ): g.nil=f0 & g.cons=f1.prod(I,g) => g=prl(f0,f1)
- unconditioned: no
- productive: (no)

The list is also a parameterized object and a functor, just like other objects. Let's examine its action on list morphisms. In functional programming, this action of a list functor on morphisms is often referred to as map.

cpl> show function list
f0: *a -> *b
------------------------------
list(f0): list(*a) -> list(*b)

Next, let's express some familiar functions using the list type.

Concatenation (append):

cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)
append : prod(list(*a),list(*a)) -> list(*a)  defined

Reversal (reverse):

cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))
reverse : list(*a) -> list(*a)  defined

head / tail:

cpl> let hd = prl(in2, in1.pi1)
hd : list(*a) -> coprod(*a,1)  defined
cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))
tl : list(*a) -> coprod(list(*a),1)  defined

We've chosen hd / tl here because we'll later need to use these names when working with infinite lists. In CPL, since only total functions exist and no partial functions are allowed, the codomain is a disjoint union with 1 (equivalent to the Maybe or Option types in other languages).

For convenience, we've also defined versions that lift the domain to the disjoint union with 1, allowing us to recursively apply head / tail to the results of these operations.

cpl> let hdp=case(hd,in2)
hdp : coprod(list(*a),1) -> coprod(*a,1)  defined
cpl> let tlp = case(tl, in2)
tlp : coprod(list(*a),1) -> coprod(list(*a),1)  defined

Sequential numbers [n-1, n-2, ..., 1, 0]:

cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))
seq : nat -> list(nat)  defined

Now, let's perform some computations.

Some calculations require simp full instead of just simp to proceed with reduction.

cpl> simp seq.s.s.s.0
cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil)
    : 1 -> list(nat)
cpl> simp full seq.s.s.s.0
cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))
    : 1 -> list(nat)

While simp alone stops at an intermediate form, simp full completes the full reduction. The result cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil))) represents list notation in CPL. In other languages, this corresponds to the list [2, 1, 0]:

CPL Representation	Meaning
nil	Empty list []
cons.pair(x, xs)	Prepend x: x : xs
cons.pair(s.s.0, cons.pair(s.0, cons.pair(0, nil)))	[2, 1, 0]

Let's examine the results of computing with other functions as well:

cpl> simp hdp.tl.seq.s.s.s.0
in1.s.0
    : 1 -> coprod(nat,*a)

Since seq.s.s.s.0 equals [2, 1, 0], applying tl to remove the head yields [1, 0], and then applying hdp to get the head results in in1.s.0 (which equals Just 1).

cpl> simp full append.pair(seq.s.s.0, seq.s.s.s.0)
cons.pair(s.0,cons.pair(0,cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))))
    : 1 -> list(nat)
cpl> simp full reverse.it
cons.pair(0,cons.pair(s.0,cons.pair(s.s.0,cons.pair(0,cons.pair(s.0,nil.!)))))
    : 1 -> list(nat)

append.pair(seq.s.s.0, seq.s.s.s.0) concatenates [1, 0] and [2, 1, 0] to form [1, 0, 2, 1, 0], while reverse.it reverses this to produce [0, 1, 2, 0, 1].

In the final example simp full reverse.it, we use it to reference the result of the previous computation (append.pair(seq.s.s.0, seq.s.s.s.0)). it is a useful feature that automatically stores the result of the immediately preceding simp command.

Differences Between simp and simp full

CPL provides two reduction commands:

• simp: Performs basic reduction. Fast but may stop prematurely
• simp full: Performs more thorough reduction. Use when a completely reduced form is required

Infinite Lists

In addition to finite data types like natural numbers and lists, we can also define data types for infinite lists.

Unlike finite lists, infinite lists are defined as a right object. This is an example of a coinductive data type:

• head: inflist(a) → a (extracts the head element)
• tail: inflist(a) → inflist(a) (obtains the remaining infinite list)
• fold(h,t): x → inflist(a) allows unfolding the infinite list (note that while named fold, in modern functional programming conventions this would more appropriately be called unfold)

While finite lists operate by "building up and then consuming," infinite lists have the contrasting structure of "unfolding from state."

Visualized graphically:

Corresponding to programming concepts:

• Haskell's lazy evaluation-based infinite lists
• Streams and iterators
• Generation via unfold

Now let's define an infinite list in CPL.

cpl> edit
| right object inflist(a) with fold is
|   head: inflist -> a
|   tail: inflist -> inflist
| end object;
right object inflist(+) defined

cpl> show object inflist
right object inflist(+)
- natural transformations:
    head: inflist(*a) -> *a
    tail: inflist(*a) -> inflist(*a)
- factorizer:
    f0: *a -> *b  f1: *a -> *a
    ------------------------------
    fold(f0,f1): *a -> inflist(*b)
- equations:
    (REQ1): head.fold(f0,f1)=f0
    (REQ2): tail.fold(f0,f1)=fold(f0,f1).f1
    (RFEQ): inflist(f0)=fold(f0.head,tail)
    (RCEQ): head.g=f0 & tail.g=g.f1 => g=fold(f0,f1)
- unconditioned: no
- productive: (no)

Now, let's define and compute with arrows using infinite lists.

First, we create an ascending sequence 0, 1, 2, 3, ...:

cpl> let incseq=fold(I,s).0
incseq : 1 -> inflist(nat)  defined

fold(I,s) represents the unfolding rule that "outputs the current state as the head (I), then applies s to the state to proceed." Starting from the initial state 0, this produces the infinite sequence 0, 1, 2, 3, ...

cpl> simp head.incseq
0
    : 1 -> nat
cpl> simp head.tail.tail.tail.incseq
s.s.s.0
    : 1 -> nat

We can extract the first element 0 using head, and the fourth element 3 using head.tail.tail.tail.

Next, we define the alt function that alternates between two infinite lists:

cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1))
alt : prod(inflist(*a),inflist(*a)) -> inflist(*a)  defined

alt uses the product prod(inflist, inflist) as its state, with head.pi1 outputting the head of the first list, and pair(pi2, tail.pi1) swapping the roles of the two lists (outputting the second list first, followed by the first list's tail).

cpl> let infseq=fold(I,I).0
infseq : 1 -> inflist(nat)  defined
cpl> simp head.tail.tail.alt.pair(incseq, infseq)
s.0
    : 1 -> nat

infseq is a constant sequence 0, 0, 0, ... The expression alt.pair(incseq, infseq) produces an alternating sequence 0, 0, 1, 0, 2, 0, 3, ... Therefore, the third element (index 2 starting from 0) is s.0 (= 1).

Category-Theoretic Background: left and right

When defining data types in CPL, there are two types of declarations: left object and right object. This reflects the important concept of duality in category theory.

right object (terminal structure)

A right object is a structure based on limits in category theory. Limits are characterized by their property of being "defined by incoming morphisms from other objects."

• Key characteristic: Morphisms from other objects to this one (incoming morphisms) are crucial
• Role in factorization: Creates new morphisms by combining multiple morphisms
• Examples in CPL:
  • Terminal object 1: The unique morphism ! from any object to 1
  • Product prod(a,b): Creates morphism pair(f,g): x -> prod(a,b) from two morphisms f: x -> a and g: x -> b
  • Exponent object exp(a,b): Creates morphisms through currying
  • Infinite list inflist: Expands infinite structures using fold
• Correspondence to programming: Coinductive types, types whose values are determined by behavior, lazy evaluation

left object (initial structure)

A left object is a structure based on colimits in category theory. Colimits are characterized by their property of being "defined by outgoing morphisms from this object to others."

• Key characteristic: Morphisms from this object to other objects (outgoing morphisms) are crucial
• Role in factorization: Breaks down and consumes multiple cases
• Examples in CPL:
  • Natural numbers nat: Consumes (folds) natural numbers defined recursively by pr
  • Coproduct coprod(a,b): Branches into two cases using case
  • List list: Folds recursive list structures using prl
• Correspondence to programming: Inductive types, types whose values are determined by structure, pattern matching

Which one should be used?

General guidelines:

• Finite data structures: Use left object (constructed recursively)
• Infinite data structures: Use right object (expanded corecursively)

However, the symmetry between left and right in category theory is profound, and being able to experience this duality while using CPL is one of the language's key features.

Correspondence to category theory

This left/right distinction corresponds to the following:

CPL	Category Theory	Property
right object	Limit	Unifies "incoming" morphisms via universal morphisms
left object	Colimit	Unifies "outgoing" morphisms via couniversal morphisms

In CPL, these concepts are treated symmetrically, allowing you to learn how category theory concepts are applied in practical programming.

Summary

Through this tutorial, you've learned both the basic usage of CPL and fundamental category theory concepts.

What you've learned

CPL usage:

• Command operations in the REPL (edit, show, let, simp, etc.)
• Defining data types (objects and functors) using left object and right object
• Defining and combining morphisms
• Performing computation through expression simplification

Category theory concepts:

• Terminal/initial objects: The concept of "a point where all paths converge"
• Products/coproducts: The dual operations of "combining/selecting multiple pieces of information"
• Exponential objects: Structures that treat functions as values (Cartesian closed categories)
• Limits/colimits: Foundational concepts behind right object and left object
• Inductive/coinductive data types: The contrast between finite and infinite structures
• Duality: The symmetrical relationship between left and right in category theory

Unique features of CPL

In CPL, structures that would typically be "built-in" in other programming languages (such as numbers, lists, and functions) are all explicitly defined using category theory concepts. This results in:

• Direct connections between fundamental programming concepts and category theory
• Hands-on experience with left/right duality through actual code
• Understanding the mathematical structure underlying the type system

Next steps

To deepen your understanding of CPL, we recommend trying the following:

1. Exploring sample files

   • The samples/ directory contains various program examples
   • Try loading and executing samples using load "samples/examples.cpl"

2. Writing more complex programs

   • The Ackermann function (see samples/ack.cpl)
   • Other recursive functions and data structures

3. Studying category theory

   • Use the concepts learned in CPL as a starting point to read category theory textbooks
   • You'll gain deeper understanding of concepts like limits, colimits, and adjoints

4. Exploring other category-theoretic programming

   • Revisit the type systems of other functional languages like Haskell from a category theory perspective
   • Applications to dependent type theory and proof assistants (Coq, Agda, etc.)

References

Theoretical foundations of CPL

• Tatsuya Hagino, "A Categorical Programming Language", PhD Thesis, University of Edinburgh, 1987
  • The doctoral thesis that established the theoretical foundations of CPL
• Tatsuya Hagino, "Categorical Functional Programming Language", Computer Software Vol 7 No.1, 1992
  • A paper explaining CPL's overview in Japanese

Introductions to category theory

• Bartosz Milewski, "Category Theory for Programmers"
  • An introductory category theory textbook for programmers. Available free online.
• Steve Awodey, "Category Theory" (Oxford Logic Guides)
  • A more mathematically rigorous textbook on category theory

Online resources

• CPL WebAssembly version: https://msakai.github.io/cpl/
  • Allows you to try CPL directly in your browser
• GitHub repository: https://github.com/msakai/cpl
  • Contains source code, samples, and documentation

Related concepts

• Cartesian closed category: A category with products and exponential objects. The categorical model of lambda calculus.
• Adjunction: The central concept underlying left and right objects.
• Universal property: A key characteristic property in category theory that defines objects and morphisms.

---

We hope this tutorial serves as your first introduction to the world of CPL and category theory. Happy programming!

TUTORIAL_ja.md

CPL チュートリアル

はじめに

CPL (Categorical Programming Language) は、圏論の概念に基づいて設計されたプログラミング言語です。CPLでは、通常のプログラミング言語で「データ型」や「関数」と呼ばれるものが、圏論における「対象」と「射」として扱われます。

集合論	関数型プログラミング	CPL
集合	データ型	対象
写像	関数	射

CPLの特徴

• 圏論的なデータ型定義: すべてのデータ型は、随伴 (adjunction) と F-(余)代数 (F-(co)algebra) を一般化した F,G-両代数 (F,G-dialgebra) という圏論の概念を用いて定義されます
• 型安全性: 圏論の理論に基づいた強力な型システム
• 関数型プログラミング: 全域関数のみを扱い、副作用のない純粋な計算を行います
• 双対性: left object (始対象的構造) と right object (終対象的構造) による対称的な設計

前提知識

このチュートリアルでは、以下の知識があると理解しやすいでしょう:

• プログラミングの基礎知識
• Haskellなどの関数型プログラミング言語に触れた経験（あれば望ましい）

圏論の知識は必要ありません。このチュートリアルを通じて、CPLの使い方とともに圏論の基本的な概念を学ぶことができます。

このチュートリアルで学べること

• CPLの基本的な使い方（REPLの操作、データ型の定義、関数の定義）
• 圏論の基本概念（終対象/始対象、積/余積、指数対象など）
• left object と right object の違いと、圏論における双対性
• 具体的なプログラミング例（自然数、リスト、無限リストなど）

目次

• はじめに
• 基本的なコマンド
• 初期画面
• 終対象の定義
• 直積の定義
• 指数対象の定義
• 自然数対象の定義
• 直和の定義
• 型の表示
• 射の合成と恒等射
• 式に名前を付ける
• 計算
• リスト型
• 無限リスト
• 圏論的背景: left と right
• まとめ
• 参考文献

基本的なコマンド

CPLのREPL (Read-Eval-Print Loop) では、以下のコマンドを使用します。このセクションでは概要のみを説明し、詳細は実際の使用例の中で学んでいきます。

• edit: 複数行編集モードに入ります。データ型の定義などに使用します。セミコロン (;) で編集モードを終了します
• show <式>: 射（関数）の型（定義域と余域）を表示します
• show object <関手>: 対象（データ型）の詳細情報を表示します
• show function <関数>: ファクトライザ（高階関数）やユーザー定義関数の型を表示します
• let <名前> = <式>: 射に名前を付けて定義します
• let <名前>(<引数>) = <式>: パラメータを持つ射を定義します
• simp <式>: 式を簡約（計算）します
• simp full <式>: 式を完全に簡約します（simpだけでは簡約が進まない場合に使用）
• it: 直前の計算結果を参照します
• load <ファイル名>: ファイルから定義を読み込みます
• help: ヘルプを表示します
• exit: CPLを終了します

初期画面

起動すると以下のような画面になります。

Categorical Programming Language (Haskell version)
version 0.1.0

Type help for help

cpl> 

終対象の定義

CPLには組み込みのデータ型がなく、全てのデータ型は明示的に定義する必要があります。

何をするにも、他の関数型言語におけるユニット型に相応する終対象 (terminal object) が必ず必要なため、まずはこれを定義します。

圏論において、終対象 1 とは「どの対象 X からも、ただ一つだけ射が存在する対象」のことです。これは「終点」のような役割を果たし、情報を持たない（あるいは唯一の値しか持たない）対象を表します。ただ一つだけ存在する射を ! と書きます。

図式で描くと以下のような状況です。

プログラミングとの対応:

• Haskellの () 型（ユニット型）
• 他の言語における void や unit 型
• 「値が一つしかない型」という概念

それでは、CPLで終対象を定義します。 edit コマンドを用いて、複数行編集モードに入り、データ型の定義を入力し、セミコロン ; で複数行編集モードを終了します。

cpl> edit
| right object 1 with !
| end object;
right object 1 defined

right object 1 defined と出力され、終対象 1 が定義できました。

定義された対象の詳細な情報は show object を用いて表示することができます。

cpl> show object 1
right object 1
- natural transformations:
- factorizer:
    
    ----------
    !: *a -> 1
- equations:
    (RFEQ): 1=!
    (RCEQ): g=!
- unconditioned: yes
- productive: ()

対象 1 が定義されると同時に任意の対象から終対象への特別な射 ! も定義されています。

show コマンドを使うことでも、射の型(定義域と余域)を表示することができます。 ここで *a は対象を表す変数で、したがってこれは任意の対象から終対象 1 への射を表しています。

cpl> show !
!
    : *a -> 1

直積の定義

続いて、 直積 (product) を定義します。直積は、二つの対象を組み合わせて一つの対象を作る操作です。

圏論において、直積 A × B (CPLでは prod(a,b)) は「二つの対象 A と B の情報を両方とも保持する対象」として定義されます。これは以下の性質を持ちます:

• 射影 π₁: A × B → A と π₂: A × B → B が存在する
• 任意の対象 X から A と B への射 f: X → A と g: X → B があれば、それらを組み合わせた唯一の射 ⟨f,g⟩: X → A × B が存在し、 π₁ ∘ ⟨f,g⟩ = f と π₂ ∘ ⟨f,g⟩ = g を満たす（これが普遍性と呼ばれる性質です）

図式として描くと以下のようになります：

プログラミングとの対応:

• Haskellの (a, b) 型（タプル）
• 他の言語におけるペアや構造体
• 「二つの値を組み合わせた型」という概念

それでは、CPLで直積を定義します：

cpl> edit
| right object prod(a,b) with pair is
|   pi1: prod -> a
|   pi2: prod -> b
| end object;
right object prod(+,+) defined

（ここで pi1, pi2 の定義域では、今定義しようとしている対象 prod については引数を省略して書くことになっていることに気をつけてください。これは「x -> a, x -> b を備えた x の中で最も普遍的なものを prod(a,b) と定義する」という意図ですが、x という名前を新たに導入することを避けて、prod という名前を再利用していると考えると良いでしょう）

終対象の場合と違って、直積は prod(a,b) はパラメータを取る対象になっており、定義結果では prod(+,+) と表示されます。 + は共変性を表し、 prod は2引数で、どちらの引数についても共変であることが分かります。 show object を用いて詳細を表示します。

cpl> show object prod
right object prod(+,+)
- natural transformations:
    pi1: prod(*a,*b) -> *a
    pi2: prod(*a,*b) -> *b
- factorizer:
    f0: *a -> *b  f1: *a -> *c
    ------------------------------
    pair(f0,f1): *a -> prod(*b,*c)
- equations:
    (REQ1): pi1.pair(f0,f1)=f0
    (REQ2): pi2.pair(f0,f1)=f1
    (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
    (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
- unconditioned: yes
- productive: (yes,yes)

終対象の場合と異なり、直積の場合には射影を表す二つの射 pi1, pi2 が同時に定義されています（show コマンドでも型を確認してみましょう）。

また、 f: a -> b と g: a -> c から pair(f,g): a -> prod(b,c) を作る関数 (ファクトライザ) pair も同時に定義されています。上で ⟨f,g⟩ と書かれていた射は今回入力した直積の定義では pair(f,g) と表記されます。 ファクトライザ pair 自体は射ではないので show で表示することは出来ず、 show function を使うことで型を表示できます。

cpl> show function pair
f0: *a -> *b  f1: *a -> *c
------------------------------
pair(f0,f1): *a -> prod(*b,*c)

また、prod は対象 a, b を対象 prod(a,b) に写すだけでなく、射 f: a -> c, g: b -> d を prod(a,b) -> prod(b,d) へと写します。圏論における 関手 (functor) は対象を対象に、対象の間の射を写された対象の間の射へと写します。 show function prod とすることで、 prod の射に対する作用の型を確認することができます。

cpl> show function prod
f0: *a -> *c  f1: *b -> *d
---------------------------------------
prod(f0,f1): prod(*a,*b) -> prod(*c,*d)

また、 equations を見ると、以下の4つの等式が成り立つことが分かります。なお、ここで使われている . は射の合成 (composition) を表す記法で、g.f は「まず f を適用し、次に g を適用する」という意味です（数学の記法 g ∘ f に対応します）。

• (REQ1): pi1.pair(f0,f1)=f0
  • (上で直積の満たす性質として述べたもの)
• (REQ2): pi2.pair(f0,f1)=f1
  • (〃)
• (RFEQ): prod(f0,f1)=pair(f0.pi1,f1.pi2)
  • (prod の pair と pi1, pi2 による定義)
• (RCEQ): pi1.g=f0 & pi2.g=f1 => g=pair(f0,f1)
  • (g が pair(f0,f1) と同じ条件を満たすのであれば g=pair(f0,f1) 、すなわち pair(f0,f1) は一意)

指数対象の定義

次に、関数を値として扱うための構造である 指数対象 (exponential object) を定義します。

指数対象 Bᴬ (CPLでは exp(a,b) と表記) は「A から B への射全体を表す対象」です。これは以下の性質を持ちます:

• 評価射 eval: Bᴬ × A → B が存在し、関数を値に適用できる
  • (ここでは eval という名前で呼んでいますが、関数型プログラミングの文脈では apply と呼ぶ方が自然でしょう)
• 任意の射 f: X × A → B に対して、カリー化された射 curry(f): X → Bᴬ が一意に存在し、 eval ∘ (curry(f) × I) = f を満たす
  • (ここで、 I: A → A は恒等射を、 × は直積の射への作用を表しています)

図式として描くと以下のようになります：

なぜ指数対象が「関数空間」なのか？ 集合の圏で具体的に考えてみましょう。

• Bᴬ は A から B への関数全体の集合 — 集合の圏では、指数対象 Bᴬ は {f | f: A → B} という関数の集合そのものになります
• eval は関数適用 — eval(f, a) = f(a) です。つまり「関数 f とその引数 a のペアを受け取り、適用結果を返す」という操作です
• curry は引数の分離 — f: X × A → B に対して、curry(f)(x) は a ↦ f(x, a) という関数を返します。つまり二引数関数を「関数を返す一引数関数」に変換する操作がカリー化です
• 普遍性が関数空間を特徴づける — 上の図式が可換であること、すなわち「X × A → B の関数」と「X → Bᴬ の関数」が一対一に対応するという性質こそが、Bᴬ を関数空間として特徴づけています。この対応が、プログラミングにおけるカリー化と関数適用の関係に他なりません

プログラミングとの対応:

• Haskellの a -> b 型（関数型）
• カリー化 (currying) と関数適用 (application)
• 「関数を第一級の値として扱う」という概念

終対象、直積、指数対象を備えた圏はカルテシアン閉圏 (Cartesian Closed Category) と呼ばれ、ラムダ計算や関数型プログラミングの理論的基礎となっています。

それでは、CPLで指数対象を定義します：

cpl> edit
| right object exp(a,b) with curry is
|   eval: prod(exp,a) -> b
| end object;
right object exp(-,+) defined

show object を使って詳細を表示してみます。

cpl> show object exp
right object exp(-,+)
- natural transformations:
    eval: prod(exp(*a,*b),*a) -> *b
- factorizer:
    f0: prod(*a,*b) -> *c
    ---------------------------
    curry(f0): *a -> exp(*b,*c)
- equations:
    (REQ1): eval.prod(curry(f0),I)=f0
    (RFEQ): exp(f0,f1)=curry(f1.eval.prod(I,f0))
    (RCEQ): eval.prod(g,I)=f0 => g=curry(f0)
- unconditioned: yes
- productive: (no,no)

関数適用を行う eval 、カリー化を行う curry 、圏論での指数対象の条件などが定義されていることが分かります。

show function を使って関手 exp の射に対する作用を確認してみましょう。

cpl> show function exp
f0: *c -> *a  f1: *b -> *d
------------------------------------
exp(f0,f1): exp(*a,*b) -> exp(*c,*d)

exp の引数となる射の向きと、exp のパラメータが始域から余域に変化する方向に注目してください。

• f0 は *c -> *a という関数の向きに対して、結果のパラメータは逆向きの *a から *c へ変化
• f1 は *b -> *d という関数の向きに対して、結果のパラメータは順方向の *b から *d に変化

しています。これは exp が第一引数について反変(contravariant)、第二引数について共変(covariant)な関手であることを意味しています。exp の定義時や show object exp で表示されていた exp(-,+) はこのことをコンパクトに表現した記法です。

自然数対象の定義

自然数対象 (natural numbers object) は、0と後続関数によって定義される帰納的な構造です。

自然数対象 ℕ は以下の要素によって特徴付けられます:

• ゼロ 0: 1 → ℕ（初期値）
• 後続関数 s: ℕ → ℕ（succ、+1する関数）
• 任意の対象 X と射 z: 1 → X および f: X → X に対して、帰納的に定義された唯一の射 pr(z,f): ℕ → X が存在し、 pr(z,f) ∘ 0 = z と pr(z,f) ∘ s = f ∘ pr(z,f) を満たす

この pr (primitive recursion、原始再帰) は数学的帰納法に対応し、自然数上の関数を定義する基本的な方法です。

これを図式として描くと以下のようになります。

プログラミングとの対応:

• ペアノの公理による自然数の定義

• Haskellの以下のようなデータ型に相当:

  data Nat = Zero | Succ Nat

• 再帰的な計算（畳み込み、fold）

それではCPLで自然数対象を定義しましょう。

cpl> edit
| left object nat with pr is
|   0: 1 -> nat
|   s: nat -> nat
| end object;
left object nat defined

show object nat とすることで、情報を表示してみましょう。

cpl> show object nat
left object nat
- natural transformations:
    0: 1 -> nat
    s: nat -> nat
- factorizer:
    f0: 1 -> *a  f1: *a -> *a
    -------------------------
    pr(f0,f1): nat -> *a
- equations:
    (LEQ1): pr(f0,f1).0=f0
    (LEQ2): pr(f0,f1).s=f1.pr(f0,f1)
    (LFEQ): nat=pr(0,s)
    (LCEQ): g.0=f0 & g.s=f1.g => g=pr(f0,f1)
- unconditioned: no
- productive: ()

ゼロと後者関数を表す 0 と s 、また数学的帰納法に対応する pr およびそれらが満たすべき条件が定義されています。

直和の定義

直和 (coproduct) は、「どちらか一方」を表す構造で、直積の双対概念です。

直和 A + B (CPLでは coprod(a,b)) は、二つの対象 A と B のどちらか一方の値を持つ対象です:

• 入射 in₁: A → A + B と in₂: B → A + B が存在する（値を直和に「注入」する）
• 任意の対象 X への射 f: A → X と g: B → X があれば、それらを場合分けで組み合わせた唯一の射 case(f,g): A + B → X が存在し、 case(f,g) ∘ in₁ = f と case(f,g) ∘ in₂ = g を満たす

これは直積の「矢印を逆にした」双対概念であり、圏論における対称性の良い例です。

図式で描くと以下のようになります（直積の図式と比較して、矢印が逆になっていることを確認してください）：

プログラミングとの対応:

• Haskellの Either a b 型
• 他の言語における variant 型や（タグ付きの） union 型
• パターンマッチングによる分岐処理

それではCPLで直和を定義しましょう。

cpl> edit
| left object coprod(a,b) with case is
|   in1: a -> coprod
|   in2: b -> coprod
| end object;
left object coprod(+,+) defined

cpl> show object coprod
left object coprod(+,+)
- natural transformations:
    in1: *a -> coprod(*a,*b)
    in2: *b -> coprod(*a,*b)
- factorizer:
    f0: *b -> *a  f1: *c -> *a
    --------------------------------
    case(f0,f1): coprod(*b,*c) -> *a
- equations:
    (LEQ1): case(f0,f1).in1=f0
    (LEQ2): case(f0,f1).in2=f1
    (LFEQ): coprod(f0,f1)=case(in1.f0,in2.f1)
    (LCEQ): g.in1=f0 & g.in2=f1 => g=case(f0,f1)
- unconditioned: yes
- productive: (no,no)

型の表示

show コマンドを使って射の型(定義域と余域)を表示することができます。

cpl> show pair(pi2,eval)
pair(pi2,eval)
    : prod(exp(*a,*b),*a) -> prod(*a,*b)

*a や *b は対象を表す変数であり、このような射は実際には様々な型(定義域と余域)の射の族を表しています。この族がある条件を満たすときに 自然変換 (natural transformation) と呼ばれ、これは一般的な関数型言語における 多相関数 (polymorphic function) に対応する概念です。

上の例では、pair(pi2,eval) は任意の対象 *a と *b に対して機能する射であり、F(*a,*b) = prod(exp(*a,*b),*a) という関手から G(*a,*b) = prod(*a,*b) という関手への自然変換と考えることができます。

射の合成と恒等射

ここまでの定義で . という記号が等式の中に登場していましたが、ここで改めて射の基本操作を確認しておきましょう。

射の合成

. は射の合成 (composition) を表します。射 f: A → B と g: B → C があるとき、合成射 g.f: A → C は「まず f を適用し、次に g を適用する」射です。数学の記法 g ∘ f に対応します（Unicode記号 ∘ もCPLでは使用可能です）。

例えば、後続関数 s: nat → nat とゼロ 0: 1 → nat を合成することで、自然数を表現できます:

cpl> show s.0
s.0
    : 1 -> nat
cpl> show s.s.s.0
s.s.s.0
    : 1 -> nat

s.s.s.0 は「0 (ゼロ) に s (後続関数) を3回合成した射」で、自然数の 3 を表します。同様に s.s.0 は 2、s.0 は 1 です。

恒等射

恒等射 (identity morphism) I は「何もしない射」で、任意の対象 A に対して I: A → A が存在します:

cpl> show I
I
    : *a -> *a

恒等射は f.I = f かつ I.f = f を満たします。一見役に立たないようですが、関手と組み合わせて「一方の成分だけを変換し、他方はそのまま残す」際に頻繁に使います:

cpl> show prod(s, I)
prod(s,I)
    : prod(nat,*a) -> prod(nat,*a)

ここで prod(s, I) は「直積の第一成分に s を適用し、第二成分はそのまま」という射です。

式に名前を付ける

let コマンドを使うことで射に名前を付け、後から名前で参照することができます。これにより、複雑な射を段階的に構築できます。

最初の例として、自然数の加算 add: prod(nat, nat) → nat を定義しましょう。通常の関数型言語では以下のように書ける関数です:

add 0 y = y
add (x + 1) y = add x y + 1

CPLでは、これを原始再帰 pr とカリー化 curry を組み合わせて表現します。順を追って考えてみましょう。

1. 方針: 第一引数について原始再帰 pr を使いたいが、pr(f0, f1): nat → X は一引数の射しか定義できない。そこでカリー化を使い、第二引数を関数の中に閉じ込める

2. カリー化された加算 add' を考える:

   • add': nat → exp(nat, nat) — 自然数 n を受け取り「n を加える関数」を返す射
   • これは pr(f0, f1) の形で定義できる

3. f0 = curry(pi2) (ゼロの場合):

   • add'(0) は「0を加える関数」= 恒等関数
   • pi2: prod(1, nat) → nat は直積の第二成分を取り出す射で、ここでは「第一成分（終対象の唯一の値）を捨てて第二引数をそのまま返す」射として機能する
   • curry(pi2): 1 → exp(nat, nat) がゼロの場合の基底

4. f1 = curry(s.eval) (後続の場合):

   • add'(n+1) は「add'(n) の結果に s を適用する関数」
   • eval: prod(exp(nat,nat), nat) → nat は関数適用
   • s.eval: prod(exp(nat,nat), nat) → nat は「関数適用してから後続を取る」
   • curry(s.eval): exp(nat,nat) → exp(nat,nat) が再帰ステップ

5. アンカリー化: add' = pr(curry(pi2), curry(s.eval)) を eval と prod で元に戻す

   • prod(add', I): prod(nat, nat) → prod(exp(nat,nat), nat) — 第一引数に add' を適用
   • eval.prod(add', I): prod(nat, nat) → nat — 得られた関数を第二引数に適用

以上をまとめると:

cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)
add : prod(nat,nat) -> nat  defined

let では、パラメータを持つ射の定義も行うことができます。

cpl> let uncurry(f) = eval . prod(f, I)
f: *a -> exp(*b,*c)
-----------------------------
uncurry(f): prod(*a,*b) -> *c

計算

CPLでは simp コマンドによって、射の式を簡約することで計算を行います。先ほど定義した加算の関数 add を使った射を簡約してみましょう。

cpl> simp add.pair(s.s.0, s.0)
s.s.s.0
    : 1 -> nat

この結果 s.s.s.0 は、後続関数 s を3回適用したもので、自然数の3を表しています。つまり、2 + 1 = 3 という計算が行われました。

加算と同様に、乗算と階乗も定義して計算してみましょう。

乗算 mult: prod(nat, nat) → nat は加算と同じパターン（カリー化 + 原始再帰 + アンカリー化）で定義できます:

cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)
mult : prod(nat,nat) -> nat

add との違いはゼロの場合と再帰ステップだけです:

• ゼロの場合 curry(0.!) — 0 × y = 0（0.! は「何を入れてもゼロ」を返す射）
• 後続の場合 curry(add.pair(eval, pi2)) — (n+1) × y = n × y + y（再帰結果 eval に y 自身 pi2 を加える）

階乗 fact: nat → nat は少し異なる方法を使います。pr で prod(nat, nat) の状態（累積値とカウンタのペア）を持ち運びます:

cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))
fact : nat -> nat  defined

• 初期値 pair(s.0, 0) — (1, 0) すなわち「0! = 1、カウンタ = 0」
• 再帰ステップ pair(mult.pair(s.pi2, pi1), s.pi2) — (acc, k) から ((k+1) × acc, k+1) を計算
• 最後に pi1 で累積値（階乗の結果）を取り出す

計算してみましょう:

cpl> simp fact.s.s.s.s.0
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.0
    : 1 -> nat

s が24回適用されているので、4! = 24 という正しい結果が得られています。

リスト型

次は自然数とほぼ同じですが、少しだけ複雑なデータ型であるリスト型を定義してみます。

リストは自然数と同様に帰納的な構造を持ちますが、要素の型をパラメータとして持つ点が異なります:

• 空リスト nil: 1 → list(a)
• 要素追加 cons: a × list(a) → list(a)（先頭に要素を追加）
• 畳み込み prl(z,f): list(a) → b により、リストを再帰的に処理

図式を描くと以下のようになります。

これは帰納的データ型の典型例で、有限の構造を表現します。

プログラミングとの対応:

• Haskellの [a] 型（リスト）
• foldr による畳み込み

それではCPLでリストを定義してみましょう。

cpl> edit
| left object list(p) with prl is
|   nil: 1 -> list
|   cons: prod(p,list) -> list
| end object;
left object list(+) defined

cpl> show function list
f0: *a -> *b
------------------------------
list(f0): list(*a) -> list(*b)
cpl> show object list
left object list(+)
- natural transformations:
    nil: 1 -> list(*a)
    cons: prod(*a,list(*a)) -> list(*a)
- factorizer:
    f0: 1 -> *a  f1: prod(*b,*a) -> *a
    ----------------------------------
    prl(f0,f1): list(*b) -> *a
- equations:
    (LEQ1): prl(f0,f1).nil=f0
    (LEQ2): prl(f0,f1).cons=f1.prod(I,prl(f0,f1))
    (LFEQ): list(f0)=prl(nil,cons.prod(f0,I))
    (LCEQ): g.nil=f0 & g.cons=f1.prod(I,g) => g=prl(f0,f1)
- unconditioned: no
- productive: (no)

リストも対象によってパラメータ化された対象、関手となっています。リストの射に対する作用について確認してみましょう。リスト関手の射に対する作用は関数型プログラミングではしばしば map と呼ばれています。

cpl> show function list
f0: *a -> *b
------------------------------
list(f0): list(*a) -> list(*b)

次にリスト型を用いたお馴染みの関数達を表現してみましょう。

連結（append）:

cpl> let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I)
append : prod(list(*a),list(*a)) -> list(*a)  defined

逆転（reverse）:

cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))
reverse : list(*a) -> list(*a)  defined

head / tail:

cpl> let hd = prl(in2, in1.pi1)
hd : list(*a) -> coprod(*a,1)  defined
cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))
tl : list(*a) -> coprod(list(*a),1)  defined

後で無限リストを使う際に head / tail という名前を使いたいので、ここでは hd / tl という名前を使っています。また、CPLでは全域関数しか存在せず部分関数は存在しないため、余域は1との直和（他の言語における Maybe 型や Option 型）になっています。

さらに、 head / tail の結果に再度 head / tail を適用するのに便利なように、定義域を 1 との直和に持ち上げたバージョンも定義しておきましょう。

cpl> let hdp=case(hd,in2)
hdp : coprod(list(*a),1) -> coprod(*a,1)  defined
cpl> let tlp = case(tl, in2)
tlp : coprod(list(*a),1) -> coprod(list(*a),1)  defined

連番 [n-1, n-2, ..., 1, 0]:

cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))
seq : nat -> list(nat)  defined

これらを利用して計算を行ってみます。

一部の計算では simp だけでは簡約が進まないため、 simp full を使う必要があります。

cpl> simp seq.s.s.s.0
cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil)
    : 1 -> list(nat)
cpl> simp full seq.s.s.s.0
cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))
    : 1 -> list(nat)

simp だけでは中間的な形で止まりますが、simp full で完全に簡約されます。結果の cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil))) は、CPLにおけるリストの表現です。これは他の言語で書けば [2, 1, 0] に対応します:

CPLの表現	意味
nil	空リスト []
cons.pair(x, xs)	x を先頭に追加 x : xs
cons.pair(s.s.0, cons.pair(s.0, cons.pair(0, nil)))	[2, 1, 0]

他の関数の計算結果も見てみましょう:

cpl> simp hdp.tl.seq.s.s.s.0
in1.s.0
    : 1 -> coprod(nat,*a)

seq.s.s.s.0 は [2, 1, 0] なので、tl で先頭を除いた [1, 0] に対し hdp で先頭を取ると in1.s.0 (= Just 1) になります。

cpl> simp full append.pair(seq.s.s.0, seq.s.s.s.0)
cons.pair(s.0,cons.pair(0,cons.pair(s.s.0,cons.pair(s.0,cons.pair(0,nil)))))
    : 1 -> list(nat)
cpl> simp full reverse.it
cons.pair(0,cons.pair(s.0,cons.pair(s.s.0,cons.pair(0,cons.pair(s.0,nil.!)))))
    : 1 -> list(nat)

append.pair(seq.s.s.0, seq.s.s.s.0) は [1, 0] と [2, 1, 0] の連結で [1, 0, 2, 1, 0] に、reverse.it はその逆転で [0, 1, 2, 0, 1] になります。

最後の例 simp full reverse.it では、it を使って直前の計算結果（append.pair(seq.s.s.0, seq.s.s.s.0) の結果）を参照しています。it は直前の simp コマンドの結果を自動的に保存する便利な機能です。

simp と simp full の違い

CPLには二つの簡約コマンドがあります:

• simp: 基本的な簡約を行います。高速ですが、簡約が途中で止まることがあります
• simp full: より徹底的に簡約を行います。完全に簡約された形が必要な場合に使用します

無限リスト

自然数やリストのような有限のデータ型だけでなく、無限リストのデータ型を定義することもできます。

無限リストは、有限リストとは異なり right object として定義されます。これは余帰納的データ型 (coinductive type) の例です:

• head: inflist(a) → a（先頭要素を取り出す）
• tail: inflist(a) → inflist(a)（残りの無限リストを得る）
• fold(h,t): x → inflist(a) により、無限リストを展開（fold という名前が使われていますが、現代の関数型プログラミングの慣習ではむしろ unfold と呼ばれます）

有限リストが「構築して消費する」のに対し、無限リストは「状態から展開していく」という対照的な構造を持ちます。

図式を描くと以下のようになります。

プログラミングとの対応:

• Haskellの遅延評価による無限リスト
• ストリームやイテレータ
• unfold による生成

それではCPLで無限リストを定義しましょう。

cpl> edit
| right object inflist(a) with fold is
|   head: inflist -> a
|   tail: inflist -> inflist
| end object;
right object inflist(+) defined

cpl> show object inflist
right object inflist(+)
- natural transformations:
    head: inflist(*a) -> *a
    tail: inflist(*a) -> inflist(*a)
- factorizer:
    f0: *a -> *b  f1: *a -> *a
    ------------------------------
    fold(f0,f1): *a -> inflist(*b)
- equations:
    (REQ1): head.fold(f0,f1)=f0
    (REQ2): tail.fold(f0,f1)=fold(f0,f1).f1
    (RFEQ): inflist(f0)=fold(f0.head,tail)
    (RCEQ): head.g=f0 & tail.g=g.f1 => g=fold(f0,f1)
- unconditioned: no
- productive: (no)

それでは、無限リストを用いた射の定義と計算をしてみましょう。

まず、0, 1, 2, 3, ... という増加列を作ります:

cpl> let incseq=fold(I,s).0
incseq : 1 -> inflist(nat)  defined

fold(I,s) は「現在の状態をそのまま head として出力し (I)、状態に s を適用して次へ進む」という展開規則です。初期状態 0 から始めると、0, 1, 2, 3, ... という無限列になります。

cpl> simp head.incseq
0
    : 1 -> nat
cpl> simp head.tail.tail.tail.incseq
s.s.s.0
    : 1 -> nat

head で先頭要素 0 を、head.tail.tail.tail で4番目の要素 3 を取り出せます。

次に、二つの無限リストを交互に組み合わせる alt を定義します:

cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1))
alt : prod(inflist(*a),inflist(*a)) -> inflist(*a)  defined

alt は直積 prod(inflist, inflist) を状態として、head.pi1 で第一リストの先頭を出力し、pair(pi2, tail.pi1) で二つのリストの役割を入れ替えます（第二を先に、第一のtailを後に）。

cpl> let infseq=fold(I,I).0
infseq : 1 -> inflist(nat)  defined
cpl> simp head.tail.tail.alt.pair(incseq, infseq)
s.0
    : 1 -> nat

infseq は 0, 0, 0, ... という定数列です。alt.pair(incseq, infseq) は 0, 0, 1, 0, 2, 0, 3, ... と交互に並べた列になるため、3番目の要素（0始まりで index 2）は s.0 (= 1) です。

圏論的背景: left と right

CPLでデータ型を定義する際、left object と right object という二種類の宣言方法があります。これは圏論における重要な概念である双対性 (duality) を反映しています。

right object（終対象的構造）

right object は圏論における極限 (limit) に基づいた構造です。極限は「他の対象から入ってくる射によって特徴付けられる」という性質を持ちます。

• 特徴: 他の対象からこの対象への射（入射）が重要
• ファクトライザの役割: 複数の射から新しい射を作り出す
• CPLでの例:
  • 終対象 1: 任意の対象から1への唯一の射!
  • 直積 prod(a,b): 二つの射f: x -> aとg: x -> bからpair(f,g): x -> prod(a,b)を作る
  • 指数対象 exp(a,b): カリー化により射を作る
  • 無限リスト inflist: foldにより無限の構造を展開する
• プログラミングとの対応: 余帰納的データ型（coinductive types）、振る舞いによって値が規定される型、遅延評価

left object（始対象的構造）

left object は圏論における余極限 (colimit) に基づいた構造です。余極限は「この対象から他の対象へ出ていく射によって特徴付けられる」という性質を持ちます。

• 特徴: この対象から他の対象への射（出射）が重要
• ファクトライザの役割: 複数のケースを分解・消費する
• CPLでの例:
  • 自然数 nat: prにより帰納的に定義された自然数を消費（畳み込み）
  • 直和 coprod(a,b): caseにより二つのケースを分岐処理
  • リスト list: prlにより帰納的なリスト構造を畳み込む
• プログラミングとの対応: 帰納的データ型（inductive types）、構造によって値が規定される型、パターンマッチング

どちらを使うべきか

一般的な指針:

• 有限のデータ構造: left object（帰納的に構築される）
• 無限のデータ構造: right object（余帰納的に展開される）

しかし、圏論における left と right の対称性は深遠で、CPLを使いながらこの双対性を体感できることがCPLの大きな特徴の一つです。

圏論との対応

この left/right の区別は、圏論における以下の概念と対応しています:

CPL	圏論	性質
right object	極限 (limit)	普遍射により「入射」を統一
left object	余極限 (colimit)	余普遍射により「出射」を統一

CPLでは、これらの概念が対称的に扱われ、圏論の理論が実際のプログラミングにどのように活用されるかを学ぶことができます。

まとめ

このチュートリアルを通じて、CPLの基本的な使い方と、圏論の基本概念を学びました。

学んだこと

CPLの使い方:

• REPLでのコマンド操作（edit, show, let, simpなど）
• データ型（対象・関手）の定義（left object と right object）
• 射の定義と組み合わせ
• 式の簡約による計算

圏論の概念:

• 終対象/始対象: 「すべての道が通じる点」という概念
• 積/余積: 「複数の情報を組み合わせる/選択する」という双対な操作
• 指数対象: 関数を値として扱う構造（カルテシアン閉圏）
• 極限/余極限: right object と left object の基礎となる概念
• 帰納的/余帰納的データ型: 有限と無限の構造の対比
• 双対性: 圏論における left と right の対称的な関係

CPLのユニークな特徴

CPLでは、他のプログラミング言語では「組み込み」として提供される構造（数値、リスト、関数など）を、すべて圏論の概念を用いて明示的に定義します。これにより:

• プログラミングの基本概念と圏論の理論が直接結びつく
• left/right の双対性を実際のコードで体験できる
• 型システムの背後にある数学的構造を理解できる

次のステップ

CPLをさらに深く学ぶために、以下を試してみてください:

1. サンプルファイルの探索

   • samples/ ディレクトリには様々なプログラム例があります
   • load "samples/examples.cpl" でサンプルを読み込んで実行してみましょう

2. より複雑なプログラムを書く

   • アッカーマン関数（samples/ack.cpl 参照）
   • 他の再帰的な関数やデータ構造

3. 圏論を学ぶ

   • CPLで学んだ概念を出発点に、圏論の教科書を読んでみましょう
   • 極限、余極限、随伴などの概念がより深く理解できるようになります

4. 他の圏論的プログラミング

   • Haskellなど他の関数型言語の型システムを圏論の観点から見直す
   • 依存型理論や証明支援系（Coq、Agdaなど）への応用

参考文献

CPLの理論的基礎

• Tatsuya Hagino, "A Categorical Programming Language", PhD Thesis, University of Edinburgh, 1987
  • CPLの理論的基礎を確立した博士論文
• Tatsuya Hagino, "Categorical Functional Programming Language", Computer Software Vol 7 No.1, 1992
  • CPLの概要を日本語で解説した論文

圏論の入門書

• Bartosz Milewski, "Category Theory for Programmers"
  • プログラマ向けの圏論入門。オンラインで無料公開
• Steve Awodey, "Category Theory" (Oxford Logic Guides)
  • 数学的により厳密な圏論の教科書

オンラインリソース

• CPL WebAssembly版: https://msakai.github.io/cpl/
  • ブラウザで直接CPLを試すことができます
• GitHub リポジトリ: https://github.com/msakai/cpl
  • ソースコード、サンプル、ドキュメント

関連する概念

• カルテシアン閉圏: 直積と指数対象を持つ圏。ラムダ計算の圏論的モデル
• 随伴 (Adjunction): left/right object の背後にある中心的な概念
• 普遍性 (Universal Property): 圏論における対象や射を特徴付ける重要な性質

---

このチュートリアルが、CPLと圏論の世界への第一歩となれば幸いです。楽しいプログラミングを!