SAKAI Masahiro - CPL Diff

= A Categorical Programming Language

CPLは萩野先生の作ったプログラミング言語で、
((<圏論>))に基づいたデータ型の定義と計算モデルを持ちます。
詳しくは((<URL:http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en>))から入手できる論文を参照してください。

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.

For detail, see Hagino's Ph.D thesis available at ((<URL:http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en>)).

== Examples

こんな言語。

   right object 1 with !
   end object;
  
   right object prod(a,b) with pair is
     pi1: prod -> a
     pi2: prod -> b
   end object;
  
   right object exp(a,b) with curry is
     ev: prod(exp,a) -> b
   end object;
  
   left object nat with pr is
     zero: 1 -> nat
     succ: nat -> nat
   end object;
  
   left object coprod(a,b) with case is
     in1: a -> coprod
     in2: b -> coprod
   end object;
  
   let add = ev.pair(pr(curry(pi2), curry(s.ev)).pi1, pi2)
   let mult = ev.prod(pr(curry(zero.!), curry(add.pair(ev, pi2))), id)
   let fact = pi1.pr(pair(s.zero, zero), pair(mult.pair(s.pi2, pi1), s.pi2))

ここまでがデータ型と関数の定義で、
それぞれ terminal object ((- 普通の言語で言うところのUnit型 -)),
直積(product), 関数空間(exponential), 自然数, coproduct, 自然数の加算、
乗算、階乗を定義してる。

これらの定義から、例えば「fact.succ.succ.succ.zero」は
「succ.succ.succ.succ.succ.succ.zero」に簡約される。

== Features

* ((<dialgebra>))を用いたデータ型の定義
* データ型の定義から導かれる書き換えルールによる項書き換えによる計算モデル。
* 変数が無い (ポイントフリー)

== Download

* Implementation in Haskell:
  * ((<"HackageDB:CPL"|URL:http://hackage.haskell.org/package/CPL>))
  * ((<github|URL:https://github.com/msakai/cpl>))
  * Download old versions:
    * ((<"CPL-0.0.6.tar.gz"|URL:https://dl.dropboxusercontent.com/u/123796/archives/cabal/CPL-0.0.6.tar.gz>)) ((<"CPL-0.0.6.tar.gz"|URL:https://storage.googleapis.com/msakai-jp-archives/cabal/CPL-0.0.6.tar.gz>)) (2009-10-26)
    * ((<"CPL-0.0.5.tar.gz"|URL:https://dl.dropboxusercontent.com/u/123796/archives/cabal/CPL-0.0.5.tar.gz>)) ((<"CPL-0.0.5.tar.gz"|URL:https://storage.googleapis.com/msakai-jp-archives/cabal/CPL-0.0.5.tar.gz>)) (2009-10-08)
    * ((<"CPL-0.0.4.tar.gz"|URL:https://dl.dropboxusercontent.com/u/123796/archives/cabal/CPL-0.0.4.tar.gz>)) ((<"CPL-0.0.4.tar.gz"|URL:https://storage.googleapis.com/msakai-jp-archives/cabal/CPL-0.0.4.tar.gz>)) (2009-09-27)
    * ((<"CPL-0.0.3.tar.gz"|URL:https://dl.dropboxusercontent.com/u/123796/archives/cabal/CPL-0.0.3.tar.gz>)) ((<"CPL-0.0.3.tar.gz"|URL:https://storage.googleapis.com/msakai-jp-archives/cabal/CPL-0.0.3.tar.gz>)) (2009-06-15)
    * ((<files:cpl-hs-0.0.2.tar.gz>)) (2008-04-30)
    * ((<files:cpl-hs-0.0.1.tar.gz>))
* Implementation in Ruby (No longer maintained):
  * Download:
    * ((<files:cpl-0.0.3.tar.gz>))
    * ((<files:cpl-0.0.2.tar.gz>))
    * ((<files:cpl-0.0.1.tar.gz>))
  * ((<RAA:CPL>))

== リンク

* ((<ヒビルテ:CPL|URL:http://msakai.jp/d/?category=CPL>)):CPL|URL:/d/?category=CPL>))
* ((<CHARITY>)) はCPLを元にしたシステムらしい。