こわくない CPL (0) CPLの導入 - Ryusei’s Notes (a.k.a. M59のブログ)

圏論プログラミング言語 CPL - M59のブログでは、CPLの紹介と、データ型についての考察をしました。ここでは、理屈抜きでCPLで遊ぶための記事を書きます。CPLで実際にプログラムが書けるようになるのが目的です。

CPLのインストール

CPLには、Haskellによる実装があります。

CPL: An interpreter of Hagino's Categorical Programming Language (CPL).

cabalを使ってインストールできます。こんな感じにインストールしました。自分の環境ではreadlineが使えなかったので、-f -Readlineオプションを指定しています。Readlineが使えなくても、Haskelineがかわりに使われるので問題ありませんでした。

cabal get cpl
cd CPL-0.0.7
cabal sandbox init
cabal install --bindir ~/.cabal/bin --datadir ~/.cabal/share -f -Readline

CPLを起動してみましょう。

% cpl
Categorical Programming Language (Haskell version)
version 0.0.7

Type help for help

cpl>

とりあえず、helpコマンドを使って、どのようなコマンドが使えるか調べましょう。

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 object <functor>       print information of functor
  load <filename>             load from file
  set trace [on|off]          enable/disable trace
  reset                       remove all definitions

cplはexitでもquitでもbyeでも終了できます。

cpl> bye
%

プログラムの読込み

下のCPLのプログラムをコピーして、fib.cplなどといったファイル名で保存してください。

# 終対象
right object 𝟙 with ! is
end object;

# 積
right object prod(a, b) with pair is
  π₁: prod -> a
  π₂: prod -> b
end object;

# 冪
right object exp(a, b) with λ is
  ev: prod(exp, b) -> a
end object;

# 自然数
left object ℕ with pr is
  0: 𝟙 -> ℕ
  s: ℕ -> ℕ
end object;

# 加算
let add = ev.prod(pr(λ(π₂), exp(s, I)), I);

# フィボナッチ数
let fib = π₁.pr(pair(0, s.0), pair(π₂, add));

# fib(6)を計算する
simp fib.s.s.s.s.s.s.0;

cplコマンドにファイル名を渡すと、データ型が定義され、プログラムが実行されます。

% cpl fib.cpl
Categorical Programming Language (Haskell version)
version 0.0.7

Type help for help

> right object 𝟙 with ! is
> end object
right object 𝟙 is defined
> right object prod(a, b) with pair is
>   π₁: prod -> a
>   π₂: prod -> b
> end object
right object prod(+,+) is defined
> right object exp(a, b) with λ is
>   ev: prod(exp, b) -> a
> end object
right object exp(+,-) is defined
> left object ℕ with pr is
>   0: 𝟙 -> ℕ
>   s: ℕ -> ℕ
> end object
left object ℕ is defined
> let add = ev.prod(pr(λ(π₂), exp(s, I)), I)
add = ev.prod(pr(λ(π₂),exp(s,I)),I)
    : prod(ℕ,ℕ) -> ℕ
> let fib = π₁.pr(pair(0, s.0), pair(π₂, add))
fib = π₁.pr(pair(0,s.0),pair(π₂,add))
    : ℕ -> ℕ
> simp fib.s.s.s.s.s.s.0
s.s.s.s.s.s.s.s.0
    : 𝟙 -> ℕ
%

-iオプションを付けると、ファイルを読み込んだ後、インタラクティブモードに入ります。

% cpl fib.cpl -i
Categorical Programming Language (Haskell version)
version 0.0.7

...

> simp fib.s.s.s.s.s.s.0
s.s.s.s.s.s.s.s.0
    : 𝟙 -> ℕ
cpl>

実行時トレース

set traceコマンドで、実行時のトレースのオン・オフを切り替えられます。

cpl> set trace on
cpl> simp fib.s.0
0:fib.s.0*I
1[1]:s.0*I
2[2]:0*I
3[1]:s*0
4:fib*s.0
5:π₁.pr(pair(0,s.0),pair(π₂,add))*s.0
6[1]:pr(pair(0,s.0),pair(π₂,add))*s.0
7[1]:pair(π₂,add).pr(pair(0,s.0),pair(π₂,add))*0
8[2]:pr(pair(0,s.0),pair(π₂,add))*0
9[2]:pair(0,s.0)*I
10[1]:pair(π₂,add)*pair(0,s.0)
11:π₁*pair(π₂,add).pair(0,s.0)
12:π₂*pair(0,s.0)
13:s.0*I
14[1]:0*I
15:s*0
16:I*s.0
s.0
    : 𝟙 -> ℕ
cpl>