Reasoned Schemer (109) conda

なんだか/oで完結したみたいな気分になってましたが
ここで少し流れが変わってconda、conduが登場
ここらへん、“The Second Commandment”が何を言っているのかよくわからなかった記憶
ひさしぶりに処理系の中身と関連付けながら見ていく
こんどはわかるかな

condaの定義

(define-syntax conda
  (syntax-rules ()
    ((conda (g0 g ...)) (conj g0 g ...))
    ((conda (g0 g ...) ln ...)
     (ifte g0 (conj g ...) (conda ln ...)))))

condaのそれぞれの節の最初のgoalを条件にしてifteに展開していく

ifteの定義

(define (ifte g1 g2 g3)
  (lambda (s)
    (let loop ((s-inf (g1 s)))
      (cond
        ((null? s-inf) (g3 s))
        ((pair? s-inf)
         (append-map-inf g2 s-inf))
        (else (lambda () (loop (s-inf))))))))

questionが失敗だったら残りのconda節を評価
questionが成功だったらその結果をもってanswerをappend-map-infする
append-map-infするというのはconj2するということと同じ
answerもconjされてるから結果的には対象となるconda節のgoalをすべてconjすることになる
そして残りのconda節は無視される
questionがsuspensionだったら評価してもう一度

not-pastao

(defrel (not-pastao x)
  (conda ((== 'pasta x) fail)
         (succeed succeed)))

からの

> (run* x (conda ((not-pastao x) fail)
                 ((== 'spaghetti x) succeed)))
'(spaghetti)

まずnot-pastaoの中の(== 'pasta x)が成功
成功したのでいったんx == 'pastaとなるけど
けっきょくnot-pastaoとしてはfailするのでこの束縛は上位には伝わらず
xはfreshなまま
でx == 'spaghettiで成功

これはこれでいいのか？
x == 'spaghettiなら(not-pastao x)が成功してconda的にはそこでfailするはず、とも言えそうな

続いて

> (run* x (== 'spaghetti x)
          (conda ((not-pastao x) fail)
                 ((== 'spaghetti x) succeed)))
'()

x == 'spaghettiなら(not-pastao x)が成功してconda的にはそこでfailする、
と見れば普通
さっきのがNGでこっちはOKってことなの？

(),
because (not-pastao x) succeeds, which shows the risks involved when using conda. We can’t allow a fresh variable to become associated as part of a conda question.

()です。
なぜならば、(not-pastao x)が成功するからです。これは、condaを使うときに巻き込まれるリスクを示しています。我々は、condaのquestionの一部としてfreshな変数をassociateさせてはなりません。

これがつまりThe Second Commandmentの言ってることなんだけど
最初に読んだときはここで、さっきのはOKだけど今度のはダメ、って書いてあると思ったんだよな
ここが勘違いだった？
xがfreshだと、not-pastaoの(== 'pasta x)が成功してx == 'pastaにしてしまうからダメと言っているのか
freshだと==が成功してしまうから比較にはならないと
そういうことだなきっと
値が決まってから判定するような使い方するってことね