Bidirectional Typechecking を実装してみた。

はじめに

Desk言語ではBidirectional Typechecking のテクニックを使っているという話を聞いてよくわからないので調べてみて最も基本的な単相の双方向型検査器をPrologで書いてみました:

% Implementation of Bidirectional Typing Rules: A Tutorial
% http://davidchristiansen.dk/tutorials/bidirectional.pdf
% t ::= bool | t -> t | [t]
% b ::= true | false
% e ::= b | x | e$e | λ(x,e) | if(e,e,e) | e:t | [e|e] | []
% t は型でboolがbool型、t->tが関数型、[t]がリスト型です。
% bはbool値でtrueまたはfalseです。
% eは式を表し、bがbool値、xが変数、e$eが関数適用、λ(x,e)が関数、
% if(e,e,e)がif式、e:tが型注釈、[e|e]がリストのcons、[]が空リストです。
:- op(650,xfy,$), op(600,xfy,[⇐,⇒,⊢]), op(1200,xfx,if).
term_expansion(A if B, A :- B).
% check type
Γ⊢λ(X,E)  ⇐ (T2->T1) if [X:T2|Γ]⊢E ⇐ T1.
Γ⊢[E1|E2] ⇐ [T1]     if Γ⊢E1 ⇐ T1, Γ⊢E2 ⇐ [T1].
_⊢[]      ⇐ [_].
Γ⊢E       ⇐ T1       if Γ⊢E ⇒ T1.
% infer type
_⊢true        ⇒bool.
_⊢false       ⇒bool.
Γ⊢X           ⇒T1   if member(X:T1,Γ).
Γ⊢(E1:T1)     ⇒T1   if Γ⊢E1⇐T1.
Γ⊢(E1$E2)     ⇒T1   if Γ⊢E1⇒(T2->T1), Γ⊢E2⇐T2.
Γ⊢if(E1,E2,E3)⇒T1   if Γ⊢E1⇐bool,     Γ⊢E2⇒T1, Γ⊢E3⇒T1.
Γ⊢[E1|E2]     ⇒[T1] if Γ⊢E1⇒T1,       Γ⊢E2⇐[T1].

test(E,ET):- []⊢E⇒T,!,T=ET.
:- test(λ(x, if(x, false, true)):(bool->bool),bool->bool).
:- test([true, true, false],[bool]).
:- test([([]:[bool]),[],[]],[[bool]]).
:- halt.

構文

t ::=       (型)
  bool      (bool型)
  t -> t    (関数型)
  [t]       (リスト型)
b ::=       (bool値)
  true      (真)
  false     (儀)
e ::=       (式)
  b         (bool値)
  x         (変数)
  e$e       (関数適用)
  λ(x,e)    (関数)
  if(e,e,e) (if式)
  e:t       (型注釈)
  [e|e]     (cons)
  []        (空リスト)

単相の双方向型検査器は、単一化をすることなく型推論ができたりできなかったりします。 ⊢e⇐t の形の規則は型推論が不可能な規則であり型を入力する型検査器であることを表します。 ⊢e⇒t の形の規則は型推論が可能な規則であり型が出力されることを表します。 型が推論できない場合は型注釈を付けることで型推論が可能な式にできます。

# 代数的データ型とBNFで妄想するプログラミング言語2

代数的データ型とBNFで妄想するプログラミング言語2

はじめに

昨日はザーッとBNFを書いていく方法を書いてみました。 しかし成果物をみるとちゃんとした仕様書とは言えないものができてしまったように思います。 今日は昨日の成果をもとに仕様のみを抜き出して書いていこうと思います。 言語仕様は全体的な構文と機能ごとの追加構文、例、説明で構成することにします。

1. 整数

構文:

e ::=       式
    i       整数

1. 整数

構文:

e ::=       式
    i       整数

例:

0
123
456789

整数は0から9までの文字の連続です。

2. 足し算

構文:

e ::=       式
    i       整数
    e+e     足し算

2. 足し算

構文:

    e+e     足し算

整数は0から9までの文字の連続です。

例:

1+2
123+456+789

足し算は2項演算子 + で結合された式で、いくつも連続して書くことができます。

3. その他の四則演算

足し算とその他の四則演算を1つにまとめてしまいます。

構文:

e ::=       式
    i       整数
    e+e     足し算
    e-e     引き算
    e*e     掛け算
    e/e     割り算

2. 四則演算

構文:

e ::=       式
    :
    e+e     足し算
    e-e     引き算
    e*e     掛け算
    e/e     割り算

例:

1+2
1-2
1*2
1/2

足し算は2項演算子 + で結合された式で、いくつも連続して書くことができます。 引き算は二項演算子 -、掛け算は二項演算子 *、割り算は二項演算子/を使って結合された式として表せます。

4. Bool

構文:

b ::=       bool
    true    真
    false   儀
e ::=       式
    i       整数
    b       bool
    e+e     足し算
    e-e     引き算
    e*e     掛け算
    e/e     割り算

3. Bool

構文:

b ::=       bool
    true    真
    false   儀
e ::=       式
    :
    b       bool

例:

true
false

