9

私は最近Haskellについてたくさん読んでいます、そしてそれが純粋に関数型言語であることから得られる利点。（私はLispのモナドについて議論することに興味がありません）（少なくとも論理的に）副作用のある関数を可能な限り分離することは私にとって理にかなっています。私はsetf他の破壊的な関数をたくさん使ってきました、そして私はLispと（ほとんどの）その派生物でそれらの必要性を認識しています。

どうぞ：

  1. (declare pure)コンパイラの最適化に役立つ可能性があるものはありますか？それとも、すでに知っているので、これは論点ですか？
  2. 宣言は、関数やプログラム、または少なくとも純粋であると宣言されたサブセットを証明するのに役立ちますか？それとも、プログラマー、コンパイラー、および証明者にはすでに明らかであるため、これも不要なものですか？
  3. 他に何もないとしても、コンパイラーがこの宣言で関数の純粋さを強制し、Lispプログラムの可読性/保守性を高めることはプログラマーにとって有用でしょうか？
  4. これは意味がありますか？それとも私は今考えることすらできないほど疲れていますか？

ここで洞察をいただければ幸いです。コンパイラの実装または証明可能性に関する情報は大歓迎です。

編集

明確にするために、私はこの質問をCommonLispに限定するつもりはありませんでした。それは明らかに（私が思うに）特定の派生言語には当てはまりませんが、他のLispのいくつかの機能がこの種の機能をサポートする（またはサポートしない）傾向があるかどうかも興味があります。

4

3 に答える 3

7

2つの答えがありますが、どちらも実際の問題には触れていません。

まず、はい、関数が純粋であることを知っておくのは明らかに良いことです。それを知りたいコンパイラレベルのものと、ユーザーレベルのものがたくさんあります。lisp言語は非常に柔軟であるため、少しひねることができます。コンパイラにもっと頑張ってもらうように求める「純粋な」宣言の代わりに、宣言で定義内のコードを制限するだけです。このようにして、関数が純粋であることを保証できます。

追加のサポート機能を使用してそれを行うこともできます-私はjohanbevの答えに対して行ったコメントでそれらのうちの2つに言及しました：不変のバインディングと不変のデータ構造の概念を追加します。Common Lispでは、これらは非常に問題があり、特に不変のバインディングであることがわかっています（CLは、コードを「サイドエフェクト」して所定の位置にロードするため）。しかし、そのような機能は物事を単純化するのに役立ち、考えられないことではありません（たとえば、不変のペアやその他のデータ構造を持ち、不変のバインディングを持つRacket実装を参照してください。

しかし、本当の問題は、そのような制限された機能で何ができるかということです。非常に単純な見た目の問題でさえ、問題がはびこっています。（これにはSchemeのような構文を使用しています。）

(define-pure (foo x)
  (cons (+ x 1) (bar)))

この関数が本当に純粋であると言うのは簡単なようですが、何もしません。また、define-pure本文を制限し、純粋なコードのみを許可することは、この場合は正常に機能し、この定義を許可するようです。

ここで、問題から始めます。

  1. を呼び出しconsているので、純粋であることがわかっていることも前提としています。さらに、前述したように、それが何であるかに依存する必要があるため、バインディングは不変consであると想定します。cons既知のビルトインなので簡単です。barもちろん、同じことをしてください。

  2. ただし、副作用があります（Racketの不変のペアについて話している場合でも）。新しいペアがcons 割り当てられます。これは些細で無視できる点のように思えますが、たとえば、そのようなものを純粋関数に表示することを許可すると、それらを自動メモ化することはできなくなります。問題は、誰かが新しいペア（他の既存のペアにはないfooペア）を返すすべての呼び出しに依存する可能性があることです。eqうまくするには、純粋関数をさらに制限して、不変の値だけでなく、コンストラクターが常に新しい値を作成するとは限らない値（たとえば、allocateの代わりにhash-consを処理できる値）を処理する必要があるようです。

  3. しかし、そのコードは-を呼び出しますbar-したがって、同じ仮定をする必要はbarありません：それは不変のバインディングを持つ純粋関数として知られている必要があります。bar特に、は引数を受け取らないことに注意してください。その場合、コンパイラはbarそれが純粋関数であることを要求できるだけでなく、その情報を使用してその値を事前に計算することもできます。結局のところ、入力のない純粋関数は単純な値に減らすことができます。（ところで、Haskellには引数ゼロの関数がないことに注意してください。）

  4. そして、それは別の大きな問題をもたらします。1つの入力barの関数である場合はどうなりますか？その場合、エラーが発生し、いくつかの例外がスローされます...そしてそれはもはや純粋ではありません。例外は副作用です。ここで、他のすべてに加えてのアリティを知る必要があり、他の例外を回避する必要があります。さて、その入力はどうですか？それが数字でない場合はどうなりますか？それも例外をスローするので、それも避ける必要があります。これは、型システムが必要であることを意味します。barx

  5. これをに変更する(+ x 1)と(/ 1 x)、型システムが必要なだけでなく、0を区別するのに十分な洗練されたシステムが必要であることがわかります。

  6. あるいは、全体を再考して、例外をスローしない新しい純粋な算術演算を行うこともできますが、他のすべての制限により、言語が根本的に異なるため、家から遠く離れています。

  7. 最後に、PITAのままであるもう1つの副作用があります。の定義がである場合はどうなりbarます(define-pure (bar) (bar))か？上記のすべての制限に従って、それは確かに純粋です...しかし、発散は副作用の一形態であるため、これでさえコーシャではなくなります。（たとえば、コンパイラーにnullary関数を値に最適化させた場合、この例では、コンパイラー自体が無限ループに陥ります。）（そして、はい、Haskellはそれを処理しません、それはそれをしません問題は少ないです。）

