packages feed

CPL 0.1.0 → 0.2.0

raw patch · 56 files changed

+4133/−248 lines, 56 filesdep +ghc-experimentaldep −readlinedep ~basebinary-added

Dependencies added: ghc-experimental

Dependencies removed: readline

Dependency ranges changed: base

Files

− CHANGELOG.markdown 
@@ -1,48 +0,0 @@-0.1.0 (2025-10-29)----------------------------------* Update Cabal-Version requirement from >=1.10 to 2.2-* Require `mtl` >=2.2.1 for `Control.Monad.Except`-* Fix compilation error on recent `mtl` package--0.0.9 (2018-02-16)----------------------------------* Use `Control.Monad.Except` instead of deprecated Control.Monad.Error--0.0.8 (2016-01-14)----------------------------------* "→" can be used instead of "->"-* GHC-7.10 support-* Add windows installer--0.0.7 (2014-08-13)----------------------------------* Clean up internals-* Enable `-fReadline` and `-fHaskeline` by default--0.0.6 (2009-10-26)----------------------------------Readline/Haskeline support.--0.0.4----------------------------------Function defintions are added.--Examples:--    > let uncurry(f) = eval . prod(f, I)-    uncurry(f) = eval.prod(f,I)-    f: *a -> exp(*b,*c)-    ------------------------------    uncurry(f): prod(*a,*b) -> *c--    > let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))-    primrec(f,g) = pi2.pr(pair(0,f),pair(s.pi1,g))-    f: 1 -> *a  g: prod(nat,*a) -> *a-    ----------------------------------    primrec(f,g): nat -> *a
+ CHANGELOG.md view
@@ -0,0 +1,76 @@+0.2.0 (2026-02-06)+-------------------------------++* Add `show function <name>` subcommand to display information of functions including functors, factorizers, and user-defined parameterized morphisms:+    ```+    cpl> show function exp  +    f0: *c -> *a  f1: *b -> *d+    ------------------------------------+    exp(f0,f1): exp(*a,*b) -> exp(*c,*d)+    cpl> show function curry+    f0: prod(*a,*b) -> *c+    ---------------------------+    curry(f0): *a -> exp(*b,*c)+    cpl> let uncurry(f) = eval . prod(f, I)+    cpl> show function uncurry+    f: *a -> exp(*b,*c)+    -----------------------------+    uncurry(f): prod(*a,*b) -> *c+    ```+* Add WebAssembly support for browser-based CPL interpreter (<https://msakai.github.io/cpl/>)+* Add tutorials both in English and Japanese+* Accept `id` as a synonym for `I` (identity morphism)+* Allow the omission of the `is` keyword in data type definitions+* Assume that files loaded via the `load` command use UTF-8 encoding+* Remove readline support (the `Readline` cabal flag and `USE_READLINE_PACKAGE` code path)+* Drop support for GHC <9.2 (base <4.16)+* Stop providing MSI installer++0.1.0 (2025-10-29)+-------------------------------++* Update Cabal-Version requirement from >=1.10 to 2.2+* Require `mtl` >=2.2.1 for `Control.Monad.Except`+* Fix compilation error on recent `mtl` package++0.0.9 (2018-02-16)+-------------------------------++* Use `Control.Monad.Except` instead of deprecated Control.Monad.Error++0.0.8 (2016-01-14)+-------------------------------++* "→" can be used instead of "->"+* GHC-7.10 support+* Add windows installer++0.0.7 (2014-08-13)+-------------------------------++* Clean up internals+* Enable `-fReadline` and `-fHaskeline` by default++0.0.6 (2009-10-26)+-------------------------------++Readline/Haskeline support.++0.0.4+-------------------------------++Function defintions are added.++Examples:++    > let uncurry(f) = eval . prod(f, I)+    uncurry(f) = eval.prod(f,I)+    f: *a -> exp(*b,*c)+    -----------------------------+    uncurry(f): prod(*a,*b) -> *c++    > let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g))+    primrec(f,g) = pi2.pr(pair(0,f),pair(s.pi1,g))+    f: 1 -> *a  g: prod(nat,*a) -> *a+    ---------------------------------+    primrec(f,g): nat -> *a
COPYING view
@@ -1,4 +1,4 @@-Copyright 2004-2008 Masahiro Sakai. All rights reserved.+Copyright 2004-2026 Masahiro Sakai. All rights reserved.  Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are
CPL.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 Name:		CPL-Version:	0.1.0+Version:	0.2.0 License:	BSD-3-Clause License-File:	COPYING Author:		Masahiro Sakai (masahiro.sakai@gmail.com)@@ -20,9 +20,16 @@    programs is the reduction of elements (i.e. special morphisms) to    their canonical form. Extra-Doc-Files:-   README.markdown,-   CHANGELOG.markdown+   README.md,+   CHANGELOG.md,+   TUTORIAL.md,+   TUTORIAL_ja.md,+   doc-images/*.png,+   images/*.png,+   web/README.md Extra-Source-Files:+   doc-images/*.tex,+   doc-images/Makefile,    samples/ack.cpl,    samples/automata.cdt,    samples/ccc.cdt,@@ -33,16 +40,28 @@    samples/rec.cdt,    samples/benchmark.cpl,    samples/ack_3_4.cpl,-   samples/function.cpl+   samples/function.cpl,+   scripts/build-wasm.sh,+   scripts/generate-favicons.sh,+   scripts/generate-samples-js.sh,+   web/cpl-terminal.js,+   web/index.html,+   web/tutorial_header.txt,+   web/tutorial_ja_header.txt,+   web/tutorial.css,+   web/favicon_header.html,+   web/favicon.ico,+   web/favicon-16x16.png,+   web/favicon-32x32.png,+   web/apple-touch-icon.png,+   web/icon-192x192.png,+   web/icon-512x512.png,+   web/manifest.json Build-Type: Simple  source-repository head   type:     git-  location: git://github.com/msakai/cpl.git--Flag Readline-  Description: Use Readline-  Default: True+  location: https://github.com/msakai/cpl.git  Flag Haskeline   Description: Use Haskeline@@ -53,17 +72,29 @@   Default: False   Manual: True +Flag Web+  Description: Build for browser environment with WebAssembly + JavaScript FFI+  Default: False+  Manual: True+ Executable cpl   Main-is: Main.hs   HS-Source-Dirs: src   Other-Modules: AExp CDT CDTParser CPLSystem Exp ExpParser FE Funct ParserUtils Simp Statement Subst Type Typing Variance Paths_CPL   Autogen-Modules: Paths_CPL-  Build-Depends: base >=4 && <5, mtl >=2.2.1, containers, array, parsec+  Build-Depends: base >=4.16 && <5, mtl >=2.2.1, containers, array, parsec   Default-Language: Haskell2010   Other-Extensions: TypeSynonymInstances, FlexibleInstances, CPP, GeneralizedNewtypeDeriving-  if flag(Readline)-    CPP-Options: "-DUSE_READLINE_PACKAGE"-    Build-Depends: readline+  if flag(Web)+    CPP-Options: "-DUSE_WEB_BACKEND"+    GHC-Options:+      -no-hs-main+      -optl-mexec-model=reactor+      -optl-Wl,--export=hs_init+      -optl-Wl,--export=hs_start+    Build-Depends: ghc-experimental+    if impl(ghc >= 9.10)+      Other-Extensions: JavaScriptFFI   else     if flag(Haskeline)       CPP-Options: "-DUSE_HASKELINE_PACKAGE"
− README.markdown 
@@ -1,66 +0,0 @@-An implementation of "A Categorical Programming Language"-=========================================================--[![Build Status](https://github.com/msakai/cpl/actions/workflows/build.yaml/badge.svg)](https://github.com/msakai/cpl/actions/workflows/build.yaml)-[![Hackage](https://img.shields.io/hackage/v/CPL.svg)](https://hackage.haskell.org/package/CPL)-[![Hackage Deps](https://img.shields.io/hackage-deps/v/CPL.svg)](https://packdeps.haskellers.com/feed?needle=CPL)-[![License](https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause)--This package is an implementation of "A Categorical Programming Language"-(CPL for short)[1][2] written in Haskell.--CPL is a functional programming language based on category-theory. Data types are declared in a categorical manner by-adjunctions. Data types that can be handled include the terminal-object, the initial object, the binary product functor, the binary-coproduct functor, the exponential functor, the natural number object,-the functor for finite lists, and the functor for infinite lists.-Each data type is declared with its basic operations or-morphisms. Programs consist of these morphisms, and execution of-programs is the reduction of elements (i.e. special morphisms) to-their canonical form.--Install----------De-Compress the archive and enter its top directory.-Then type:--```-$ cabal configure-$ cabal build-$ cabal install-```--If you want to compile with readline or haskeline, add `-fReadline` or-`-fHaskeline` respectively to the configure command.--Usage--------See chapter 5 of [1]--License----------This program is licensed under the BSD-style license.-(See the file [COPYING](COPYING).)--Copyright (C) 2004-2014 Masahiro Sakai <masahiro.sakai@gmail.com>--Author---------Masahiro Sakai <masahiro.sakai@gmail.com>--Bibliography---------------1. Tatsuya Hagino, “A Categorical Programming Language”.-    Ph.D. Thesis, University of Edinburgh, 1987.-    available at <http://web.sfc.keio.ac.jp/~hagino/index.html.en>--2. Tatsuya Hagino, “Categorical Functional Programming Language”.-    Computer Software, Vol 7, No.1.-    Advances in Software Science and Technology 4, 1992.-    ISBN 0-12-037104-9.
+ README.md view
@@ -0,0 +1,164 @@+An implementation of "A Categorical Programming Language"+=========================================================++[![Build Status](https://github.com/msakai/cpl/actions/workflows/build.yaml/badge.svg)](https://github.com/msakai/cpl/actions/workflows/build.yaml)+[![Hackage](https://img.shields.io/hackage/v/CPL.svg)](https://hackage.haskell.org/package/CPL)+[![Hackage Deps](https://img.shields.io/hackage-deps/v/CPL.svg)](https://packdeps.haskellers.com/feed?needle=CPL)+[![License](https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause)++This package is an implementation of "A Categorical Programming Language"+(CPL for short)[1][2] written in Haskell.++🚀 **Try CPL in your browser:** [WebAssembly Demo](https://msakai.github.io/cpl/) (no installation required!)++![CPL WebAssembly Demo](images/screenshot.png)++CPL is a functional programming language based on category+theory. Data types are declared in a categorical manner by+adjunctions. Data types that can be handled include the terminal+object, the initial object, the binary product functor, the binary+coproduct functor, the exponential functor, the natural number object,+the functor for finite lists, and the functor for infinite lists.+Each data type is declared with its basic operations or+morphisms. Programs consist of these morphisms, and execution of+programs is the reduction of elements (i.e. special morphisms) to+their canonical form.++📦 Install+-------++### Option 1: Use WebAssembly Version (No Installation) 🌐++Try CPL directly in your browser:+[https://msakai.github.io/cpl/](https://msakai.github.io/cpl/)++No installation required! Works on Chrome, Firefox, Safari, and Edge.++### Option 2: Build from Source 🔧++**Supported GHC versions:** >=9.2++#### Standard Build (Native)++De-Compress the archive and enter its top directory.+Then type:++```bash+$ cabal configure+$ cabal build+$ cabal install+```++If you want to compile without haskeline, add `-f-Haskeline` to the configure+command.++Alternatively, you can use Stack:++```bash+$ stack build+$ stack exec cpl+```++To disable haskeline with Stack, use the `--flag` option:++```bash+$ stack build --flag CPL:-Haskeline+```++#### WebAssembly Build++See [web/README.md](web/README.md) for detailed instructions on building and testing the WebAssembly version.++📖 Usage+-----++If you are new to CPL, we recommend starting with the [Tutorial](#tutorial) below.+For a concise reference of the language syntax, see chapter 5 of [1].++### Quick Start ⚡++Once you have CPL running (either in browser or terminal), try these commands:++```+cpl> edit+| right object 1 with !+| end object;+right object 1 defined+cpl> edit+| right object prod(a,b) with pair is+|   pi1: prod -> a+|   pi2: prod -> b+| end object;+right object prod(+,+) defined+cpl> edit+| right object exp(a,b) with curry is+|   eval: prod(exp,a) -> b+| end object;+right object exp(-,+) defined+cpl> edit+| left object nat with pr is+|   0: 1 -> nat+|   s: nat -> nat+| end object;+left object nat defined+cpl> show pair(pi2,eval)+pair(pi2,eval)+    : prod(exp(*a,*b),*a) -> prod(*a,*b)+cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)+add : prod(nat,nat) -> nat  defined+cpl> simp add.pair(s.s.0, s.0)+s.s.s.0+    : 1 -> nat+cpl> help+  exit                        exit the interpreter+  quit                        ditto+  bye                         ditto+  edit                        enter editing mode+  simp [full] <exp>           evaluate expression+  show <exp>                  print type of expression+  show function <name>        print information of function+  show object <functor>       print information of functor+  load <filename>             load from file+  set trace [on|off]          enable/disable trace+  reset                       remove all definitions+cpl> exit+```++For more examples, see the `samples/` directory.+For step-by-step explanations, see the [Tutorial](#tutorial) below.++### Tutorial++A comprehensive tutorial that covers CPL usage and the category theory concepts behind it.+No prior knowledge of category theory is required.++- [Tutorial (English)](TUTORIAL.md)+- [チュートリアル (日本語)](TUTORIAL_ja.md)++Topics covered: terminal objects, products, coproducts, exponential objects,+natural numbers, lists, infinite lists, and the duality between `left object` and `right object`.++License+-------++This program is licensed under the BSD-style license.+(See the file [COPYING](COPYING).)++Copyright (C) 2004-2026 Masahiro Sakai <masahiro.sakai@gmail.com>++Author+------++Masahiro Sakai <masahiro.sakai@gmail.com>++📖 Bibliography+------------++1. Tatsuya Hagino, “A Categorical Programming Language”.+    Ph.D. Thesis, University of Edinburgh, 1987.+    available at <https://web.sfc.keio.ac.jp/~hagino/index.html.en>++2. Tatsuya Hagino, “Categorical Functional Programming Language”.+    Computer Software, Vol 7, No.1.+    Advances in Software Science and Technology 4, 1992.+    ISBN 0-12-037104-9.
+ TUTORIAL.md view
@@ -0,0 +1,946 @@+# 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” (or “arrows”) 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](#introduction)+- [Basic Commands](#basic-commands)+- [Initial Screen Display](#initial-screen-display)+- [Defining Terminal Objects](#defining-terminal-objects)+- [Defining Cartesian Products](#defining-cartesian-products)+- [Defining Exponential Objects](#defining-exponential-objects)+- [Defining the Natural Numbers Object](#defining-the-natural-numbers-object)+- [Defining Coproducts](#defining-coproducts)+- [Displaying Types](#displaying-types)+- [Composing Morphisms and Identity Morphisms](#composing-morphisms-and-identity-morphisms)+- [Assigning Names to Expressions](#assigning-names-to-expressions)+- [Computation](#computation)+- [List Types](#list-types)+- [Infinite Lists](#infinite-lists)+- [Category Theory Background: Left vs. Right](#category-theory-background-left-vs.-right)+- [Summary](#summary)+- [References](#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 entering semicolon (`;`)+- **`show <expression>`**: Displays the type (domain and codomain) of an morphism (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 morphism by assigning it a name+- **`let <name>(<arguments>) = <expression>`**: Defines an morphism 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 morphism from `X` to `1`.” It serves as an “endpoint” representing an object with no information (or containing only one value). The unique morphism is written as `!`.++Visually, this corresponds to the following situation:++![](./doc-images/terminal-object.png)++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 entering 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 morphism `!` is also defined from any object to the terminal object.++The `show` command can also be used to display the morphism's type (domain and codomain). Here, `*a` is a variable representing an object, so this represents an morphism from any object to the terminal object 1.++```+cpl> show !+!+    : *a -> 1+```++## Defining the Product++Next, we'll define the **product**. The product 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 morphisms `π₁: A × B → A` and `π₂: A × B → B`+- For any object `X` with morphisms `f: X → A` and `g: X → B` to `A` and `B` respectively, there exists a unique morphism `⟨f,g⟩: X → A × B` such that `π₁ ∘ ⟨f,g⟩ = f` and `π₂ ∘ ⟨f,g⟩ = g` (this kind of property is referred to as the **universal property**).++Visually represented as a diagram:++![](./doc-images/product.png)++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 lacks arguments. The mearning is “Among all `x` equipped with `x -> a` and `x -> b`, we define the most general `x` as `prod(a,b)`,” but resuing 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 morphisms `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 morphism previously written as `⟨f,g⟩` is now written as `pair(f,g)` in this definition of products in CPL. The factorizer `pair` itself is not an morphism 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 morphisms `f: a -> c` and `g: b -> d` to `prod(a,b) -> prod(b,d)`. In category theory, a **functor** maps objects to objects and morphisms between objects to morphisms between mapped objects. Using `show function prod`, you can verify the type of `prod`'s action on morphisms.++```+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 **morphism 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 morphisms from `A` to `B`.” It possesses the following properties:++- An evaluation morphism `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 morphism `f: X × A → B`, there exists a unique curried morphism `curry(f): X → Bᴬ` satisfying `eval ∘ (curry(f) × I) = f`+  - (Here, `I: A → A` represents the identity morphism, and `×` denotes the product morphism operation)++Visualized as a diagram, it appears as follows:++![](./doc-images/exponential.png)++**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ᴬ` is 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 the terminal object, 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.++Let's examine how the functor `exp` operates on morphisms using `show function`:++```+cpl> show function exp+f0: *c -> *a  f1: *b -> *d+------------------------------------+exp(f0,f1): exp(*a,*b) -> exp(*c,*d)+```++Note the directionality of the argument morphisms, and how the parameters of `exp` change from domain to codomain in the result:++- `f0` is a morphism from `*c` to `*a`, but the parameter changes direction from `*a` to `*c` in the result+- `f1` is a morphism from `*b` to `*d`, and the direction of the parameter is the same, 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:++![](./doc-images/natural-numbers.png)++Please note the direction of the arrows. Whereas in the terminal objects, products, and exponential objects we have handled so far, there existed a unique morphism with that object as its *codomain*, in the case of the natural numbers object, conversely, there exists a unique morphism with that object as its *domain*.++Correspondences to programming concepts:++- The definition of natural numbers according to Peano's axioms+- Equivalent to Haskell data types such as:++  ```haskell+  data Nat = Zero | Succ Nat+  ```++- Recursive computations (folding)++Now, let's define the natural numbers object in CPL. While we have previously defined objects as `right object`s when there exists a unique morphism with that object as their *codomain*, we now define the natural numbers object as `left object` as there exists a unique morphism with that object as their *domain*:++```+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 has two injection morphisms `in₁: A → A + B` and `in₂: B → A + B` (which “inject” values into the coproduct)+- For any objects `X` and morphisms `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 is the dual concept of the product, obtained by “reversing the arrow,” and serves as a good example of symmetry in category theory.++Visualized graphically, it appears as follows: (Compare with the product diagram to verify that morphisms are reversed):++![](./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 ranging over objects, and the morphism actually denotes families of morphisms with varying 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 morphism 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 morphism 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 “morphism 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” morphism, 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 morphism 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 exponential object.++2. **Curried addition `add'`**:+   - `add': nat → exp(nat, nat)` — An morphism 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 morphism 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 morphisms 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 morphism expressions using the `simp` command. Let's simplify an morphism 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 morphism 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 lists are parameterized by their element type:++- 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:++![](./doc-images/list.png)++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, that is, a functor. Let's examine its action on morphisms. In functional programming, this action of the 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 want to use these names when working with infinite lists later. In CPL, since only total functions exist and no partial functions are allowed, the codomain is a coproduct 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 coproduct with `1`, allowing us to apply `head` / `tail` to the results of these operations again.++```+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)` | `x : xs` (Prepend `x` to the beginning of `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 morphisms 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 of factorizer**: 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 of factorizer**: **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, Right adjoint, F-coalgebra  | Unifies “incoming” morphisms via universal morphisms   |+| left object   | Colimit, Left adjoing, F-algebra   | 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 view
@@ -0,0 +1,946 @@+# 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](#圏論的背景-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` からも、ただ一つだけ射が存在する対象」のことです。これは「終点」のような役割を果たし、情報を持たない（あるいは唯一の値しか持たない）対象を表します。ただ一つだけ存在する射を `!` と書きます。++図式で描くと以下のような状況です。++![](./doc-images/terminal-object.png)++プログラミングとの対応:++- 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` を満たす（このような性質は**普遍性**と呼ばれます）++図式として描くと以下のようになります：++![](./doc-images/product.png)++プログラミングとの対応:++- 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` は恒等射を、 `×` は直積の射への作用を表しています)++図式として描くと以下のようになります：++![](./doc-images/exponential.png)++**なぜ指数対象が「関数空間」なのか？** 集合の圏で具体的に考えてみましょう。++- **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、原始再帰) は**数学的帰納法**に対応し、自然数上の関数を定義する基本的な方法です。++これを図式として描くと以下のようになります。++![](./doc-images/natural-numbers.png)++矢印の向きに注意してください。これまで取り扱ってきた終対象・直積・指数対象では、その対象を*余域*とする一意な射が存在したのに対して、自然数対象の場合には、逆にその対象を*始域*とする一意な射が存在します。++プログラミングとの対応:++- ペアノの公理による自然数の定義+- Haskellの以下のようなデータ型に相当:++  ```haskell+  data Nat = Zero | Succ Nat+  ```++- 再帰的な計算（畳み込み、fold）++それではCPLで自然数対象を定義しましょう。これまで扱ってきた、その対象を*余域*とする一意な射が存在する場合には `right object` として対象を定義していましたが、その対象を*始域*とする一意な射が存在する場合には `left object` として対象を定義します:++```+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` を満たす++これは直積の「矢印を逆にした」双対概念であり、圏論における対称性の良い例です。++図式で描くと以下のようになります（直積の図式と比較して、矢印が逆になっていることを確認してください）：++![](./doc-images/coproduct.png)++プログラミングとの対応:++- 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` を定義しましょう。通常の関数型言語では以下のように書ける関数です:++```haskell+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` により、リストを再帰的に処理++図式を描くと以下のようになります。++![](./doc-images/list.png)++これは**帰納的データ型**の典型例で、有限の構造を表現します。++プログラミングとの対応:++- 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 : xs` (`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` と呼ばれます）++有限リストが「構築して消費する」のに対し、無限リストは「状態から展開していく」という対照的な構造を持ちます。++図式を描くと以下のようになります。++![](./doc-images/inflist.png)++プログラミングとの対応:++- 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)、右随伴 (right adjoint)、F-余代数 (F-coalgebra) | 普遍射により「入射」を統一  |+| left object   | 余極限 (colimit)、左随伴 (left adjoint)、F-代数 (F-algebra)  | 余普遍射により「出射」を統一 |++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と圏論の世界への第一歩となれば幸いです。楽しいプログラミングを!
+ doc-images/Makefile view
@@ -0,0 +1,18 @@+TEXS := $(wildcard *.tex)+PDFS := $(TEXS:.tex=.pdf)+PNGS := $(TEXS:.tex=.png)++LATEXMK = latexmk -pdf -interaction=nonstopmode+MAGICK  = magick -density 300++all: $(PNGS)++%.pdf: %.tex+	$(LATEXMK) $<++%.png: %.pdf+	$(MAGICK) $< $@++clean:+	latexmk -C+	rm -f *.png
+ doc-images/coproduct.png view

binary file changed (absent → 8798 bytes)

+ doc-images/coproduct.tex view
@@ -0,0 +1,10 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+A \arrow[rrdd, bend right, "f"'] \arrow[rr, "\mathrm{in}_1"] & & A+B \arrow[dd, "{\mathrm{case}(f,g)}" description] & & B \arrow[ll, "\mathrm{in}_2"'] \arrow[lldd, bend left, "g"] \\+\\+& & X+\end{tikzcd}+\end{document}
+ doc-images/exponential.png view

binary file changed (absent → 7322 bytes)

+ doc-images/exponential.tex view
@@ -0,0 +1,10 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+B^A \times A \arrow[rr, "\mathrm{eval}"] & & B \\+\\+X \times A \arrow[uu, dashed, "\mathrm{curry}(f)\times I" description] \arrow[uurr, bend right, "f"']+\end{tikzcd}+\end{document}
+ doc-images/inflist.png view

binary file changed (absent → 9516 bytes)

+ doc-images/inflist.tex view
@@ -0,0 +1,10 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+A & & \mathrm{inflist}(A) \arrow[ll, "\mathrm{head}"'] \arrow[rr, "\mathrm{tail}"] & & \mathrm{inflist}(A) \\+\\+  & & X \arrow[uull, bend left, "h"] \arrow[rr, "t"'] \arrow[uu, dashed, "{\mathrm{fold}(h,t)}" description] & & X \arrow[uu, dashed, "{\mathrm{fold}(h,t)}" description]+\end{tikzcd}+\end{document}
+ doc-images/list.png view

binary file changed (absent → 9965 bytes)

+ doc-images/list.tex view
@@ -0,0 +1,10 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+\mathbf{1} \arrow[rr, "\mathrm{nil}"] \arrow[rrdd, bend right, "z"'] & & \mathrm{list}(A) \arrow[dd, "{\mathrm{prl}(z,f)}" description] & & A\times \mathrm{list}(A) \arrow[ll, "\mathrm{cons}"'] \arrow[dd, "{I \times \mathrm{prl}(z,f)}" description] \\+\\+& & X & & A\times X \arrow[ll, "f"]+\end{tikzcd}+\end{document}
+ doc-images/natural-numbers.png view

binary file changed (absent → 7357 bytes)

+ doc-images/natural-numbers.tex view
@@ -0,0 +1,10 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+1 \arrow[rr, "0"] \arrow[rrdd, bend right, "z"'] & & \mathbb{N} \arrow[dd, dashed, "{\mathrm{pr}(z,f)}" description] \arrow[rr, "s"] & & \mathbb{N} \arrow[dd, dashed, "{\mathrm{pr}(z,f)}" description] \\+\\+& & X \arrow[rr, "f"'] & & X+\end{tikzcd}+\end{document}
+ doc-images/product.png view

binary file changed (absent → 8266 bytes)

+ doc-images/product.tex view
@@ -0,0 +1,12 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+A & & A\times B \arrow[ll, "\pi_1"'] \arrow[rr, "\pi_2"] & & B \\+\\+  & & X \arrow[lluu, bend left, "f"]+        \arrow[uu, dashed, "{\langle f, g \rangle}" description]+        \arrow[rruu, bend right, "g"']+\end{tikzcd}+\end{document}
+ doc-images/terminal-object.png view

binary file changed (absent → 1297 bytes)

+ doc-images/terminal-object.tex view
@@ -0,0 +1,9 @@+\documentclass{standalone}+\usepackage{amssymb}+\usepackage{tikz-cd}+\begin{document}+\begin{tikzcd}+  \mathbf{1} \\+  X \arrow[u, dashed, "!"]+\end{tikzcd}+\end{document}
+ images/screenshot.png view

binary file changed (absent → 153300 bytes)

samples/examples.txt view
@@ -1,45 +1,50 @@-% cpl.rb -cpl.rb (An Implementation of Categorical Programming Language)-version 0.0.1+Categorical Programming Language (Haskell version)+version 0.2.0++Type help for help+ cpl> edit | right object 1 with ! | end object;-right object 1 defined+right object 1 is defined cpl> edit | right object prod(a,b) with pair is |   pi1: prod -> a |   pi2: prod -> b | end object;-right object prod(+,+) defined+right object prod(+,+) is defined cpl> edit | right object exp(a,b) with curry is |   eval: prod(exp,a) -> b | end object;-right object exp(-,+) defined+right object exp(-,+) is defined cpl> edit | left object nat with pr is |   0: 1 -> nat |   s: nat -> nat | end object;-left object nat defined+left object nat is defined cpl> edit | left object coprod(a,b) with case is |   in1: a -> coprod |   in2: b -> coprod | end object;-left object coprod(+,+) defined+left object coprod(+,+) is defined cpl> show pair(pi2,eval) pair(pi2,eval)     : prod(exp(*a,*b),*a) -> prod(*a,*b) cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)-add : prod(nat,nat) -> nat  defined+add = eval.prod(pr(curry(pi2),curry(s.eval)),I)+    : prod(nat,nat) -> nat cpl> simp add.pair(s.s.0, s.0) s.s.s.0     : 1 -> nat cpl> let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I)-mult : prod(nat,nat) -> nat+mult = eval.prod(pr(curry(0.!),curry(add.pair(eval,pi2))),I)+    : prod(nat,nat) -> nat cpl> let fact=pi1.pr(pair(s.0,0), pair(mult.pair(s.pi2,pi1), s.pi2))-fact : nat -> nat  defined+fact = pi1.pr(pair(s.0,0),pair(mult.pair(s.pi2,pi1),s.pi2))+    : nat -> nat 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@@ -48,21 +53,28 @@ |   nil: 1 -> list |   cons: prod(p,list) -> list | end object;-left object list(+) defined+left object list(+) is defined 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+append = eval.prod(prl(curry(pi2),curry(cons.pair(pi1.pi1,eval.pair(pi2.pi1,pi2)))),I)+    : prod(list(*a),list(*a)) -> list(*a) cpl> let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!)))-reverse : list(*a) -> list(*a)  defined+reverse = prl(nil,append.pair(pi2,cons.pair(pi1,nil.!)))+    : list(*a) -> list(*a) cpl> let hd = prl(in2, in1.pi1)-hd : list(*a) -> coprod(*a,1)  defined+hd = prl(in2,in1.pi1)+    : list(*a) -> coprod(*a,1) cpl> let hdp=case(hd,in2)-hdp : coprod(list(*a),1) -> coprod(*a,1)  defined+hdp = case(hd,in2)+    : coprod(list(*a),1) -> coprod(*a,1) cpl> let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil)))-tl : list(*a) -> coprod(list(*a),1)  defined+tl = coprod(pi2,I).prl(in2,in1.prod(I,case(cons,nil)))+    : list(*a) -> coprod(list(*a),1) cpl> let tlp = case(tl, in2)-tlp : coprod(list(*a),1) -> coprod(list(*a),1)  defined+tlp = case(tl,in2)+    : coprod(list(*a),1) -> coprod(list(*a),1) cpl> let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons))-seq : nat -> list(nat)  defined+seq = pi2.pr(pair(0,nil),pair(s.pi1,cons))+    : nat -> list(nat) cpl> simp seq.s.s.s.0 cons.pair(s.pi1,cons).pair(s.pi1,cons).pair(0,nil)     : 1 -> list(nat)@@ -71,7 +83,7 @@     : 1 -> list(nat) cpl> simp hdp.tl.seq.s.s.s.0 in1.s.0-    : 1 -> coprod(nat,*a)+    : 1 -> coprod(nat,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)@@ -83,9 +95,10 @@ |   head: inflist -> a |   tail: inflist -> inflist | end object;-right object inflist(+) defined+right object inflist(+) is defined cpl> let incseq=fold(I,s).0-incseq : 1 -> inflist(nat)  defined+incseq = fold(I,s).0+    : 1 -> inflist(nat) cpl> simp head.incseq 0     : 1 -> nat@@ -93,9 +106,11 @@ s.s.s.0     : 1 -> nat cpl> let alt=fold(head.pi1, pair(pi2, tail.pi1))-alt : prod(inflist(*a),inflist(*a)) -> inflist(*a)  defined+alt = fold(head.pi1,pair(pi2,tail.pi1))+    : prod(inflist(*a),inflist(*a)) -> inflist(*a) cpl> let infseq=fold(I,I).0-infseq : 1 -> inflist(nat)  defined+infseq = fold(I,I).0+    : 1 -> inflist(nat) cpl> simp head.tail.tail.alt.pair(incseq, infseq) s.0     : 1 -> nat
+ scripts/build-wasm.sh view
@@ -0,0 +1,158 @@+#!/bin/bash+set -e++# CPL WebAssembly Build Script+# Builds CPL interpreter for WebAssembly using GHC's WASM backend+# Output goes to _site/ directory for local testing and deployment++echo "================================================"+echo "Building CPL for WebAssembly"+echo "================================================"+echo ""++# Check for required tools+echo "Checking toolchain..."++if ! command -v wasm32-wasi-ghc &> /dev/null; then+    echo "Error: wasm32-wasi-ghc not found"+    echo ""+    echo "Please install the GHC WebAssembly cross-compiler:"+    echo "  https://ghc.gitlab.haskell.org/ghc/doc/users_guide/wasm.html"+    echo ""+    echo "For macOS/Linux, you can download pre-built binaries:"+    echo "  https://downloads.haskell.org/~ghc/"+    exit 1+fi++if ! command -v wasm32-wasi-cabal &> /dev/null; then+    echo "Error: wasm32-wasi-cabal not found"+    echo ""+    echo "Please ensure the GHC WASM toolchain is properly installed."+    exit 1+fi++echo "✓ wasm32-wasi-ghc found: $(wasm32-wasi-ghc --version | head -n1)"+echo "✓ wasm32-wasi-cabal found: $(wasm32-wasi-cabal --version | head -n1)"+echo ""++# Get project root (script is in scripts/)+PROJECT_ROOT="$(cd "$(dirname "$0")/.." && pwd)"+cd "$PROJECT_ROOT"++echo "Project root: $PROJECT_ROOT"+echo ""++# Output directory+OUTPUT_DIR="$PROJECT_ROOT/_site"++# Clean previous build artifacts (optional)+if [ "$1" = "--clean" ]; then+    echo "Cleaning previous build artifacts..."+    rm -rf dist-newstyle+    echo "✓ Clean complete"+    echo ""+fi++# Create output directory+mkdir -p "$OUTPUT_DIR"++echo "Generating sample files module..."+"$PROJECT_ROOT/scripts/generate-samples-js.sh"+echo ""++echo ""+echo "Configuring CPL for WebAssembly..."+wasm32-wasi-cabal configure -fWeb -f-Haskeline++echo ""+echo "Building CPL..."+wasm32-wasi-cabal build++echo ""+echo "Locating WASM binary..."++# Find the compiled WASM binary+WASM_BIN=$(wasm32-wasi-cabal list-bin cpl)++if [ -z "$WASM_BIN" ]; then+    echo "Error: Could not find compiled WASM binary"+    echo "Expected to find 'cpl.wasm' in dist-newstyle/build/wasm32-wasi/..."+    exit 1+fi++echo "✓ Found WASM binary: $WASM_BIN"++# Copy WASM binary to output directory+echo ""+echo "Copying WASM binary to $OUTPUT_DIR/cpl.wasm..."+cp "$WASM_BIN" "$OUTPUT_DIR/cpl.wasm"+echo "✓ Copied WASM binary"++# Post-link processing (if available)+echo ""+echo "Checking for post-link processor..."+LIBDIR=$(wasm32-wasi-ghc --print-libdir)++if [ -f "$LIBDIR/post-link.mjs" ]; then+    echo "Running post-link processor..."+    node "$LIBDIR/post-link.mjs" -i "$OUTPUT_DIR/cpl.wasm" -o "$OUTPUT_DIR/cpl.js"+    echo "✓ Post-link processing complete"+else+    echo "ℹ No post-link processor found (this is usually fine)"+fi++# Copy source files from web/ to output directory+echo ""+echo "Copying web files to $OUTPUT_DIR/..."+cp "$PROJECT_ROOT/web/index.html" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/cpl-terminal.js" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/favicon.ico" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/favicon-16x16.png" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/favicon-32x32.png" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/apple-touch-icon.png" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/icon-192x192.png" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/icon-512x512.png" "$OUTPUT_DIR/"+cp "$PROJECT_ROOT/web/manifest.json" "$OUTPUT_DIR/"+echo "✓ Copied web files"++# Get file size+WASM_SIZE=$(du -h "$OUTPUT_DIR/cpl.wasm" | cut -f1)++echo ""+echo "================================================"+echo "Build complete!"+echo "================================================"+echo ""+echo "Output directory: $OUTPUT_DIR"+echo "WASM binary size: $WASM_SIZE"+echo ""+echo "To test locally, run:"+echo "  python3 -m http.server -d _site 8000"+echo "Then open: http://localhost:8000"+echo ""+echo "For full site with tutorials, also run:"+echo "  ./scripts/build-tutorial.sh"+echo ""++# Verify required files exist+echo "Checking output files..."+MISSING_FILES=0++for f in index.html cpl-terminal.js cpl.wasm cpl.js samples.js favicon.ico favicon-16x16.png favicon-32x32.png apple-touch-icon.png icon-192x192.png icon-512x512.png manifest.json; do+    if [ -f "$OUTPUT_DIR/$f" ]; then+        echo "  ✓ $f"+    else+        echo "  ✗ $f (missing)"+        MISSING_FILES=1+    fi+done++if [ $MISSING_FILES -eq 0 ]; then+    echo ""+    echo "✓ All required files present"+else+    echo ""+    echo "⚠ Some files are missing. The web interface may not work correctly."+fi++echo ""
+ scripts/generate-favicons.sh view
@@ -0,0 +1,86 @@+#!/bin/bash+set -euo pipefail++# Script to generate favicon files from source logo images+# Usage: ./scripts/generate-favicons.sh+#+# Requires: ImageMagick (magick command)+#+# Source images:+#   - logo-with-diagram.png: Used for larger icons (180x180+)+#   - logo-without-diagram.png: Used for smaller icons (32x32 and below)++SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"+PROJECT_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"+OUTPUT_DIR="${PROJECT_ROOT}/web"++echo "=== Generating Favicon Files ==="++# Check if ImageMagick is installed+if ! command -v magick &> /dev/null; then+    echo "Error: ImageMagick is not installed"+    echo "Install with: brew install imagemagick  (macOS)"+    echo "          or: sudo apt-get install imagemagick  (Ubuntu/Debian)"+    exit 1+fi++echo "ImageMagick found: $(magick --version | head -n1)"++# Check source images exist+LOGO_WITH_DIAGRAM="${PROJECT_ROOT}/logo-with-diagram.png"+LOGO_WITHOUT_DIAGRAM="${PROJECT_ROOT}/logo-without-diagram.png"++if [ ! -f "$LOGO_WITH_DIAGRAM" ]; then+    echo "Error: $LOGO_WITH_DIAGRAM not found"+    exit 1+fi++if [ ! -f "$LOGO_WITHOUT_DIAGRAM" ]; then+    echo "Error: $LOGO_WITHOUT_DIAGRAM not found"+    exit 1+fi++echo "Source images found:"+echo "  - $LOGO_WITH_DIAGRAM"+echo "  - $LOGO_WITHOUT_DIAGRAM"+echo ""++# Create output directory if needed+mkdir -p "$OUTPUT_DIR"++# Generate small icons from logo-without-diagram.png+# (The diagram is not visible at small sizes)+echo "Generating small icons from logo-without-diagram.png..."+magick "$LOGO_WITHOUT_DIAGRAM" -resize 16x16 "$OUTPUT_DIR/favicon-16x16.png"+echo "  Created favicon-16x16.png"++magick "$LOGO_WITHOUT_DIAGRAM" -resize 32x32 "$OUTPUT_DIR/favicon-32x32.png"+echo "  Created favicon-32x32.png"++# Generate favicon.ico (multi-resolution)+TMPDIR=$(mktemp -d)+magick "$LOGO_WITHOUT_DIAGRAM" -resize 16x16 "$TMPDIR/16.png"+magick "$LOGO_WITHOUT_DIAGRAM" -resize 32x32 "$TMPDIR/32.png"+magick "$TMPDIR/16.png" "$TMPDIR/32.png" "$OUTPUT_DIR/favicon.ico"+rm -rf "$TMPDIR"+echo "  Created favicon.ico (16x16 + 32x32)"++# Generate large icons from logo-with-diagram.png+# (The diagram is visible at larger sizes)+echo ""+echo "Generating large icons from logo-with-diagram.png..."++magick "$LOGO_WITH_DIAGRAM" -resize 180x180 "$OUTPUT_DIR/apple-touch-icon.png"+echo "  Created apple-touch-icon.png (180x180)"++magick "$LOGO_WITH_DIAGRAM" -resize 192x192 "$OUTPUT_DIR/icon-192x192.png"+echo "  Created icon-192x192.png (192x192)"++magick "$LOGO_WITH_DIAGRAM" -resize 512x512 "$OUTPUT_DIR/icon-512x512.png"+echo "  Created icon-512x512.png (512x512)"++echo ""+echo "=== Favicon generation complete ==="+echo ""+echo "Generated files in $OUTPUT_DIR/:"+ls -la "$OUTPUT_DIR"/favicon* "$OUTPUT_DIR"/apple-touch-icon.png "$OUTPUT_DIR"/icon-*.png 2>/dev/null | awk '{print "  " $9 " (" $5 " bytes)"}'
+ scripts/generate-samples-js.sh view
@@ -0,0 +1,25 @@+#!/bin/bash+set -e++# Generate _site/samples.js from samples/ directory+# This script converts .cpl and .cdt files into a JavaScript module+# that can be imported by the web frontend.++PROJECT_ROOT="$(cd "$(dirname "$0")/.." && pwd)"+OUTPUT_DIR="$PROJECT_ROOT/_site"+mkdir -p "$OUTPUT_DIR"+OUTPUT="$OUTPUT_DIR/samples.js"++echo "// Auto-generated from samples/ directory. Do not edit manually." > "$OUTPUT"+echo "export const sampleFiles = {" >> "$OUTPUT"++for f in "$PROJECT_ROOT"/samples/*.cpl "$PROJECT_ROOT"/samples/*.cdt; do+  [ -f "$f" ] || continue+  name="samples/$(basename "$f")"+  # Use node for safe JSON escaping+  content=$(node -e "process.stdout.write(JSON.stringify(require('fs').readFileSync('$f', 'utf8')))")+  echo "  $(node -e "process.stdout.write(JSON.stringify('$name'))"):  $content," >> "$OUTPUT"+done++echo "};" >> "$OUTPUT"+echo "Generated $OUTPUT"
src/AExp.hs view
@@ -3,7 +3,7 @@ -- Module      :  AExp -- Copyright   :  (c) Masahiro Sakai 2004,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -95,7 +95,7 @@ -- XXX aexpType :: AExp -> Type aexpType = f-  where +  where     f (Identity a) = a :-> a     f (Comp g h) = dom (f h) :-> cod (f g)     f (Nat nat annotation) =
src/CDT.hs view
@@ -1,13 +1,13 @@-{-# LANGUAGE CPP, FlexibleContexts #-}+{-# LANGUAGE FlexibleContexts #-} ----------------------------------------------------------------------------- -- | -- Module      :  CDT -- Copyright   :  (c) Masahiro Sakai 2004,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional--- Portability :  non-portable (CPP, FlexibleContexts)+-- Portability :  non-portable (FlexibleContexts) -- -- Categorical Data Type --@@ -59,9 +59,7 @@ import Type import Subst (tv, apply) -#if __GLASGOW_HASKELL__ >= 706 import Prelude hiding (join)-#endif import Data.List (findIndices, transpose, find, findIndex, intercalate)  @@ -242,7 +240,7 @@ ----------------------------------------------------------------------------  makeProjectionSequence :: FE -> [Int]-makeProjectionSequence fe = +makeProjectionSequence fe =   case fe of     FE.Var 0 -> []     FE.Var _ ->@@ -258,7 +256,7 @@     Just nat -> natIndex nat : makeProjectionSequence (natDeclDom nat)     _        -> error "BUG"   where-    f nat = i+1 `elem` tv (natDeclCod nat) && +    f nat = i+1 `elem` tv (natDeclCod nat) &&             case natDeclDom nat of               FE.Var 0 -> True               _        -> False
src/CDTParser.hs view
@@ -3,7 +3,7 @@ -- Module      :  CDTParser -- Copyright   :  (c) Masahiro Sakai 2006,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -24,7 +24,8 @@ import CDT import ParserUtils -import Text.ParserCombinators.Parsec+import Text.Parsec hiding (string')+import Text.Parsec.String (Parser) import Control.Monad import Data.List @@ -33,7 +34,7 @@ data CDTDecl = CDTDecl !ObjectType String !Int String [(String, Type)]  cdtDecl :: Parser CDTDecl-cdtDecl = +cdtDecl =     do t <- mplus (string' "left"  >> return LeftObject)                   (string' "right" >> return RightObject)        string' "object"@@ -44,7 +45,7 @@        string' "with"        fact_name <- ident        let endObject  = string' "end" >> string' "object"-           normalDecl = do string' "is"+           normalDecl = do optional (try (string' "is"))                            manyTill (try (nat_decl (name : params)))                                     (try endObject)            emptyDecl  = endObject >> return []@@ -52,7 +53,7 @@        return $ CDTDecl t name (length params) fact_name nat_decls  nat_decl :: [String] -> Parser (String, Type)-nat_decl params = +nat_decl params =     do name <- ident        char' ':'        let f x = x `elemIndex` params@@ -63,7 +64,7 @@  fe :: (String -> Maybe Int) -> Parser FE fe lookupVar = fe'-    where fe' = +    where fe' =             do name <- ident                params <- option [] $ between (char' '(') (char' ')')                                    $ sepBy fe' (char' ',')
src/CPLSystem.hs view
@@ -4,7 +4,7 @@ -- Copyright   :  (c) Masahiro Sakai 2004,2009  -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -22,6 +22,7 @@     , addCDT     , letExp     , simp+    , getFunctionSignature     ) where  import CDT@@ -41,7 +42,7 @@ import Control.Monad import Data.Maybe import Data.List-import Text.ParserCombinators.Parsec+import Text.Parsec import qualified Data.Map as Map  type CDTEnv = [CDT]@@ -70,8 +71,8 @@     Left err -> Left (show err)     Right e ->       case ExpParser.evalExp (objects sys) (arityEnv sys) e of-        Nothing -> Left "invalid expression" -- FIXME-        Just e2 ->+        Left err -> Left err+        Right e2 ->           Typing.runTI (tiEnv sys) $ do             t <- Typing.inferType (substIt sys e2)             t2 <- Typing.appSubst t@@ -85,8 +86,8 @@     Left err -> Left (show err)     Right (name,ps,e) ->       case ExpParser.evalExp (objects sys) (Map.union (Map.fromList (zip ps (repeat 0))) (arityEnv sys)) e of-        Nothing -> Left "invalid definition" -- FIXME-        Just e1 ->+        Left err -> Left err+        Right e1 ->           Typing.runTI (tiEnv sys) $ do             (ts, t) <- Typing.inferType2 ps e1             ts2 <- Typing.appSubst ts@@ -103,7 +104,7 @@ tiEnv sys = Map.map (\(_, _, t) -> Left t) (varTable sys)  substIt :: System -> Exp -> Exp-substIt sys e = +substIt sys e =   case lastExp sys of     Nothing -> e     Just it -> f e@@ -124,7 +125,8 @@   where     vt = varTable sys     objs = objects sys-    names = Map.keys vt +++    names = ExpParser.identityNames +++            Map.keys vt ++             map CDT.functName objs ++             map CDT.factName objs  ++             concatMap (map CDT.natName . CDT.nats) objs@@ -160,3 +162,33 @@                then Simp.simpWithTrace full e'                else [(0, compile sys Identity, Simp.simp full e')]     in traces++inferFunctType :: System -> CDT -> Either String ([Type], Type)+inferFunctType sys obj = Typing.runTI (tiEnv sys) $ do+  let ps = ["f" ++ show i | (i, _) <- zip [0..] (CDT.functVariance obj)]+  (ts, t) <- Typing.inferType2 ps (Funct obj [Var v [] | v <- ps])+  ts2 <- Typing.appSubst ts+  (_ :! t2) <- Typing.appSubst t+  let vars = Subst.tv (t2 : ts2)+      s = zip vars [FE.Var i | i<-[0..]]+  return (Subst.apply s ts2, Subst.apply s t2)++getFunctionSignature :: System -> String -> Maybe ([(String, Type)], Type)+getFunctionSignature _sys name | name `elem` ExpParser.identityNames = Just ([], FE.Var 0 :-> FE.Var 0)+getFunctionSignature sys name+  | Just (args, _e, FType _ args' t) <- Map.lookup name (varTable sys) =+      Just (zip args args', t)+  | otherwise = listToMaybe $ do+      obj <- objects sys+      msum+        [ do nat <- CDT.nats obj+             guard $ CDT.natName nat == name+             return ([], CDT.natType nat)+        , do guard $ CDT.factName obj == name+             return (zip ["f" ++ show i | i <- [0..]] (CDT.factParams obj), CDT.factDestType obj)+        , do guard $ CDT.functName obj == name+             let ps = ["f" ++ show i | (i, _) <- zip [0..] (CDT.functVariance obj)]+             case inferFunctType sys obj of+               Left err -> error err  -- This should not happen+               Right (ts, t) -> return (zip ps ts, t)+        ]
src/Exp.hs view
@@ -3,7 +3,7 @@ -- Module      :  Exp -- Copyright   :  (c) Masahiro Sakai 2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable
src/ExpParser.hs view
@@ -3,7 +3,7 @@ -- Module      :  ExpParser -- Copyright   :  (c) Masahiro Sakai 2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -15,6 +15,7 @@     , exp     , def     , evalExp+    , identityNames     ) where  import qualified CDT@@ -23,9 +24,13 @@  import Prelude hiding (exp) import Control.Monad-import Text.ParserCombinators.Parsec+import Control.Monad.Except+import Text.Parsec hiding (string')+import Text.Parsec.String (Parser)+import Data.List (find) import Data.Maybe import qualified Data.Map as Map+import Text.Printf  ---------------------------------------------------------------------------- @@ -38,7 +43,7 @@ exp =     do xs <- sepBy1 pident (tok (char '.' `mplus` char '\x2218'))        return (foldr1 Comp xs)-    where pident = +    where pident =               do s  <- ident                  xs <- option [] $ between (char' '(') (char' ')')                                  $ exp `sepBy` char' ','@@ -60,31 +65,41 @@  type CDTEnv = [CDT.CDT] -evalExp :: CDTEnv -> (Map.Map String Int) -> Exp -> Maybe E.Exp-evalExp cenv env = listToMaybe . f-    where f (Comp a b) =-              do a' <- f a-                 b' <- f b-                 return (E.Comp a' b')-          f (Ident "I" args) =-              do guard (length args == 0)-                 return E.Identity-          f (Ident s args)  =-              do let arity = length args-                 args' <- mapM f args-                 o <- cenv-                 msum [ do guard $ CDT.functName o  == s &&-                                   CDT.functArity o == arity-                           return (E.Funct o args')-                      , do guard $ CDT.factName o == s &&-                                   CDT.nNats o == arity-                           return (E.Fact o args')-                      , do guard $ arity == 0-                           n <- CDT.nats o-                           guard $ CDT.natName n == s-                           return (E.Nat n)-                      , do guard $ Just arity == Map.lookup s env-                           return (E.Var s args')-                      ]+evalExp :: CDTEnv -> (Map.Map String Int) -> Exp -> Either String E.Exp+evalExp cenv env = f+  where+    f :: Exp -> Either String E.Exp+    f (Comp a b) = do+      a' <- f a+      b' <- f b+      return (E.Comp a' b')+    f (Ident s args) | s `elem` identityNames = do+      unless (length args == 0) $+        throwError $ printf "%s: wrong number of arguments (given %d, expected %d)" s (length args) (0 :: Int)+      return E.Identity+    f (Ident s args)  = do+      let arity = length args+      args' <- mapM f args+      case () of+        _ | Just o <- find (\o -> CDT.functName o  == s) cenv -> do+          unless (CDT.functArity o == arity) $+            throwError $ printf "%s: wrong number of arguments (given %d, expected %d)" s arity (CDT.functArity o)+          return (E.Funct o args')+        _ | Just o <- find (\o -> CDT.factName o  == s) cenv -> do+          unless (CDT.nNats o == arity) $+            throwError $ printf "%s: wrong number of arguments (given %d, expected %d)" s arity (CDT.nNats o)+          return (E.Fact o args')+        _ | Just n <- find (\n -> CDT.natName n == s) [n | o <- cenv, n <- CDT.nats o] -> do+          unless (arity == 0) $+            throwError $ printf "%s: wrong number of arguments (given %d, expected %d)" s arity (0 :: Int)+          return (E.Nat n)+        _ | Just arity' <- Map.lookup s env -> do+          unless (arity == arity') $+            throwError $ printf "%s: wrong number of arguments (given %d, expected %d)" s arity arity'+          return (E.Var s args')+        _ -> throwError ("unknown symbol: " ++ s)++identityNames :: [String]+identityNames = ["I", "id"]  ----------------------------------------------------------------------------
src/FE.hs view
@@ -4,7 +4,7 @@ -- Module      :  FE -- Copyright   :  (c) Masahiro Sakai 2004,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable
src/Main.hs view
@@ -1,10 +1,14 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+#if defined(USE_WEB_BACKEND)+{-# LANGUAGE JavaScriptFFI #-}+#endif ----------------------------------------------------------------------------- -- | -- Module      :  Main -- Copyright   :  (c) Masahiro Sakai 2004,2009,2014 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -23,9 +27,11 @@ import qualified Simp import Paths_CPL +import Control.Exception (try, SomeException) import Data.Maybe import Data.List import Data.Char (isSpace)+import qualified Data.Map as Map import Data.Version import System.Environment import System.Exit@@ -34,9 +40,9 @@ import Control.Monad.Except import Control.Monad.State.Strict -- haskeline's MonadException requries strict version import System.Console.GetOpt-#if defined(USE_READLINE_PACKAGE)-import qualified System.Console.SimpleLineEditor as SLE-import Control.Exception (bracket)+#if defined(USE_WEB_BACKEND)+import GHC.Wasm.Prim (JSString (..), toJSString, fromJSString, JSException (..), JSVal)+import Control.Exception (evaluate) #elif defined(USE_HASKELINE_PACKAGE) import qualified System.Console.Haskeline as Haskeline #else@@ -45,38 +51,73 @@  ---------------------------------------------------------------------------- -#ifdef USE_HASKELINE_PACKAGE-type Console = Haskeline.InputT IO-#else+#if defined(USE_WEB_BACKEND)++-- JavaScript FFI imports for WebAssembly backend+foreign import javascript "terminal_readLine($1)"+  js_readLine :: JSString -> IO JSString++foreign import javascript unsafe "terminal_printLine($1)"+  js_printLine :: JSString -> IO ()++foreign import javascript unsafe "terminal_initialize()"+  js_initialize :: IO ()++foreign import javascript "terminal_loadFile($1)"+  js_loadFile :: JSString -> IO JSString++foreign import javascript "$1.toString()"+  js_toString :: JSVal -> IO JSString++-- Export main function for JavaScript to call as hs_start+foreign export javascript "hs_start" main :: IO ()+ type Console = IO-#endif  runConsole :: Console a -> IO a-#if defined(USE_READLINE_PACKAGE)-runConsole m = bracket SLE.initialise (const SLE.restore) (const m)+runConsole m = js_initialize >> m++readLine' :: String -> Console String+readLine' prompt = do+  result <- js_readLine (toJSString prompt)+  return $ fromJSString result++printLine' :: String -> Console ()+printLine' str = js_printLine (toJSString str)+ #elif defined(USE_HASKELINE_PACKAGE)++type Console = Haskeline.InputT IO++runConsole :: Console a -> IO a runConsole m = Haskeline.runInputT Haskeline.defaultSettings m++readLine' :: String -> Console String+readLine' prompt = liftM (fromMaybe "") $ Haskeline.getInputLine prompt++printLine' :: String -> Console ()+printLine' s = liftIO $ putStrLn $ s+ #else++type Console = IO++runConsole :: Console a -> IO a runConsole m = bracket initialie (hSetBuffering stdout) (const m)   where     initialie = do       x <- hGetBuffering stdout       hSetBuffering stdout NoBuffering       return x-#endif  readLine' :: String -> Console String-#if defined(USE_READLINE_PACKAGE)-readLine' prompt = liftM (fromMaybe "") $ SLE.getLineEdited prompt-#elif defined(USE_HASKELINE_PACKAGE)-readLine' prompt = liftM (fromMaybe "") $ Haskeline.getInputLine prompt-#else readLine' prompt = putStr prompt >> getLine-#endif  printLine' :: String -> Console () printLine' s = liftIO $ putStrLn $ s +#endif+ ----------------------------------------------------------------------------  type UIState = Sys.System@@ -216,6 +257,23 @@            case find (\x -> CDT.functName x == name) objects of              Just obj -> printLines $ lines $ showObjectInfo obj              Nothing  -> throwError $ "unknown object: " ++ name+    ("function", arg') ->+        do sys <- get+           let name = strip arg'+           case Sys.getFunctionSignature sys name of+             Just (args, t) ->+               if null args+                 then printLines [name ++ ": " ++ show t]+                 else do+                   let lhs = name ++ "(" ++ intercalate "," (map fst args) ++ ")"+                       upper = intercalate "  " $ [p ++ ": " ++ show pt | (p,pt) <- args]+                       lower = lhs ++ ": " ++ show t+                   printLines+                     [ upper+                     , replicate (max (length upper) (length lower)) '-'+                     , lower+                     ]+             Nothing  -> throwError $ "unknown function: " ++ name     ("aexp", arg') -> do -- XXX       sys <- get       case Sys.parseExp sys (strip arg') of@@ -286,8 +344,41 @@               loop (zip [(0::Int)..] traces)  cmdLoad :: Command+#if defined(USE_WEB_BACKEND) cmdLoad s =-    do contents <- liftIO $ readFile filename+    do let filename = let s' = strip s in+                          case s' of+                          '"':_ -> read s'+                          _     -> s'+       result <- liftIO $ try $ evaluate =<< (fromJSString <$> js_loadFile (toJSString filename))+       case result of+         Left (JSException val) -> do+           s2 <- liftIO $ js_toString val+           throwError (fromJSString s2)+         Right contents -> do+           let src  = unlines (map removeComment (lines contents))+               cmds = split src+           forM_ cmds $ \cmd -> do+             printLines ["> " ++ l | l <- lines cmd]+             dispatchCommand cmd+    where removeComment []      = []+          removeComment ('#':_) = []+          removeComment (x:xs)  = x : removeComment xs+          split :: String -> [String]+          split s = map (strip . reverse) (f s [])+              where f (';':xs) tmp = tmp : (f xs [])+                    f (x:xs) tmp   = f xs (x:tmp)+                    f [] tmp       = [tmp]+#else+cmdLoad s =+    do result <- liftIO $ try $ do+         h <- openFile filename ReadMode+         hSetEncoding h utf8+         hGetContents h+       contents <-+         case result of+           Left (e :: SomeException) -> throwError (show e)+           Right contents -> return contents        let src  = unlines (map removeComment (lines contents))            cmds = split src        forM_ cmds $ \cmd -> do@@ -306,6 +397,7 @@               where f (';':xs) tmp = tmp : (f xs [])                     f (x:xs) tmp   = f xs (x:tmp)                     f [] tmp       = [tmp]+#endif  cmdEdit :: Command cmdEdit _ = loop >>= dispatchCommand@@ -319,18 +411,28 @@           return $ l ++ "\n" ++ s  cmdQuit :: Command+#if defined(USE_WEB_BACKEND)+cmdQuit _ = throwError ("'quit' is not supported on WebAssembly backend. Use 'reset' instead.")+#else cmdQuit _ = liftIO $ exitWith ExitSuccess+#endif  cmdHelp :: Command-cmdHelp _ = printLines +cmdHelp _ = printLines               [ "  exit                        exit the interpreter"               , "  quit                        ditto"               , "  bye                         ditto"               , "  edit                        enter editing mode"               , "  simp [full] <exp>           evaluate expression"               , "  show <exp>                  print type of expression"+              , "  show function <name>        print information of function"               , "  show object <functor>       print information of functor"+#if defined(USE_WEB_BACKEND)+              , "  load <filename>             load built-in sample file"+              , "  load                        open file picker"+#else               , "  load <filename>             load from file"+#endif               , "  set trace [on|off]          enable/disable trace"               , "  reset                       remove all definitions"               ]@@ -400,7 +502,7 @@          (_,_,errs) -> do            forM_ errs $ \err -> hPutStr stderr err            hPutStrLn stderr $ usageInfo header options-           exitFailure             +           exitFailure  header :: String header = "Usage: cpl [OPTION...] files..."
src/ParserUtils.hs view
@@ -6,7 +6,8 @@     , ident     ) where -import Text.ParserCombinators.Parsec+import Text.Parsec hiding (string')+import Text.Parsec.String (Parser) import Data.Char  type Ident = String
src/Simp.hs view
@@ -4,7 +4,7 @@ -- Module      :  Simp -- Copyright   :  (c) Masahiro Sakai 2004-2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -107,27 +107,27 @@     simp1 :: CompiledExp -> CompiledExp -> CompiledExp      simp1 Identity c = c --- IDENT-    +     simp1 (Comp a b) c = simp1 a (simp1 b c) --- COMP-    +     simp1 e@(LNat _) c = e `comp` c -- L-NAT     simp1 (RNat sym) c       | full = simp1_FULL_R_NAT sym c --- FULL-R-NAT       | otherwise = simp1_R_NAT sym c --- R-NAT-    +     simp1 (LFact _ _ table) c = --- L-FACT       case split c of       (LNat sym, c') -> simp1 (table ! (CDT.natIndex sym)) c'       _ -> impossible-    +     simp1 e@(RFact obj args) c       | full && CDT.isUnconditioned obj = simp1_FULL_C_FACT obj args c       | otherwise = e `comp` c -- R-FACT-    +     simp1 (Var _ e) c = simp1 e c-    +     -----------------------------------    +     simp1_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp     simp1_R_NAT sym c =       case simp2 c sym of@@ -137,7 +137,7 @@         else simp1 (subst1 factR (CDT.natDeclCod sym))                    (simp1 (args !! CDT.natIndex sym) c'')       _ -> impossible-    +     simp1_FULL_R_NAT :: CDT.Nat -> CompiledExp -> CompiledExp     simp1_FULL_R_NAT sym factP =         case pickupFactR sym factP of@@ -147,7 +147,7 @@             else simp1 (subst1 factR (CDT.natDeclCod sym))                        (simp1 (args !! CDT.natIndex sym) factP')         _ -> impossible-    +     simp1_FULL_C_FACT :: CDT.CDT -> [CompiledExp] -> CompiledExp -> CompiledExp     simp1_FULL_C_FACT obj args p = RFact obj (zipWith f args (CDT.nats obj))         {- 並列処理出来るのって、ここのzipWithくらいだろうか -}@@ -156,9 +156,9 @@             case CDT.natDeclDom nat of               FE.Var 0 -> simp1 e p               fe       -> e `comp` subst1 p fe -- ack(3,3)で16000回くらい-    +     -----------------------------------    +     simp2 :: CompiledExp -> CDT.Nat -> (CompiledExp, CompiledExp)     simp2 c sym = f (CDT.natProjectionSequence sym) c         where
src/Statement.hs view
@@ -3,7 +3,7 @@ -- Module      :  Statement -- Copyright   :  (c) Masahiro Sakai 2004,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable
src/Subst.hs view
@@ -4,10 +4,10 @@ -- Module      :  Subst -- Copyright   :  (c) Masahiro Sakai 2006,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional--- Portability :  +-- Portability : -- -- Based on "Typing Haskell in Haskell". -- http://www.cse.ogi.edu/~mpj/thih/@@ -92,7 +92,7 @@        s2 <- matchList (apply s1 as) (apply s1 bs)        return (s2 @@ s1) matchList [] [] = return nullSubst-matchList _ _   = throwError "types do not unify"    +matchList _ _   = throwError "types do not unify"  varBind :: MonadError String m => VarId -> FE -> m Subst varBind u t | t == Var u    = return nullSubst
src/Type.hs view
@@ -4,7 +4,7 @@ -- Module      :  Type -- Copyright   :  (c) Masahiro Sakai 2006,2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable
src/Variance.hs view
@@ -1,10 +1,9 @@-{-# LANGUAGE CPP #-} ----------------------------------------------------------------------------- -- | -- Module      :  Variance -- Copyright   :  (c) Masahiro Sakai 2009 -- License     :  BSD-style--- +-- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional -- Portability :  portable@@ -25,9 +24,7 @@     , mnemonic     ) where -#if __GLASGOW_HASKELL__ >= 706 import Prelude hiding (join)-#endif  data Variance     = Covariance     --- +
+ web/README.md view
@@ -0,0 +1,356 @@+# CPL WebAssembly Edition++This directory contains the source files for the WebAssembly version of the CPL (Categorical Programming Language) interpreter.++Build outputs go to the `_site/` directory in the project root.++## Try Online++Visit https://msakai.github.io/cpl/ and start using CPL immediately!++### Commands to Try++```+cpl> edit+| right object 1 with !+| end object;+right object 1 defined+cpl> edit+| right object prod(a,b) with pair is+|   pi1: prod -> a+|   pi2: prod -> b+| end object;+right object prod(+,+) defined+cpl> edit+| right object exp(a,b) with curry is+|   eval: prod(exp,a) -> b+| end object;+right object exp(-,+) defined+cpl> edit+| left object nat with pr is+|   0: 1 -> nat+|   s: nat -> nat+| end object;+left object nat defined+cpl> show pair(pi2,eval)+pair(pi2,eval)+    : prod(exp(*a,*b),*a) -> prod(*a,*b)+cpl> let add=eval.prod(pr(curry(pi2), curry(s.eval)), I)+add : prod(nat,nat) -> nat  defined+cpl> simp add.pair(s.s.0, s.0)+s.s.s.0+    : 1 -> nat+```++## Files++### Source files (in this directory)++- **index.html** - Web interface with xterm.js terminal emulator+- **cpl-terminal.js** - JavaScript terminal controller and WASM loader+- **tutorial.css** - Stylesheet for tutorial pages++### Generated files (in `_site/`)++The build process outputs the following files to `_site/`:++- **cpl.wasm** - Compiled CPL interpreter+- **cpl.js** - JavaScript glue module (generated by post-link processing)+- **samples.js** - Sample files module+- Plus copies of the source files above++## Building++The WASM binary is built using GHC's WebAssembly backend. To build it yourself:++```bash+# From the project root+./scripts/build-wasm.sh+```++### Prerequisites++Install GHC WebAssembly cross-compiler (GHC 9.10.3 or later):++```bash+curl https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta/-/raw/master/bootstrap.sh | sh+source ~/.ghc-wasm/env+```++This provides `wasm32-wasi-ghc` and `wasm32-wasi-cabal` in `PATH`.++Build configuration:++```bash+wasm32-wasi-cabal configure -fWeb -f-Haskeline+```++To clean and rebuild:++```bash+./scripts/build-wasm.sh --clean+```++## Testing Locally++To test the WASM version locally:++```bash+# Build WASM and web files+./scripts/build-wasm.sh++# Optionally build tutorial pages+./scripts/build-tutorial.sh++# Start local server+python3 -m http.server -d _site 8000+```++Then open http://localhost:8000 in your browser.++## Deployment++### Automatic Deployment++- **Trigger:** Push to `master` branch+- **Build trigger:** Also runs on tags, pull requests, and manual dispatch (build only, no deploy)+- **Workflow:** `.github/workflows/wasm-deploy.yaml`+- **Destination:** GitHub Pages (https://msakai.github.io/cpl/)+- **Artifacts:** `cpl.wasm`, `cpl.js`, `index.html`, `cpl-terminal.js`, `samples.js`++### Manual Deployment++```bash+# Build WASM and tutorial pages+./scripts/build-wasm.sh+./scripts/build-tutorial.sh++# Deploy files from _site/ directory to your web server+```++## Browser Compatibility++Tested and working on:+- Chrome/Chromium 90++- Firefox 90++- Safari 15++- Edge 90+++## Architecture++```+Browser+  ├── xterm.js (terminal UI)+  └── cpl-terminal.js (FFI bridge)+       └── cpl.wasm (CPL interpreter)+            └── Haskell runtime+```++### Console Abstraction++The Haskell code uses CPP macros to conditionally compile different Console implementations, allowing the same codebase to support multiple backends:++```haskell+#if defined(USE_WEB_BACKEND)+  -- JavaScript FFI implementation (GHC.Wasm.Prim / JSString)+#elif defined(USE_HASKELINE_PACKAGE)+  -- Haskeline implementation+#else+  -- Plain IO implementation+#endif+```++For WASM, four JavaScript FFI functions are exposed:+- `terminal_initialize()` - Initialize xterm.js terminal+- `terminal_printLine(text)` - Print a line to terminal+- `terminal_readLine(prompt)` - Read user input (async)+- `terminal_loadFile(filename)` - Load a file by name or open file picker++### JavaScript FFI Flow++1. **Haskell declares FFI imports/exports** in `src/Main.hs`:+   ```haskell+   foreign import javascript "terminal_readLine($1)"+     js_readLine :: JSString -> IO JSString++   foreign import javascript "terminal_loadFile($1)"+     js_loadFile :: JSString -> IO JSString++   foreign export javascript "hs_start" main :: IO ()+   ```++2. **JavaScript implements FFI functions** in `cpl-terminal.js`:+   ```javascript+   window.terminal_readLine = async (jsVal) => {+     const prompt = String(jsVal);+     const result = await cplTerminal.readLine(prompt);+     return result;+   };++   window.terminal_loadFile = async (jsVal) => {+     const filename = String(jsVal).trim();+     if (filename) {+       // Look up built-in sample files+       if (sampleFiles[filename] !== undefined) {+         return sampleFiles[filename];+       }+       throw new Error(`File not found: ${filename}`);+     }+     // No filename: open file picker dialog+     ...+   };+   ```++3. **JSFFI glue code (`cpl.js`) connects them** at instantiation using a knot-tying pattern:+   ```javascript+   const jsffiModule = await import('./cpl.js');+   const __exports = {};+   const jsffi = jsffiModule.default(__exports);++   const { instance } = await WebAssembly.instantiate(wasmBytes, {+     ghc_wasm_jsffi: jsffi,+     wasi_snapshot_preview1: wasi.wasiImport,+   });+   Object.assign(__exports, instance.exports);+   ```++### WASI Integration++The browser environment requires a WASI shim (`@bjorn3/browser_wasi_shim`) to satisfy the WASI snapshot preview1 imports that GHC's WASM backend emits:++```javascript+import { WASI, OpenFile, File, ConsoleStdout } from '@bjorn3/browser_wasi_shim';++const fds = [+  new OpenFile(new File([])),                                       // stdin+  ConsoleStdout.lineBuffered(msg => console.log(`[CPL] ${msg}`)),   // stdout+  ConsoleStdout.lineBuffered(msg => console.warn(`[CPL] ${msg}`)),  // stderr+];+const wasi = new WASI([], [], fds);+```++The WASI reactor is initialized before the Haskell RTS:++```javascript+wasi.initialize(instance);   // calls _initialize+instance.exports.hs_init();  // init Haskell RTS+instance.exports.hs_start(); // run main (exported via foreign export)+```++### JavaScript Side (cpl-terminal.js)++The JavaScript side provides:+- **CPLTerminal class** - Manages xterm.js terminal instance+- **Keyboard handling** - Enter, Backspace, Ctrl+C, Ctrl+D, Tab+- **WASM loading** - Fetches and instantiates WASM module+- **FFI bindings** - Connects Haskell to JavaScript++### Build Configuration (CPL.cabal)++The WASM flag in CPL.cabal enables WebAssembly-specific build options:++```cabal+Flag Web+  Description: Build for browser environment with WebAssembly + JavaScript FFI+  Default: False+  Manual: True+```++When enabled:+- Sets `-DUSE_WEB_BACKEND` CPP flag+- Uses `-no-hs-main` (no standard main entry point)+- Exports `hs_init` and `hs_start` symbols+- Enables `JavaScriptFFI` extension for GHC 9.10++- Adds `ghc-experimental` dependency for `GHC.Wasm.Prim`++### Post-link Processing++GHC's WASM backend generates a `post-link.mjs` tool that extracts JSFFI information from the compiled `.wasm` binary and produces a JavaScript glue module (`cpl.js`). This glue code implements the knot-tying pattern required for bidirectional FFI:++```bash+node "$LIBDIR/post-link.mjs" -i _site/cpl.wasm -o _site/cpl.js+```++### Build Systems++Two parallel build systems are maintained:++1. **Stack** (for native builds)+   - Uses `stack.yaml`+   - Default for development+   - Supports haskeline++2. **Cabal** (for both native and WASM builds)+   - Uses `CPL.cabal` with flags+   - WASM builds: `wasm32-wasi-cabal configure -fWeb`+   - Native builds: `cabal configure`++## Known Limitations++- **Command history** - Basic line editing only+- **Tab completion** - Not implemented+- **Multi-line paste** - May have issues with large pastes++These features may be added in future versions.++## Troubleshooting++### WASM module fails to load++Check browser console for errors. Common issues:+- Missing or incorrect MIME type for `.wasm` files+- CORS issues (must serve from web server, not `file://`)+- Browser doesn't support WebAssembly++### Terminal not responding++- Ensure JavaScript is enabled+- Check browser console for errors+- Try refreshing the page++### Build errors++If `./scripts/build-wasm.sh` fails:+- Verify GHC WASM toolchain is installed correctly+- Check that `wasm32-wasi-ghc` and `wasm32-wasi-cabal` are in `PATH`+- Try `./scripts/build-wasm.sh --clean` to clean build artifacts++## Performance++The WASM version has similar performance to the native version for most operations, with slight overhead for JavaScript-Haskell FFI calls.++### Binary Size+- ~2.9 MB (includes GHC runtime system, libraries, and CPL interpreter)++### Load Time+- First load depends on network speed and browser WASM compilation+- Subsequent loads are faster due to browser caching++## Security++The WASM version runs in the browser's sandbox and has no access to:+- Local file system (except via the browser file picker dialog triggered by `load` with no arguments)+- Network (except for loading the WASM module itself)+- Other tabs or browser state++This makes it safe to run untrusted CPL programs in the browser.++## Contributing++To improve the WASM version:++1. Modify Haskell code in `src/Main.hs` (USE_WEB_BACKEND section)+2. Update JavaScript in `web/cpl-terminal.js`+3. Build and test locally with `./scripts/build-wasm.sh && python3 -m http.server -d _site 8000`+4. Submit pull request++See main README.md for general contribution guidelines.++## References++- [GHC WebAssembly Backend User's Guide](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/wasm.html)+- [ghc-wasm-meta](https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta) - GHC WASM toolchain bootstrap+- [xterm.js Documentation](https://xtermjs.org/)+- [@bjorn3/browser_wasi_shim](https://github.com/aspect-build/aspect-cli/tree/main/aspect-build/aspect-cli) - WASI shim for browsers+- [GitHub Pages Documentation](https://docs.github.com/pages)+- Tatsuya Hagino, "A Categorical Programming Language", PhD Thesis, University of Edinburgh, 1987
+ web/apple-touch-icon.png view

binary file changed (absent → 30277 bytes)

+ web/cpl-terminal.js view
@@ -0,0 +1,332 @@+import { Terminal } from 'https://cdn.jsdelivr.net/npm/xterm@5.3.0/+esm';+import { FitAddon } from 'https://cdn.jsdelivr.net/npm/xterm-addon-fit@0.8.0/+esm';+import { WASI, OpenFile, File, ConsoleStdout } from 'https://cdn.jsdelivr.net/npm/@bjorn3/browser_wasi_shim@0.3.0/+esm';+import { sampleFiles } from './samples.js';++/**+ * CPL Terminal Manager+ * Manages xterm.js terminal and provides interface for WASM CPL interpreter+ */+class CPLTerminal {+  constructor() {+    this.term = new Terminal({+      cursorBlink: true,+      fontSize: 14,+      fontFamily: 'Menlo, Monaco, "Courier New", monospace',+      theme: {+        background: '#1e1e1e',+        foreground: '#d4d4d4',+        cursor: '#00ff00',+        cursorAccent: '#1e1e1e',+        selection: 'rgba(255, 255, 255, 0.3)',+        black: '#000000',+        red: '#cd3131',+        green: '#0dbc79',+        yellow: '#e5e510',+        blue: '#2472c8',+        magenta: '#bc3fbc',+        cyan: '#11a8cd',+        white: '#e5e5e5',+        brightBlack: '#666666',+        brightRed: '#f14c4c',+        brightGreen: '#23d18b',+        brightYellow: '#f5f543',+        brightBlue: '#3b8eea',+        brightMagenta: '#d670d6',+        brightCyan: '#29b8db',+        brightWhite: '#e5e5e5'+      },+      allowProposedApi: true+    });++    this.fitAddon = new FitAddon();+    this.term.loadAddon(this.fitAddon);++    this.inputBuffer = '';+    this.resolveInput = null;+    this.isInitialized = false;+  }++  /**+   * Initialize terminal and attach event handlers+   */+  initialize() {+    if (this.isInitialized) return;++    const terminalElement = document.getElementById('terminal');+    if (!terminalElement) {+      throw new Error('Terminal element not found');+    }++    this.term.open(terminalElement);+    this.fitAddon.fit();++    // Handle window resize+    window.addEventListener('resize', () => {+      this.fitAddon.fit();+    });++    // Handle keyboard input+    this.term.onData(data => {+      this.handleInput(data);+    });++    this.isInitialized = true;+  }++  /**+   * Handle keyboard input+   * @param {string} data - Input character(s)+   */+  handleInput(data) {+    const code = data.charCodeAt(0);++    // Enter key+    if (code === 13) {+      if (this.resolveInput) {+        const input = this.inputBuffer;+        this.inputBuffer = '';+        this.term.write('\r\n');+        this.resolveInput(input);+        this.resolveInput = null;+      }+      return;+    }++    // Backspace (127) or Ctrl+H (8)+    if (code === 127 || code === 8) {+      if (this.inputBuffer.length > 0) {+        this.inputBuffer = this.inputBuffer.slice(0, -1);+        // Move cursor back, write space, move cursor back again+        this.term.write('\b \b');+      }+      return;+    }++    // Ctrl+C+    if (code === 3) {+      this.term.write('^C\r\n');+      if (this.resolveInput) {+        this.inputBuffer = '';+        this.resolveInput('');+        this.resolveInput = null;+      }+      return;+    }++    // Ctrl+D (EOF)+    if (code === 4) {+      this.term.write('^D\r\n');+      if (this.resolveInput && this.inputBuffer.length === 0) {+        this.resolveInput('quit');+        this.resolveInput = null;+      }+      return;+    }++    // Printable characters (including space)+    if (code >= 32 && code < 127) {+      this.inputBuffer += data;+      this.term.write(data);+      return;+    }++    // Tab key+    if (code === 9) {+      // For now, just insert spaces (future: implement completion)+      const spaces = '  ';+      this.inputBuffer += spaces;+      this.term.write(spaces);+      return;+    }+  }++  /**+   * Print a line to the terminal+   * @param {string} text - Text to print+   */+  printLine(text) {+    // Convert JavaScript string to lines and print each+    const lines = text.split('\n');+    for (let i = 0; i < lines.length; i++) {+      if (i > 0) this.term.write('\r\n');+      this.term.write(lines[i]);+    }+    this.term.write('\r\n');+  }++  /**+   * Read a line from the terminal (async)+   * @param {string} prompt - Prompt to display+   * @returns {Promise<string>} The input line+   */+  async readLine(prompt) {+    return new Promise(resolve => {+      this.term.write(prompt);+      this.resolveInput = resolve;+    });+  }++  /**+   * Write text without newline+   * @param {string} text - Text to write+   */+  write(text) {+    this.term.write(text);+  }++  /**+   * Clear the terminal+   */+  clear() {+    this.term.clear();+  }+}++// Global terminal instance+const cplTerminal = new CPLTerminal();++// WASM FFI exports - these will be called from Haskell+window.terminal_initialize = () => {+  cplTerminal.initialize();+};++window.terminal_printLine = (jsVal) => {+  // Convert JSVal to string+  const text = String(jsVal);+  cplTerminal.printLine(text);+};++window.terminal_readLine = async (jsVal) => {+  // Convert JSVal to string for prompt+  const prompt = String(jsVal);+  const result = await cplTerminal.readLine(prompt);+  return result;+};++window.terminal_loadFile = async (jsVal) => {+  const filename = String(jsVal).trim();++  // 1. Filename specified: look up built-in sample+  if (filename) {+    if (sampleFiles[filename] !== undefined) {+      return sampleFiles[filename];+    }+    // Not found: show available files+    const available = Object.keys(sampleFiles).join(', ');+    throw new Error(+      `File not found: ${filename}\n` ++      `Available files: ${available}\n` ++      `Type 'load' with no arguments to open a file picker.`+    );+  }++  // 2. No filename: open file picker+  return new Promise((resolve, reject) => {+    const input = document.createElement('input');+    input.type = 'file';+    input.accept = '.cpl,.cdt,.txt';+    input.style.display = 'none';+    document.body.appendChild(input);+    input.addEventListener('change', async () => {+      document.body.removeChild(input);+      const file = input.files[0];+      if (file) {+        resolve(await file.text());+      } else {+        reject(new Error('No file selected'));+      }+    });+    input.addEventListener('cancel', () => {+      document.body.removeChild(input);+      reject(new Error('File selection cancelled'));+    });+    input.click();+  });+};++/**+ * Show error message+ */+function showError(message, details) {+  const loadingEl = document.getElementById('loading');+  loadingEl.className = 'error';+  loadingEl.innerHTML = `+    <div class="error-title">Failed to load CPL interpreter</div>+    <div>${message}</div>+    ${details ? `<pre style="margin-top: 1rem; text-align: left;">${details}</pre>` : ''}+  `;+}++/**+ * Initialize and load WASM module+ */+async function initCPL() {+  const loadingEl = document.getElementById('loading');+  const terminalContainer = document.getElementById('terminal-container');++  try {+    loadingEl.textContent = 'Downloading WASM module...';++    // Fetch WASM binary+    const response = await fetch('cpl.wasm');+    if (!response.ok) {+      throw new Error(`Failed to fetch cpl.wasm: ${response.status} ${response.statusText}`);+    }++    loadingEl.textContent = 'Loading WASM module...';++    const wasmBytes = await response.arrayBuffer();++    loadingEl.textContent = 'Initializing CPL interpreter...';++    // Import JSFFI glue code generated by post-link.mjs+    const jsffiModule = await import('./cpl.js');++    // Knot-tying: create empty exports object, fill after instantiation+    const __exports = {};+    const jsffi = jsffiModule.default(__exports);++    // Set up WASI shim for browser+    const fds = [+      new OpenFile(new File([])),                                       // stdin+      ConsoleStdout.lineBuffered(msg => console.log(`[CPL] ${msg}`)),   // stdout+      ConsoleStdout.lineBuffered(msg => console.warn(`[CPL] ${msg}`)),  // stderr+    ];+    const wasi = new WASI([], [], fds);++    // Instantiate WASM with JSFFI + WASI imports+    const { instance } = await WebAssembly.instantiate(wasmBytes, {+      ghc_wasm_jsffi: jsffi,+      wasi_snapshot_preview1: wasi.wasiImport,+    });++    // Complete knot-tying: fill in exports+    Object.assign(__exports, instance.exports);++    // Initialize WASI reactor (sets wasi.inst and calls _initialize)+    wasi.initialize(instance);++    // Hide loading indicator and show terminal+    loadingEl.classList.add('hidden');+    terminalContainer.style.display = 'block';++    // Initialize Haskell RTS and start REPL+    instance.exports.hs_init();+    instance.exports.hs_start();++  } catch (error) {+    console.error('CPL initialization error:', error);+    showError(+      error.message || 'An unknown error occurred',+      error.stack+    );+  }+}++// Start initialization when DOM is ready+if (document.readyState === 'loading') {+  document.addEventListener('DOMContentLoaded', initCPL);+} else {+  initCPL();+}
+ web/favicon-16x16.png view

binary file changed (absent → 765 bytes)

+ web/favicon-32x32.png view

binary file changed (absent → 1469 bytes)

+ web/favicon.ico view

binary file changed (absent → 5686 bytes)

+ web/favicon_header.html view
@@ -0,0 +1,6 @@+<link rel="icon" type="image/x-icon" href="favicon.ico">+<link rel="icon" type="image/png" sizes="32x32" href="favicon-32x32.png">+<link rel="icon" type="image/png" sizes="16x16" href="favicon-16x16.png">+<link rel="apple-touch-icon" sizes="180x180" href="apple-touch-icon.png">+<link rel="manifest" href="manifest.json">+<meta name="theme-color" content="#4ec9b0">
+ web/icon-192x192.png view

binary file changed (absent → 33251 bytes)

+ web/icon-512x512.png view

binary file changed (absent → 176330 bytes)

+ web/index.html view
@@ -0,0 +1,216 @@+<!DOCTYPE html>+<html lang="en">+<head>+  <meta charset="UTF-8">+  <meta name="viewport" content="width=device-width, initial-scale=1.0">+  <title>CPL - Categorical Programming Language</title>+  <link rel="icon" type="image/x-icon" href="favicon.ico">+  <link rel="icon" type="image/png" sizes="32x32" href="favicon-32x32.png">+  <link rel="icon" type="image/png" sizes="16x16" href="favicon-16x16.png">+  <link rel="apple-touch-icon" sizes="180x180" href="apple-touch-icon.png">+  <link rel="manifest" href="manifest.json">+  <meta name="theme-color" content="#4ec9b0">+  <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/xterm@5.3.0/css/xterm.css">+  <style>+    :root {+      --color-primary: #4ec9b0;+      --color-primary-dim: rgba(78, 201, 176, 0.3);+      --color-bg: #1e1e1e;+      --color-bg-elevated: #2a2a2a;+      --color-border: #333;+      --color-text: #d4d4d4;+      --color-text-muted: #888;+      --color-text-subtle: #666;+      --color-error: #d32f2f;+      --color-error-bg: #5a1e1e;+      --color-error-text: #ff6b6b;+    }++    * {+      box-sizing: border-box;+    }++    body {+      margin: 0;+      padding: 20px;+      font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, 'Helvetica Neue', Arial, sans-serif;+      background: var(--color-bg);+      color: var(--color-text);+      line-height: 1.6;+    }++    .container {+      max-width: 1200px;+      margin: 0 auto;+    }++    header {+      text-align: center;+      margin-bottom: 2rem;+      padding-bottom: 1rem;+      border-bottom: 2px solid var(--color-border);+    }++    h1 {+      margin: 0 0 0.5rem 0;+      font-size: 2rem;+      color: var(--color-primary);+    }++    a {+      color: var(--color-primary);+      text-decoration: none;+    }++    a:hover {+      text-decoration: underline;+    }++    .subtitle {+      font-size: 1rem;+      color: var(--color-text-muted);+      margin: 0;+    }++    #terminal-container {+      background: var(--color-bg);+      border: 1px solid var(--color-border);+      border-radius: 8px;+      padding: 1rem;+      box-shadow: 0 4px 6px rgba(0, 0, 0, 0.3);+    }++    #terminal {+      height: 600px;+    }++    #loading {+      text-align: center;+      padding: 2rem;+      font-size: 1.1rem;+      color: var(--color-primary);+    }++    #loading.hidden {+      display: none;+    }++    .spinner {+      display: inline-block;+      width: 20px;+      height: 20px;+      border: 3px solid var(--color-primary-dim);+      border-radius: 50%;+      border-top-color: var(--color-primary);+      animation: spin 1s ease-in-out infinite;+      margin-right: 0.5rem;+      vertical-align: middle;+    }++    @keyframes spin {+      to { transform: rotate(360deg); }+    }++    .error {+      background: var(--color-error-bg);+      border: 1px solid var(--color-error);+      border-radius: 4px;+      padding: 1rem;+      margin-top: 1rem;+      color: var(--color-error-text);+    }++    .error-title {+      font-weight: bold;+      margin-bottom: 0.5rem;+    }++    .info {+      background: var(--color-bg-elevated);+      border: 1px solid var(--color-primary);+      border-radius: 4px;+      padding: 1rem;+      margin-top: 1rem;+      font-size: 0.9rem;+    }++    .info h3 {+      margin-top: 0;+      color: var(--color-primary);+      font-size: 1rem;+    }++    .info ul {+      margin: 0.5rem 0;+      padding-left: 1.5rem;+    }++    .info code {+      background: var(--color-border);+      padding: 0.2rem 0.4rem;+      border-radius: 3px;+      font-family: 'Courier New', monospace;+    }++    .info-cta {+      margin-top: 1.5rem;+      text-align: center;+      font-size: 1rem;+    }++    footer {+      text-align: center;+      margin-top: 2rem;+      padding-top: 1rem;+      border-top: 1px solid var(--color-border);+      color: var(--color-text-subtle);+      font-size: 0.9rem;+    }+  </style>+</head>+<body>+  <div class="container">+    <header>+      <h1>CPL - Categorical Programming Language</h1>+      <p class="subtitle">WebAssembly Edition</p>+    </header>++    <div id="loading">+      <div class="spinner"></div>+      Loading CPL interpreter...+    </div>++    <div id="terminal-container" style="display: none;">+      <div id="terminal"></div>+    </div>++    <div class="info">+      <h3>Quick Start</h3>+      <p>Try these commands in the terminal:</p>+      <ul>+        <li><code>help</code> - Show all available commands</li>+        <li><code>load samples/examples.cpl</code> - Load a built-in sample file demonstrating common data types and functions</li>+        <li><code>load</code> - Open file picker to load a local file</li>+        <li><code>edit</code> - Enter multi-line editing mode (end with semicolon)</li>+        <li><code>simp pi1.pair(0, s.0)</code> - Evaluate an expression</li>+        <li><code>let uncurry(f) = eval . prod(f, I)</code> - Define a function</li>+        <li><code>reset</code> - Reset all definitions</li>+      </ul>+      <p class="info-cta">+        📚 <strong>New to CPL?</strong> Check out the+        <a href="tutorial.html">Tutorial (English)</a> |+        <a href="tutorial_ja.html">チュートリアル (日本語)</a>+      </p>+    </div>++    <footer>+      <p>+        CPL Implementation by Masahiro Sakai |+        <a href="https://github.com/msakai/cpl" target="_blank">GitHub Repository</a>+      </p>+    </footer>+  </div>++  <script type="module" src="cpl-terminal.js"></script>+</body>+</html>
+ web/manifest.json view
@@ -0,0 +1,33 @@+{+  "name": "CPL - Categorical Programming Language",+  "short_name": "CPL",+  "description": "WebAssembly-based interpreter for the Categorical Programming Language",+  "start_url": ".",+  "display": "standalone",+  "background_color": "#1e1e1e",+  "theme_color": "#4ec9b0",+  "icons": [+    {+      "src": "favicon-16x16.png",+      "sizes": "16x16",+      "type": "image/png"+    },+    {+      "src": "favicon-32x32.png",+      "sizes": "32x32",+      "type": "image/png"+    },+    {+      "src": "icon-192x192.png",+      "sizes": "192x192",+      "type": "image/png",+      "purpose": "maskable"+    },+    {+      "src": "icon-512x512.png",+      "sizes": "512x512",+      "type": "image/png",+      "purpose": "maskable"+    }+  ]+}
+ web/tutorial.css view
@@ -0,0 +1,364 @@+/* Tutorial page styles - matching the CPL WASM terminal dark theme */++:root {+  --color-primary: #4ec9b0;+  --color-bg: #1e1e1e;+  --color-bg-elevated: #2a2a2a;+  --color-bg-alt: #252525;+  --color-border: #333;+  --color-text: #d4d4d4;+  --color-text-muted: #888;+  --color-code: #ce9178;+}++* {+  box-sizing: border-box;+}++body {+  margin: 0;+  padding: 20px;+  font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, 'Helvetica Neue', Arial, sans-serif;+  background: var(--color-bg);+  color: var(--color-text);+  line-height: 1.8;+  font-size: 16px;+}++/* Navigation header */+.nav-header {+  background: var(--color-bg-elevated);+  border-bottom: 2px solid var(--color-primary);+  padding: 1rem;+  margin: -20px -20px 2rem -20px;+  text-align: center;+  font-size: 0.9rem;+  max-width: none; /* Override body > * rule */+}++.nav-header a {+  color: var(--color-primary);+  text-decoration: none;+  margin: 0 0.5rem;+}++.nav-header a:hover {+  text-decoration: underline;+}++/* Main content container */+#TOC {+  background: var(--color-bg-elevated);+  border: 1px solid var(--color-primary);+  border-radius: 8px;+  padding: 1.5rem;+  margin: 0 auto 2rem auto;+  max-width: 900px;+}++#TOC > ul {+  margin: 0;+  padding-left: 1.5rem;+}++#TOC a {+  color: var(--color-primary);+  text-decoration: none;+}++#TOC a:hover {+  text-decoration: underline;+}++/* Headings */+h1, h2, h3, h4, h5, h6 {+  color: var(--color-primary);+  margin-top: 2rem;+  margin-bottom: 1rem;+  line-height: 1.3;+}++h1 {+  font-size: 2.5rem;+  border-bottom: 2px solid var(--color-primary);+  padding-bottom: 0.5rem;+  margin-top: 0;+  text-align: center;+}++h2 {+  font-size: 2rem;+  border-bottom: 1px solid var(--color-border);+  padding-bottom: 0.5rem;+}++h3 {+  font-size: 1.5rem;+}++h4 {+  font-size: 1.2rem;+  color: var(--color-text);+}++/* Links */+a {+  color: var(--color-primary);+  text-decoration: none;+}++a:hover {+  text-decoration: underline;+}++/* Override Pandoc's default div.sourceCode { margin: 1em 0 } which+   resets margin-left/right to 0 and breaks the body > * centering+   due to higher specificity (class selector beats universal selector). */+div.sourceCode {+  max-width: 900px;+  margin: 1em auto;+}++/* Code blocks and inline code */+code {+  background: var(--color-bg-elevated);+  padding: 0.2rem 0.4rem;+  border-radius: 3px;+  font-family: 'Courier New', Consolas, Monaco, monospace;+  font-size: 0.9em;+  color: var(--color-code);+}++pre {+  background: var(--color-bg-elevated);+  border: 1px solid var(--color-border);+  border-radius: 8px;+  padding: 1rem;+  overflow-x: auto;+  line-height: 1.5;+}++pre code {+  background: transparent;+  padding: 0;+  color: var(--color-text);+  font-size: 0.95em;+}++/* Blockquotes */+blockquote {+  border-left: 4px solid var(--color-primary);+  padding-left: 1rem;+  margin-left: 0;+  color: var(--color-text-muted);+  font-style: italic;+}++/* Lists */+ul, ol {+  margin: 1rem 0;+  padding-left: 2rem;+}++li {+  margin: 0.5rem 0;+}++/* Images */+img {+  max-width: 100%;+  height: auto;+  display: block;+  margin: 2rem auto;+  border: 1px solid var(--color-border);+  border-radius: 8px;+  background: white;+  padding: 1rem;+}++/* Tables */+table {+  border-collapse: collapse;+  width: 100%;+  margin: 1.5rem 0;+}++th, td {+  border: 1px solid var(--color-border);+  padding: 0.75rem;+  text-align: left;+}++th {+  background: var(--color-bg-elevated);+  color: var(--color-primary);+  font-weight: bold;+}++tr:nth-child(even) {+  background: var(--color-bg-alt);+}++/* Horizontal rule */+hr {+  border: none;+  border-top: 1px solid var(--color-border);+  margin: 2rem 0;+}++/* Paragraphs */+p {+  margin: 1rem 0;+}++/* Main content wrapper */+body > * {+  max-width: 900px;+  margin-left: auto;+  margin-right: auto;+}++/* Definition lists */+dt {+  font-weight: bold;+  color: var(--color-primary);+  margin-top: 1rem;+}++dd {+  margin-left: 2rem;+  margin-bottom: 1rem;+}++/* Syntax highlighting colors for dark theme+   (override Pandoc's default light-theme colors) */+code span.al { color: #ff6b6b; font-weight: bold; } /* Alert */+code span.an { color: #7ec8e3; font-weight: bold; font-style: italic; } /* Annotation */+code span.at { color: #c9d05c; } /* Attribute */+code span.bn { color: #b5cea8; } /* BaseN */+code span.bu { color: #4ec9b0; } /* BuiltIn */+code span.cf { color: #c586c0; font-weight: bold; } /* ControlFlow */+code span.ch { color: #ce9178; } /* Char */+code span.cn { color: #d19a66; } /* Constant */+code span.co { color: #6a9955; font-style: italic; } /* Comment */+code span.cv { color: #6a9955; font-weight: bold; font-style: italic; } /* CommentVar */+code span.do { color: #6a9955; font-style: italic; } /* Documentation */+code span.dt { color: #4ec9b0; } /* DataType */+code span.dv { color: #b5cea8; } /* DecVal */+code span.er { color: #ff6b6b; font-weight: bold; } /* Error */+code span.ex { color: #dcdcaa; } /* Extension */+code span.fl { color: #b5cea8; } /* Float */+code span.fu { color: #dcdcaa; } /* Function */+code span.im { color: #c586c0; font-weight: bold; } /* Import */+code span.in { color: #7ec8e3; font-weight: bold; font-style: italic; } /* Information */+code span.kw { color: #569cd6; font-weight: bold; } /* Keyword */+code span.op { color: #d4d4d4; } /* Operator */+code span.ot { color: #9cdcfe; } /* Other */+code span.pp { color: #c586c0; } /* Preprocessor */+code span.sc { color: #d7ba7d; } /* SpecialChar */+code span.ss { color: #ce9178; } /* SpecialString */+code span.st { color: #ce9178; } /* String */+code span.va { color: #9cdcfe; } /* Variable */+code span.vs { color: #ce9178; } /* VerbatimString */+code span.wa { color: #d19a66; font-weight: bold; font-style: italic; } /* Warning */++/* Responsive design */+@media (max-width: 768px) {+  body {+    padding: 10px;+    font-size: 14px;+  }++  h1 {+    font-size: 2rem;+  }++  h2 {+    font-size: 1.5rem;+  }++  h3 {+    font-size: 1.2rem;+  }++  pre {+    padding: 0.75rem;+    font-size: 0.85em;+  }++  #TOC {+    padding: 1rem;+  }+}++/* Print styles */+@media print {+  body {+    background: white;+    color: black;+  }++  .nav-header {+    display: none;+  }++  a {+    color: #0066cc;+  }++  /* Table of contents */+  #TOC {+    background: white;+    border: 1px solid #ccc;+  }++  #TOC a {+    color: #0066cc;+  }++  /* Code blocks */+  pre {+    background: #f5f5f5;+    border: 1px solid #ccc;+  }++  code {+    background: #f5f5f5;+    color: black;+  }++  pre code {+    background: transparent;+    border: none;+    color: black;+  }++  /* Reset syntax highlighting colors for print */+  code span.al, code span.an, code span.at, code span.bn,+  code span.bu, code span.cf, code span.ch, code span.cn,+  code span.co, code span.cv, code span.do, code span.dt,+  code span.dv, code span.er, code span.ex, code span.fl,+  code span.fu, code span.im, code span.in, code span.kw,+  code span.op, code span.ot, code span.pp, code span.sc,+  code span.ss, code span.st, code span.va, code span.vs,+  code span.wa {+    color: black;+    font-weight: normal;+    font-style: normal;+  }++  /* Tables */+  th {+    background: #f5f5f5;+    color: black;+  }++  tr:nth-child(even) {+    background: white;+  }++  /* Headings */+  h1, h2, h3, h4, h5, h6 {+    color: black;+  }+}
+ web/tutorial_header.txt view
@@ -0,0 +1,5 @@+<div class="nav-header">+  <a href="index.html">← Back to CPL WASM</a> | +  <a href="tutorial_ja.html">日本語版</a> | +  <a href="https://github.com/msakai/cpl">GitHub</a>+</div>
+ web/tutorial_ja_header.txt view
@@ -0,0 +1,5 @@+<div class="nav-header">+  <a href="index.html">← CPL WASM に戻る</a> | +  <a href="tutorial.html">English</a> | +  <a href="https://github.com/msakai/cpl">GitHub</a>+</div>