bool は trueとfalseからなります。

5. if式

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    if e then e else e      if式

4. if式

構文:

e ::=                       式
    :
    if e then e else e      if式

例:

if true then 1 else 2
(if true then 1 else 2) + 3

if は式なので結果を返し他の式の中に書くことができます。

6. 比較演算子

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式

5. 比較演算子

構文:

e ::=                       式
    :
    e<e                     比較演算子

例:

1 < 2
2 < 3

比較式は比較演算子< で結合された式です。

7. 変数、関数、関数適用

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    x                       変数
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式
    λx.e                    関数
    e e                     関数適用

6. 変数、関数、関数適用

構文:

e ::=                       式
    :
    x                       変数
    λx.e                    関数
    e e                     関数適用

例:

a
abc123
x
λa.a+1
λa.λb.a+b
(λa.a+1) 10
(λa.λb.a+b) (1+2) (3+4)

変数はアルファベットで始まる識別子で表されます。 関数はラムダ抽象を使って書き引数は1つしか使えませんが、関数を連続して書くことで複数の引数がある処理も行うことができます。 関数呼び出しは式を2つ並べた形になります。

8. let式、let rec式

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    x                       変数
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式
    λx.e                    関数
    e e                     関数適用
    let x = e in e          let式
    let rec x = e in e      let rec式

7. let式、let rec式

構文:

e ::=                       式
    :
    let x = e in e          let式
    let rec x = e in e      let rec式

例:

let a = 1+2 in let b = 2+3 in a+b

let a =
  let a = 1+2 in
  let b = 2+3 in
  a+b
in
a+3

let rec fib = λx.
  if x<2 then x else
  fib (x-2) (x-1)
in
fib 10

let式は指揮を複数に分けて書くことができるようにできる式です。プログラムを分けて書けるようになるため便利です。 let式により変数に値を束縛できます。変数はin以降で使えるようになります。inより手前ではそれ以前に定義された変数が使われます。 同じ変数名で別な値を束縛するとそれ以降で見えなくなり、シャドウィングと言います。 let rec 式はinの手前でも変数を参照ができる点以外はlet式と同様に用いることができます。再帰呼び出しをする関数を定義するような場合に用います。

9. 仕様のまとめ

最後に、全体をまとめて1つの仕様としましょう。

言語仕様

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    x                       変数
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式
    λx.e                    関数
    e e                     関数適用
    let x = e in e          let式
    let rec x = e in e      let rec式

1. 整数

構文:

e ::=                       式
    i                       整数

例:

0
123
456789

整数は0から9までの文字の連続です。

2. 四則演算

構文:

e ::=                       式
    :
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算

例:

1+2
1-2
1*2
1/2

足し算は2項演算子 + で結合された式で、いくつも連続して書くことができます。 引き算は二項演算子 -、掛け算は二項演算子 *、割り算は二項演算子/を使って結合された式として表せます。

3. Bool

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    :
    b                       bool

例:

true
false

bool は trueとfalseからなります。

4. if式

構文:

e ::=                       式
    :
    if e then e else e      if式

例:

if true then 1 else 2
(if true then 1 else 2) + 3

if は式なので結果を返し他の式の中に書くことができます。

5. 比較演算子

構文:

e ::=                       式
    :
    e<e                     比較演算子

例:

1 < 2
2 < 3

比較式は比較演算子< で結合された式です。

6. 変数、関数、関数適用

構文:

e ::=                       式
    :
    x                       変数
    λx.e                    関数
    e e                     関数適用

例:

a
abc123
x
λa.a+1
λa.λb.a+b
(λa.a+1) 10
(λa.λb.a+b) (1+2) (3+4)

変数はアルファベットで始まる識別子で表されます。 関数はラムダ抽象を使って書き引数は1つしか使えませんが、関数を連続して書くことで複数の引数がある処理も行うことができます。 関数呼び出しは式を2つ並べた形になります。

7. let式、let rec式

構文:

e ::=                       式
    :
    let x = e in e          let式
    let rec x = e in e      let rec式

例:

let a = 1+2 in let b = 2+3 in a+b

let a =
  let a = 1+2 in
  let b = 2+3 in
  a+b
in
a+3

let rec fib = λx.
  if x<2 then x else
  fib (x-2) (x-1)
in
fib 10

let式は指揮を複数に分けて書くことができるようにできる式です。プログラムを分けて書けるようになるため便利です。 let式により変数に値を束縛できます。変数はin以降で使えるようになります。inより手前ではそれ以前に定義された変数が使われます。 同じ変数名で別な値を束縛するとそれ以降で見えなくなり、シャドウィングと言います。 let rec 式はinの手前でも変数を参照ができる点以外はlet式と同様に用いることができます。再帰呼び出しをする関数を定義するような場合に用います。

10. まとめ

ここでは、fib関数を書ける言語を妄想してみたものを元に、言語仕様飲みに集中して順番に書いてみました。 最初は順番に1つの機能ごとに書いて最後にまとめて1つの仕様としました。 いきなり大きな仕様を書くのではなく徐々に大きく育てていく楽しさがあります。 慣れてしまえば、Rustのような処理系を使わずとも仕様を簡単に素早く書けるようになるはずです。

