kiyoka.2013_10_03 RSSPLAIN

Related pages: !kiyoka.blog.list !kiyoka.blog.2013_10
55555555555555555555555555555555555555545545325
5

[Nendo] 副作用の無いコードの静的解析について(2)

5

前回の続き。( 前回の記事は、右上の窓から同じタイトルで検索してね )

5

 

5

Nendoにおける型付けについて

5
 4274069117  型システム入門 -プログラミング言語と型の理論-: Benjamin C. Pierce
5

によれば、静的解析をするということは、定義した評価規則と型付規則に従って評価をすることで全ての項を型付けできる。

5

Nendoに応用し、最低限その関数が「副作用」の無い関数かを検査できるようにしたい。

5

 

5

(1)ある関数が副作用の無い関数で構築されている場合は、もちろん副作用が無いといえる。

5

(2)さらには、関数内の束縛関数は破壊したとしても自由変数を破壊しないのであれば、それは副作用の無い関数といってよい。

5

 

5

(1)は自動的に判定することができそうであるが、(2)は人間が判断すればできるのではないか。

5

そうすれば、現実的なレベルの仕様になるのではないかと考えた。

5

 

5

型注釈について

5

Nendoでは上記のような基準から、「副作用無し」と「副作用有り」というどちらかの型で型付けする案を考えた。

5

プリミティブな関数に型を付与し、そこからブートストラップで全てのユーザー定義関数に型を付けていこうと考えている。

5

プリミティブな関数には副作用がある/なしを注釈する。 (型注釈用には :[コロン] が有力。 Typed Scheme: Scheme with Static TypesEXT を参考にした)

5
+ の場合
5
(: +   Pure)
5

 

5
car と cdr
5
(: car Pure)
5
(: cdr Pure)
5

 

5
set! と reverse!
5
(: set! Unpure)
5
(: reverse! Unpure)  ;; srfi-1
5

 

5

自動型付け

5

上記の型注釈が付いた関数を使って、関数を構築すると自動的に型が付与される。

5

少なくとも、Pureな関数だけが使用された関数はPureであり、それ以外は全てUnpureと判定すればよい。

5

 

5
(define (inc1 x)
5
  (+ x 1))
5
 => pureな関数
5

 

5
(define (fast-reverse! lst)
5
  (reverse! lst))
4
 => unpureな関数
5

 

5

感想

4

TaPLを読んでいるわりには、上記の理論を証明も何もしておらず直感でしか語っていないが、多分いけると思う。

5

 

3

COMMENTshiro

「定数でないグローバル変数を参照していない」という条件は必要じゃありませんか?

2

COMMENTkiyoka

おっと、グローバル変数がありますね。あとグローバル変数の一部だと思いますが環境変数もですね。

STDINとかSTDOUTとかは副作用の代表格ですね。

5

...comment disabled...