CPL

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 ^*1, 直積(product), 関数空間(exponential), 自然数, coproduct, 自然数の加算、 乗算、階乗を定義してる。

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

Features

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

Download

• Implementation in Haskell:
  • HackageDB:CPL
  • github
  • Download old versions:
    • CPL-0.0.6.tar.gz (2009-10-26)
    • CPL-0.0.5.tar.gz (2009-10-08)
    • CPL-0.0.4.tar.gz (2009-09-27)
    • 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
• CHARITY はCPLを元にしたシステムらしい。

^*1 普通の言語で言うところのUnit型