代数的データ型とBNFで妄想するプログラミング言語

代数的データ型とBNFで妄想するプログラミング言語

はじめに

BNFってなんだか難しそうって思う方もおられると思いますがそんなに気構えずに楽しく書く気持ちを説明したいと思います。 BNFは狭義の意味ではバッカスナウア記法を用いた構文解析器を表す記法になりますが、ここで用いるBNF木構造データに対するBNF記法です。 通常は抽象構文用いて定義する代数的データ型を、具象構文をつかって定義するようなものと考えることもできます。

これ以降の章では例とRustのenumBNFによる構文を書き説明する形で言語の仕様を拡張していきます。 最終目標はλ計算でfib関数を書ける言語を作ることです。

1. 整数

例:

0
123
456789

整数は0から9までの文字の連続です。

Rust:

enum E {        // 式
    I(i32),     // 整数
}

Rustで式に整数だけ使える言語を考えるとenumを使って上記のように書くことができます。

構文:

e ::=       式
    i       整数

BNFライクに書くと上記のように書くことができます。

2. 足し算

例:

1+2
123+456+789

足し算は2項演算子 + で結合された式で、いくつも連続して書くことができます。

Rust:

type e = Box<E>;
enum E {        // 式
    I(i32),     // 整数
    Add(e,e)    // 足し算
}

Rustで再帰的に型を使いたい場合にデータサイズがわからなくなるので困ります。そういった場合はBoxなどで再帰的な型を使うことができます。 Box<E> のように書くのは長くなるので小文字のeBox<E> として使うことにしました。

構文:

e ::=       式
    i       整数
    e+e     足し算

BNF で書く場合は型のサイズなどを気にせずに以上のように書くことができます。

3. その他の四則演算

例:

1+2
1-2
1*2
1/2

引き算は二項演算子 -、掛け算は二項演算子 *、割り算は二項演算子/を使って結合された式として表せます。

Rust:

type e = Box<E>;
enum E {        // 式
    I(i32),     // 整数
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
}

Rustならコンパイルしておかしな定義になっていないことが確認できます。

構文:

e ::=       式
    i       整数
    e+e     足し算
    e-e     引き算
    e*e     掛け算
    e/e     割り算

BNF で書くとASTというよりも唯の構文のイメージになるので簡単です。

4. Bool

例:

true
false

Rust:

type e = Box<E>;
enum E {        // 式
    I(i32),     // 整数
    B(bool),    // Bool
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
}

構文:

b ::=       bool
    true    真
    false   儀
e ::=       式
    i       整数
    b       bool
    e+e     足し算
    e-e     引き算
    e*e     掛け算
    e/e     割り算

bはboolだと書けば分かる話ではありますが、BNFで書く場合はbがboolでありtrueとfalseからなると明示すると良いかもしれません。

RustでBoolを明示するなら以下のように書くことができます:

type e = Box<E>;
enum B {        // Bool
    True,       // 真
    False,      // 儀
}
enum E {        // 式
    I(i32),     // 整数
    B(B),       // Bool
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
}

5. if式

ここからは順番を構文、例、Rustにしていきます。

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    if e then e else e      if式

if式 は if e1 then e2 else e3 のような式でe1がtrueならばe2が評価されそうでなければe2が評価される式です。

例:

if true then 1 else 2
(if true then 1 else 2) + 3

if は式なので結果を返し他の式の中に書くことができます。

Rust:

type e = Box<E>;
enum B {        // Bool
    True,       // 真
    False,      // 儀
}
enum E {        // 式
    I(i32),     // 整数
    B(B),       // Bool
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
    If(e,e,e),  // if式
}

RustだとthenやelseはないASTになります。

6. 比較演算子

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式

例:

1 < 2
2 < 3

比較式は比較演算子< で結合された式です。

Rust:

type e = Box<E>;
enum B {        // Bool
    True,       // 真
    False,      // 儀
}
enum E {        // 式
    I(i32),     // 整数
    B(B),       // Bool
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
    Le(e,e),    // 比較演算子
    If(e,e,e),  // if式
}

7. 変数、関数、関数適用

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    x                       変数
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式
    λx.e                    関数
    e e                     関数適用

例:

a
abc123
x
λa.a+1
λa.λb.a+b
(λa.a+1) 10
(λa.λb.a+b) (1+2) (3+4)

変数はアルファベットで始まる識別子で表されます。 関数はラムダ抽象を使って書き引数は1つしか使えませんが、関数を連続して書くことで複数の引数がある処理も行うことができます。 関数呼び出しは式を2つ並べた形になります。

Rust:

type e = Box<E>;
type x = String;//文字列
enum B {        // Bool
    True,       // 真
    False,      // 儀
}
enum E {        // 式
    I(i32),     // 整数
    B(B),       // Bool
    X(x),       // 変数
    Add(e,e),   // 足し算
    Sub(e,e),   // 引き算
    Mul(e,e),   // 掛け算
    Div(e,e),   // 割り算
    Le(e,e),    // 比較演算子
    If(e,e,e),  // if式
    Fun(x,e),   // 関数
    App(e,e),   // 関数適用
}