于 2011-08-31T16:33:53.140 に答える
3

Lisp関数が与えられた場合、それが純粋であるかどうかを知ることは一般に決定不可能です。もちろん、必要条件と十分条件はコンパイル時にテストできます。（不純な操作がまったくない場合、関数は純粋である必要があります。不純な操作が無条件に実行される場合、関数は不純である必要があります。より複雑なケースでは、コンパイラは関数が純粋または不純であることを証明しようとします。 、ただし、すべての場合に成功するとは限りません。）

  1. ユーザーが関数に純粋として手動で注釈を付けることができる場合、コンパイラーは（a。）関数が純粋であることを証明するためにもっと一生懸命努力することができます。諦める前により多くの時間を費やすか、（b。）そうであると想定し、不純な関数（たとえば、結果のメモ化など）には正しくない最適化を追加します。したがって、そうです、注釈が正しいと想定される場合、関数に純粋な注釈を付けることはコンパイラーを助けることができます。

  2. 上記の「もっと頑張る」アイデアのようなヒューリスティックを除けば、注釈は証明者に情報を提供しないため、証明には役立ちません。（言い換えれば、証明者は、試行する前に注釈が常にそこにあると想定することができます。）ただし、純粋関数にその純粋性の証明を添付することは理にかなっています。

  3. コンパイラーは、（a。）コンパイル時に純粋関数が本当に純粋であるかどうかをチェックすることができますが、これは一般に決定不可能です。または（b。）実行時に純粋関数の副作用をキャッチし、それらをエラーとして報告するコードを追加します。 。（a。）は、単純なヒューリスティック（「不純な操作が無条件に実行されるなど）」で役立つ可能性があり、（b。）はデバッグに役立ちます。

  4. いいえ、それは理にかなっているようです。うまくいけば、この答えもそうです。

于 2011-08-31T10:55:55.953 に答える
1

通常の特典は、純度と参照透過性を想定できる場合に適用されます。ホットスポットを自動的にメモ化できます。計算を自動的に並列化できます。多くの競合状態に対処できます。また、変更できないことがわかっているデータとの構造共有を使用することもできます。たとえば、（準）プリミティブの「cons（）」は、cons-cons-セルをコピーする必要はありません。これらのセルは、別のコンスセルがそれを指していることによる影響を受けません。この例はやや明白ですが、コンパイラーは、より複雑な構造共有を理解する上で優れたパフォーマンスを発揮することがよくあります。

ただし、ラムダ（関数）が純粋であるか参照透過性があるかを実際に判断することは、CommonLispでは非常に注意が必要です。funcall（foo bar）は（symbol-function foo）を見ることから始まることを忘れないでください。したがって、この場合

(defun foo (bar)
  (cons 'zot bar))

foo（）は純粋です。

次のラムダも純粋です。

(defun quux ()
 (mapcar #'foo '(zong ding flop)))

ただし、後でfooを再定義できます。

(let ((accu -1))
 (defun foo (bar)
   (incf accu)))

quux（）への次の呼び出しはもはや純粋ではありません！古い純粋なfoo（）は、不純なラムダに再定義されました。うわぁ。この例は多少工夫されているかもしれませんが、たとえばletブロックを使用して、一部の関数を字句的に再定義することは珍しくありません。その場合、コンパイル時に何が起こるかを知ることはできません。

Common Lispは非常に動的なセマンティクスを持っているため、実際に制御フローとデータフローを事前に（たとえばコンパイル時に）決定できるようにすることは非常に困難であり、ほとんどの場合、完全に決定不可能です。これは、動的型システムを備えた言語の非常に典型的なものです。Lispには、静的型付けを使用する必要がある場合に使用できない一般的なイディオムがたくさんあります。非常に意味のある静的分析を実行しようとする試みを汚すのは、主にこれらです。短所や友人のようなプリミティブに対してそれを行うことができます。しかし、プリミティブ以外のものを含むラムダの場合、特に関数間の複雑な相互作用を調べる必要がある場合は、はるかに深い水域にいます。ラムダが純粋であるのは、それが呼び出すすべてのラムダも純粋である場合のみであることを忘れないでください。

私の頭のてっぺんに、いくつかの深いマクロ学で、再定義の問題を取り除くことが可能かもしれません。ある意味で、各ラムダは、lispイメージの状態全体を表すモナドである追加の引数を取得します（関数が実際に見るものに明らかに制限することができます）。しかし、このラムダが実際に純粋であることをコンパイラーに約束するという意味で、自分で純粋性を宣言できる方がおそらくより便利です。そうでない場合の結果は未定義であり、あらゆる種類の騒乱が続く可能性があります...

于 2011-08-31T11:30:40.150 に答える