「モナドの理解」というタイトルのワドラーの論文からの次の定義を理解するのを手伝ってくれる人はいますか? (抜粋はセクション 3.2/9 ページ、つまり「厳密性モナド」サブセクションからのものです。)
遅延関数型プログラムでは、評価の順序を制御する必要がある場合があります。これは通常、次のように定義された計算可能な関数strictで実現されます。
厳密な f x = x ≠ ⊥ の場合、f xでなければ ⊥.
操作上、厳密な f xは、最初にxを弱頭部正規形 (WHNF) に減らし、次にアプリケーションf xを減らすことによって減らされます。または、 xとf xを並列に減らすことは安全ですが、 xが WHNF になるまで結果へのアクセスを許可しません。
この論文では、2 本の垂直線で構成される記号の使用をまだ確認していないため (それが何と呼ばれているかはわかりません)、どこからともなく出てきます。
Wadler が「遅延プログラムの評価を制御するために [厳密な] 内包表記を使用する」と述べていることを考えると、理解することは非常に重要な概念のように思えます。