そろそろ Rust 実装書かなくてもわかるだろう、、、と思いますが一応。

8. let式、let rec式

構文:

b ::=                       bool
    true                    真
    false                   儀
e ::=                       式
    i                       整数
    b                       bool
    x                       変数
    e+e                     足し算
    e-e                     引き算
    e*e                     掛け算
    e/e                     割り算
    e<e                     比較演算子
    if e then e else e      if式
    λx.e                    関数
    e e                     関数適用
    let x = e in e          let式
    let rec x = e in e      let rec式

例:

let a = 1+2 in let b = 2+3 in a+b

let a =
  let a = 1+2 in
  let b = 2+3 in
  a+b
in
a+3

let rec fib = λx.
  if x<2 then x else
  fib (x-2) (x-1)
in
fib 10

let式は指揮を複数に分けて書くことができるようにできる式です。プログラムを分けて書けるようになるため便利です。 let式により変数に値を束縛できます。変数はin以降で使えるようになります。inより手前ではそれ以前に定義された変数が使われます。 同じ変数名で別な値を束縛するとそれ以降で見えなくなり、シャドウィングと言います。 let rec 式はinの手前でも変数を参照ができる点以外はlet式と同様に用いることができます。再帰呼び出しをする関数を定義するような場合に用います。

Rust:

type e = Box<E>;
type x = String;    // 文字列
enum B {            // Bool
    True,           // 真
    False,          // 儀
}
enum E {            // 式
    I(i32),         // 整数
    B(B),           // Bool
    X(x),           // 変数
    Add(e,e),       // 足し算
    Sub(e,e),       // 引き算
    Mul(e,e),       // 掛け算
    Div(e,e),       // 割り算
    Le(e,e),        // 比較演算子
    If(e,e,e),      // if式
    Fun(x,e),       // 関数
    App(e,e),       // 関数適用
    Let(x,e,e),     // let式
    LetRec(x,e,e),  // let rec式
}

9. まとめ

ここでは、ゼロからラムダ計算でfib関数を書ける言語を妄想してみました。補助言語としてRustのenumを代数的データ型として使い確認もしました。 特にパーサや評価器は作っていませんが、このように妄想することでプログラミング言語の仕様を形式的な感じに書くことができます。 ラムダ計算の形式化は様々な書き方で定義されていますが、書いたことがない方は書いてみましょう。 慣れてくるとプログラミング言語の仕様を書くのが楽しくなるはずです。 最初は難しい、あるいは面倒に感じるかも知れませんが慣れれば楽しく言語を設計できるようになるので是非チャレンジしてみましょう。

λeffをPrologに移植したら133行で書けた。

代数的効果は継続のようであるけど様々なエフェクトに使えるので今後期待されている技術です。 λeff はそのエッセンスを取り出した言語ですがそれなりに代数的効果を実験できるのでいろいろな言語に実装してみています。 今回はλeff を Prolog に移植してどの程度短くなるのか見てみました。

まずは字句解析器です。Prolog の場合は DCG 記法を使うと綺麗にパーサや字句解析器が書けます。パーサコンビネータで必要になるバックトラックや分岐、文脈を隠す機能などが揃っているのでかなり便利に使えます。値を返すパーサは文法名に返す変数名を入れないといけないのがやや冗長になりますが以下のような感じになりました:

lexer.pl

:- module(lexer,[tokens/3]).
:- set_prolog_flag(double_quotes, chars).
rep1(F,[C|Cs]) --> call(F,C),rep1(F,Cs).
rep1(F,[C])    --> call(F,C).
rep0(F,Cs)     --> rep1(F,Cs) | [],{Cs=[]}.
digit(C)       --> [C], { code_type(C, digit) }.
paren(C)       --> [C], { member(C,"()[]{}") }.
punct(C)       --> [C], { code_type(C, punct),not(paren(C,[C],[])) }.
alpha(C)       --> [C], { code_type(C, lower);code_type(C, upper);C='_' }.
alnum(C)       --> alpha(C); digit(C).
digits(Cs)     --> rep1(digit,Cs).
ident([C|Cs])  --> alpha(C),rep0(alnum,Cs).
puncts(R)      --> rep1(punct, R).
tok(T) --> digits(Cs),  { number_chars(I, Cs),!,T=int(I) }
         | ident(C),    { atom_codes(A,C),!,(member(A,[let,in,handler,val,with,handle,inst,perform,fun])->T=A;T=id(A)) }
         | paren(C),    { atom_codes(T,[C]) }
         | puncts(C),   { atom_codes(T,C) }.
tokens(Ts)     --> (" "|"\r"|"\n"|"\t"), tokens(Ts).
tokens([T|Ts]) --> tok(T), !, tokens(Ts).
tokens([])     --> "".

パーサもDCGと字句解析器を使って書きました:

parser.pl

:- module(parser,[parse/2,parseFile/2]).
:- use_module(lexer,[tokens/3]).

