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

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

型システム入門 －プログラミング言語と型の理論－

著者: Benjamin C. Pierce

Amazonで見る

によれば、静的解析をするということは、定義した評価規則と型付規則に従って評価をすることで全ての項を型付けできる。 [Nendo]に応用し、最低限その関数が「副作用」の無い関数かを検査できるようにしたい。

(1)ある関数が副作用の無い関数で構築されている場合は、もちろん副作用が無いといえる。 (2)さらには、関数内の束縛関数は破壊したとしても自由変数を破壊しないのであれば、それは副作用の無い関数といってよい。

(1)は自動的に判定することができそうであるが、(2)は人間が判断すればできるのではないか。 そうすれば、現実的なレベルの仕様になるのではないかと考えた。

型注釈について

[Nendo]では上記のような基準から、「副作用無し」と「副作用有り」というどちらかの型で型付けする案を考えた。 プリミティブな関数に型を付与し、そこからブートストラップで全てのユーザー定義関数に型を付けていこうと考えている。 プリミティブな関数には副作用がある/なしを注釈する。 (型注釈用には :コロン が有力。 Typed Scheme: Scheme with Static Types を参考にした)

• • の場合

    (: +   Pure)
    

• car と cdr

  (: car Pure)
  (: cdr Pure)
  

• set! と reverse!

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

自動型付け

上記の型注釈が付いた関数を使って、関数を構築すると自動的に型が付与される。 少なくとも、Pureな関数だけが使用された関数はPureであり、それ以外は全てUnpureと判定すればよい。

(define (inc1 x)
  (+ x 1))

=> pureな関数

(define (fast-reverse! lst)
  (reverse! lst))

=> unpureな関数

感想

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

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

コメント by kiyoka:
おっと、グローバル変数がありますね。あとグローバル変数の一部だと思いますが環境変数もですね。 STDINとかSTDOUTとかは副作用の代表格ですね。

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