readAll(File, Str) :-
    setup_call_cleanup(open(File, read, In),
       read_string(In, _, Str),
       close(In)).
parseFile(F,R):- readAll(F,S),string_chars(S,C),parse(C,R).
parse(C,R):- tokens(Ts,C,[]), expr(R,Ts,_).

rep1(F,[C|Cs]) --> call(F,C),(rep1(F,Cs);{Cs=[]}).
rep0(F,Cs) --> rep1(F,Cs) | [],{Cs=[]}.

expr(R)-->[let],id(A),[=],expr(B),[in],expr(C),
                                   {R=(let(A=B);C)}
        | [handler],id(A),['('],[val],id(B),[->],expr(C),[')'],
            ['('],['('],id(D),[','],id(E),[')'],[->],expr(F),[')'],
                                   {R=handler(A,B->C,(D,E)->F)}
        | [with],expr(A),[handle],expr(B),
                                   {R=with(A,B)}
        | [inst],['('],[')'],      {R=inst()}
        | [perform],id(A),expr(B), {R=perform(A,B)}
        | [fun],id(A),[->],expr(B),{R=fun(A->B)}
        | term(A),                 {R=A}.
term(R)-->fact(A),rep0(t1,As),     {foldl([(Op,C),B,D]>>(D=..[Op,B,C]),As,A,R)}.
t1(R)  -->[+],fact(A),             {R=(+,A)}
        | [-],fact(A),             {R=(-,A)}.
fact(R)-->app(A),rep0(f1,As),      {foldl([(Op,C),B,D]>>(D=..[Op,B,C]),As,A,R)}.
f1(R)  -->[*],app(A),              {R=(*,A)}
        | [/],app(A),              {R=(/,A)}.
app(R) -->rep1(atm,[A|As]),        {foldl([B,C,$(C,B)]>>!,As,A,R)}.
atm(R) -->['('],expr(A),[')'],     {R=A}
        | id(A),                   {R=A}
        | int(A),                  {R=A}.
int(A) -->[int(A)].
id(A)  -->[id(A)].

LLなパーサなので左再帰がある文法はループにしてfoldlで展開する感じに書き換えが必要ですが後は悩まず書けました。

評価器は構文をタグレスな形で扱うことで短く書けました。値の判定は値を返さない唯の述語として書いたり、数式演算の関数というか述語も消してしまえたのでより短くなりました。パターンマッチの分岐も評価規則ごとに分けて書けるので綺麗と思えば綺麗にかけます。パターンマッチのほうが好きな人もいると思いますけど。スモールステップ評価器は評価文脈を使うとよりきれいに書けるのですが今回は展開した状態で書いてあります。穴空きの数式をスタックにためて継続として扱う箇所はcopy_termを使ってみました:

eval.pl

:- module(eval,[run/2]).
:- op(800,xfx,[==>,$]).

i(I):- integer(I).
v(X):- atom(X).
v(handler(_,_,_)).
v(fun(_->_)).
v(eff(_)).
v(abort()).
v(I):- i(I).

subst(Y,Y,T,T):- atom(Y),!.
subst(fun(A->B),Y,T,fun(A->T1)):- A \= Y,subst(B,Y,T,T1).
subst(A$B,Y,T,T1$T2):- subst(A,Y,T,T1),subst(B,Y,T,T2).
subst(perform(A,B),Y,T,perform(T1,T2)):- subst(A,Y,T,T1),subst(B,Y,T,T2).
subst(let(Y=B);C,Y,T,let(Y=T1);C):- subst(B,Y,T,T1).
subst(let(A=B);C,Y,T,let(A=T1);T2):- subst(B,Y,T,T1),subst(C,Y,T,T2).
subst(with(A,B),Y,T,with(T1,T2)):- subst(A,Y,T,T1),subst(B,Y,T,T2).
subst(handler(A,B->C,(D,E)->F),Y,T,handler(A_,B->C_,(D,E)->F_)):-
        subst(A,Y,T,A_),(B=Y->C_=C;subst(C,Y,T,C_)),
        ((D = Y; E = Y)-> F_=F;subst(F,Y,T,F_)).
subst(L+R,Y,T,L_+R_):- subst(L,Y,T,L_),subst(R,Y,T,R_).
subst(L-R,Y,T,L_-R_):- subst(L,Y,T,L_),subst(R,Y,T,R_).
subst(L*R,Y,T,L_*R_):- subst(L,Y,T,L_),subst(R,Y,T,R_).
subst(L/R,Y,T,L_/R_):- subst(L,Y,T,L_),subst(R,Y,T,R_).
subst(T,_,_,T):- !.
substs(T,List,T_):- foldl([X/U,Acc,V]>>subst(Acc,X,U,V),List,T,T_).

cp(A,B) :- copy_term(A,B).
flatfn([],X,X).
flatfn([F|Fs],X,A):- flatfn(Fs,X,A1),cp(F,A1/A).
kfunc(Stack,fun(◇ ->R)):- flatfn(Stack,◇,R).
vh(handler(_,X->T,_),(X,T)).
vh(_,_):- throw('Handler only!').

p(_,_,_,[],Es,(abort(),[],Es)):- !.
p(Eff,E,V,[F|S],Es,R):- cp(F,□ /F1),p1(Eff,E,V,[F|S],Es,F1,R).
p1(Eff,_,V,[F|S],Es,with(handler(Eff,_,(X,K)->E1),□),(E_,[F|S],[])):- !,
    kfunc(Es,Es_),!,substs(E1,[X/V,K/Es_],E_),!.
p1(Eff,_,_,[F|S],Es,with(handler(_,_,(_,_)->Ee),□),(perform(Eff,Ee),S,[F|Es])):- !.
p1(Eff,E,_,[F|S],Es,_,(perform(Eff,E),S,[F|Es])):- !.

%==>((_,(T,S,_)),_):-length(S,L),writeln(T;L),fail.
{P,inst(),S,Es}==>{P1,eff(P1),S,Es}:- P1 is P+1,!.
{P,fun(A->B)$E,S,Es}==>{P,B_,S,Es}:- v(E),subst(B,A,E,B_),!.
{P,F$E,S,Es}==>{P,E,[T/(F$T)|S],Es}:- v(F),!.
{P,F$E,S,Es}==>{P,F,[T/(T$E)|S],Es}:- !.
{P,E1+E2,S,Es}==>{P,E,S,Es}:- v(E1),v(E2),E is E1+E2,!.
{P,E1+E2,S,Es}==>{P,E2,[T/(E1+T)|S],Es}:- v(E1),!.
{P,E1+E2,S,Es}==>{P,E1,[T/(T+E2)|S],Es}:- !.
{P,E1-E2,S,Es}==>{P,E,S,Es}:- v(E1),v(E2),E is E1-E2,!.
{P,E1-E2,S,Es}==>{P,E2,[T/(E1-T)|S],Es}:- v(E1),!.
{P,E1-E2,S,Es}==>{P,E1,[T/(T-E2)|S],Es}:- !.
{P,E1*E2,S,Es}==>{P,E,S,Es}:- v(E1),v(E2),E is E1*E2,!.
{P,E1*E2,S,Es}==>{P,E2,[T/(E1*T)|S],Es}:- v(E1),!.
{P,E1*E2,S,Es}==>{P,E1,[T/(T*E2)|S],Es}:- !.
{P,E1/E2,S,Es}==>{P,E,S,Es}:- v(E1),v(E2),E is E1 div E2,!.
{P,E1/E2,S,Es}==>{P,E2,[T/(E1/T)|S],Es}:- v(E1).
{P,E1/E2,S,Es}==>{P,E1,[T/(T/E2)|S],Es}:- !.
{P,(let(X=E);E2),S,Es}==>{P,B,S,Es}:- v(E),subst(E2,X,E,B),!.
{P,(let(X=E);E2),S,Es}==>{P,E,[T/(let(X=T);E2)|S],Es}:- !.
{P,with(H,E),S,Es}==>{P,Ev_,S,Es}:- v(E),vh(H,(X,Ev)),subst(Ev,X,E,Ev_),!.
{P,with(H,E),S,Es}==>{P,E,[T/with(H,T)|S],Es}:- !.
{P,perform(Eff,E),S,Es}==>{P,Eff_}:- v(Eff),v(E),p(Eff,E,E,S,Es,Eff_),!.
{P,perform(Eff,E),S,Es}==>{P,E,[T/perform(Eff,T)|S],Es}:- v(Eff),!.
{P,perform(Eff,E),S,Es}==>{P,Eff,[T/perform(T,E)|S],Es}:- !.
{P,V,[],Es}==>{P,V,[],Es}:- v(V).
{P,V,[F|S],Es}==>{P,V_,S,Es}:- v(V),!,cp(F,V/V_),!.
{_,E,_,_}==>_:- throw(error(eval(E))).

go({_,V,[],_},V):- v(V),!.
go(W,M2):- W==>W2, go(W2,M2).
run(T,V):- go({0,T,[],[]},V).

メインの処理は引数を引っ張り出しパース後に実行するだけです:

main.pl

:- use_module(parser,[parse/2,parseFile/2]).
:- use_module(eval,[run/2]).
:- current_prolog_flag(os_argv, [_,_,F|_]),parseFile(F,T),!,run(T,R),!,writeln(R).
:- halt.

collect.txt

let collect = inst () in
let h = handler collect (val x -> x) ((x, k) -> let v=k x in v*100+x) in
with h handle
    let a = (perform collect 1) in
    let b = (perform collect 2) in
    let c = (perform collect 3) in
    let d = (perform collect 4) in
    0

実行方法

$ swipl main.pl collect.txt
10203040

な感じで動かせます。

$ wc *.pl
      73     148    3137 eval.pl
      20      93     970 lexer.pl
       4       9     166 main.pl
      36      79    1542 parser.pl
     133     329    5815 total

全部で133行でかなり簡潔に理解出来た気がします。

ワークショップの開き方のテンプレートを考えてみた。

いかのような感じでテンプレートを用意してあると便利そうだなぁ。

# 〇〇ワークショップ

## はじめに

ワークショップの目的を書きます。

## 対象者

ここにはワークショップに参加して欲しい人に求められるスキルやあらかじめ環境構築が必要な場合は環境構築方法を書いておきます。

各言語のOSごとのインストール方法をコピペで済むようにしておくと良いはず。

### Rust インストール
### C言語インストール
### SWI-PRologインストール
### OCamlインストール
### SMLインストール
### Haskellインストール
### LLVMインストール

## 目的

ここにはどのような目的でワークショップを行うかを書きます。

## 応募期間

202x/xx/xx 中に参加表明をお願いします。

## 日程

202x/xx/xx の 20時から22時まで開催します。

## 制作物の著作権

ご自由にお使いください。

## ポリシー(CoC)

迷惑行為はおやめください。

言語実装を協力して作りたい話

久しくブログを書くことから離れてたのですが、最近は昔と違って言語実装をして遊ぶ人が増えました。 C言語C言語を作ってブートストラップするような高校生が多くいる状況は一昔前ではなかった状況で楽しいです。

ここまで人が増えてくると、かつてはソロで言語を作っていた状況ではなく協力してモノづくりをしていけるといいのになという思いがより強く感じるようになってきました。 自分は人望がないから人を集めて言語を作ろうとしてもうまくいかないと諦めていたりもしたのですが、自分で主体性を持ってやってみたらどうかという話もされたりしたので、オレオレ言語の言語コミニュティーの作り方の手法自体を考えて多くの言語処理系実装者の方々がそれなりにグループを作りやすい環境というか文化を作れたら良いかなと考えております。

グループを作るといってもLisp的な言語を作るのであればLisp的な言語を作る文化圏の人々で協力すると良いでしょうし、Ruby的な言語を作るならRubyの文化圏の人々でグループを作ると良いでしょう。

形式的な手法を使いたい人達はそれなりにまとまるとよいだろうということでグループは作れそうな気がしてます。

でメンバー募集ページのようなもので仲間を集めて協力しようという話になったら、その言語のストリームを作って話し合うといいのかな。 ということでDesk言語を手伝う話を頂いたわけですがどうなるかな?

実装組の共通言語としてProlog使って情報共有したらどうかと考えてたけど今だとRustがいいらしいのでRust実装書くのがいいのかなぁ。 しかし論文読めるようにならないだろう問題があり、一階述語論理を理解するための言語はPrologが最適だよなと思うのでした。 LisperならRacket Redexを使えばいいと思うのですけど。 Rustが使えるならRust実装のPrologを使ってもらえばいいのかな。Cでのブートストラップ組はPrologもブートストラップするとよいだろう。

あと最近の流行りがDesk言語でも採用しているという代数的効果です。これを簡潔な実装から理解したいし、Desk言語の文脈でやっていきたいかな。

言語を作ったら広めたいだろうしオレオレ言語のチュートリアルを作ったらその言語を使うワークショップをやりたい。

あと、メタなレベルだけど言語を協力して作って遊ぶワークショップもやりたい。最初は短く始めて1日で終る分量でやりたい。 そこで協力するイメージを共有できるとよい。 Prologを覚えるワークショップも開催したい。

ワークショップの開き方とかがわからないと困るので言語ワークショップの企画のテンプレートを用意して置いてコピって使えると良さそう。

ってあたりを考えている今日このごろです。

OCamlで作ったgoma言語

この記事はML Advent Calendar 2014 9日目の記事です。 前 SMLでソートMllexを使ってみる。あるいはlexユーザーに対するmllexの解説

MLアドベントカレンダーが危ない。ということで、今日は、goma言語の紹介をチャラっと書いてみます。

URLはこちら https://github.com/hsk/goma

goma言語はOCamlで作ったC++を出力するトランスレータ言語です。 ATSに影響を受けて、C言語を出力するプログラミング言語を作ってみようと思ったのですが、C++のほうが楽だし、C++でよいや、いやむしろC++への出力の方がよいのではないか?

等と考えてC++を出力しています。

特徴

  • goma言語の特徴は極めて小さい構成。
  • 型システムがGoLangっぽい。
  • C言語に近い構文。

となっております。

型システム

GoLangインターフェイスを使った型システムはなかなか優れており、ビジターパターンのようなことが簡単に出来ます。しかも、後付けで関数を追加出来るような感じで強力です。 Haskellの型クラスのようなことをしつつ、オブジェクト指向っぽい事が出来るイメージであり強力なわけです。

で、gomaでは、そのインターフェイスの仮想テーブルと型にIDを付ける事で、多体性を実現したら速いんじゃないかと思って実装してみたわけです。 でもって、メモリは食うけど速そうって言う結論が出たって感じだったと思います。

それと、未来的な事を考えると、GPGPUあるいはFPGA等で、オブジェクトのメソッド検索を並列処理で検索すると速いとかいう未来もあるのかもしれないなと思ったりしてCPUとGPUが同じメモリを共有して弄るアーキティクチャなどものびて来ているようで、昔だとAMIGAが全部グラフィックスメモリっていう構成でDMA転送が速いから高速に動くみたいなのがあったなぁっと思ったりしたのでした。

実際に使ってみる

えーとまずは、ハローワールドです。

example/hello.goma

include stdio.h
main():int = {
  printf("hello world\n")
  return 0
}

セミコロン書かなくていい感じです。

変換して実行してみます。

$ ./gomac example/hello.goma example/hello.cpp
$ g++ example/hello.cpp -o hello
$ ./hello
hello world!

こんな感じになります。出力結果はlook like this:

example/hello.cpp

#include <stdio.h>
int main() {
  printf("hello world!\n");
  return 0;
}

オッケー。

なに?C++のプログラムなのに、printf使うなって?良いんだよ便利だから。

あとは、example見てくださいでもいいんだけど、ちゃんと書け俺。

計算機とかですね。

calc.goma

include "../lib/core.h"
include stdio.h

E class ()
E :> EInt (x:int)
E :> EAdd (x:*E,y:*E)
E :> EMul (x:*E,y:*E)

Eval   trait { eval():int }
Eval :> EInt { eval():int = return @x }
Eval :> EAdd { eval():int = return (*@x)|>Eval.eval() + (*@y)|>Eval.eval() }
Eval :> EMul { eval():int = return (*@x)|>Eval.eval() * (*@y)|>Eval.eval() }

main():int = {
  
  i:EInt(1)
  printf("eval 1 = %d\n", i|>Eval.eval())

  add:EAdd(new EInt(1), new EInt(2))
  printf("eval 1 + 2 = %d\n", add|>Eval.eval())

  mul:EMul(new EAdd(new EInt(1),new EInt(2)), new EInt(111))
  printf("eval (1 + 2) * 111 = %d\n", mul|>Eval.eval())

  return 0
}

なんか、golangっぽいっしょ。

Evalトレイトを定義して、Evalトレイトを継承したかんじで、色んな型の実装を後から定義して、動くと言う事ですよ。素晴らしいじゃないすか。

package main

import "fmt"
import "time"

type EInt struct {x int }
type EAdd struct {x E; y E}
type EMul struct {x E; y E}

type E interface { eval() int }
func (p *EInt)     eval() int { return p.x }
func (p *EAdd)     eval() int { return p.x.eval() + p.y.eval() }
func (p *EMul)     eval() int { return p.x.eval() * p.y.eval() }

func main() {

  i:= EInt{1}
  fmt.Printf("eval 1 = %d\n", i.eval())

  add:=EAdd{&EInt{1}, &EInt{2}}
  fmt.Printf("eval 1 + 2 = %d\n", add.eval())

  mul:=EMul{&EAdd{&EInt{1},&EInt{2}}, &EInt{111}}
  fmt.Printf("eval (1 + 2) * 111 = %d\n", mul.eval())

}

goで書くとこんなプログラムになり、Haskellで書くといかのようになります。

calc.hs

{-# LANGUAGE ExistentialQuantification #-}

data E = forall a. Eval a => E a
data EInt = EInt Int
data EAdd = EAdd E E
data EMul = EMul E E

class    Eval a    where eval :: a -> Int
instance Eval E    where eval (E x) = eval x
instance Eval EInt where eval (EInt x) = x
instance Eval EAdd where eval (EAdd x y) = eval x + eval y
instance Eval EMul where eval (EMul x y) = eval x * eval y
 
main = do
  let i = E(EInt 1)
  putStrLn $ "eval 1 = " ++ show (eval i)

  let add = E(EAdd (E(EInt 1)) (E(EInt 2)))
  putStrLn $ "eval 1 + 2 = " ++ show (eval add)

  let mul = E(EMul (E(EAdd (E(EInt 1)) (E(EInt 2)))) (E(EInt 111)))
  putStrLn $ "eval (1 + 2) * 111 = " ++ show (eval mul)

Scalaでも書いてみたりしたのですけど、githubの方見てみてください。

次は適当フィボナッチ(2以下は1だけじゃだめだろとかいうことで)の例です。関数で書いた例とオブジェクト使ったような例があります。

fib.goma

include "../lib/core.h"
include stdio.h

fib(a:int):int =
  if (a < 2) return 1
  else       return fib(a-2)+fib(a-1)

Fib trait {
  fib():int
}

Int class (x:int)
Int <: Fib {
  fib():int =
    if (@x < 2) return 1
    else {
      p1:Int(@x - 2)
      p2:Int(@x - 1)
      return p1|>Fib.fib() + p2|>Fib.fib()
    }
}

main():int = {

  start:long = gett()
  result:int = fib(40)
  printf("fib %d %d %ld\n", 40, result, gett() - start)

  start = gett()
  i:Int(40)
  printf("fib %d %d %ld\n", i.x, i|>Fib.fib(), gett() - start)

  return 0
}

goっぽいっしょ。これが、C++のクラスではなくて、goっぽい形で実現してますけど、メモリの確保は、インターフェイスに1つテーブルがあって、型にIDが動的に振られて、IDの箇所に関数が保存されるような仕組みで動いて結構速いのです。

以上、goma言語の適当な紹介でした。

明日は、keenさんのMllexを使ってみる。あるいはlexユーザーに対するmllexの解説です。