言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella
トップ > 言語 > salmacis: パターンマッチの意味(失敗)

salmacis: パターンマッチの意味(失敗)

言語

パターンマッチの意味について考えている。簡単なパターンマッチの例としては、

(x, y) = (1, 2)

のように書くと、x に 1 が y に 2 が束縛されるというもの。Scala や F# やHaskell などの最近の言語ではパターンマッチを一般化して、データ構造のみならずどのような関数を使ってもパターンマッチが出来る。たとえば Haskell では、

$ ghci
Prelude> :set -XViewPatterns
Prelude> let half n = n / 2
Prelude> let (half -> n) = 10 in n
5.0

のように変数 n に束縛する前に関数を適用出来る。この機能はカプセル化されたオブジェクトのパターンマッチに必須の機能だ。

さて、ふとこのパターンマッチを出来るだけ一般的に実装しようと思って困ってしまった。というのも、最初の (x, y) = (1, 2) では x = car (1, 2), y = cdr (1, 2) のように分解すれば良いのだろうけど、そもそも car (ペアの最初の要素) や cdr (二番目の要素) の実装にパターンマッチが使われているはずなのでこれではどうどう巡りになってしまう。

いつもの私ならここは割り切って出来る所から実装してしまうが、これは勉強なので少し考える。だいたいデータ構造は関数の特殊例なので、まず一般的な関数のパターンマッチを先に考えないといけない。データ構造が関数であるとはどういう事かというと、(1, 2) のようなペアを作る関数 cons と、car、cdr は次のように書く事が出来る。



cons = λx.λy.λf.f x y

car = λf.f(λx.λy.x)

cdr = λf.f(λx.λy.y)

さて、ここで思ったのは、パターンマッチのためには cons の逆関数 cons-1 を考えれば良いという事だ。別の言い方をすると、cons-1 (cons A) = A となるような関数を見つければ良い。しばらく考えてこういうのを思い付いた。



λx.x x (λy.λz.y)

なんか美しくないが、こんな風に動く。



cons-1 (cons A)

   = cons A (cons A) (λy.λz.y)

   = (λy.λf.f A y) (λy.λf.f A y) (λy.λz.y)

   = (λf.f A (λy.λi0.i0 A y)) (λy.λz.y)

   = (λy.λz.y) A (λy.λf.f A y)

   = (λz.A) (λy.λf.f A y)

   = A

しかし、本当にやりたいのは



cons (cons-1 (cons A B)) = cons A B

となるような cons-1 を見つける事だ。残念ながらこれは上手く行かなかった。



cons-1 (cons A B)

   = cons A B (cons A B) (λy.λz.y)

   = (λy.λf.f A y) B ((λy.λf.f A y) B) (λy.λz.y)

   = (λf.f A B) (λf.f A B) (λy.λz.y)

   = (λf.f A B) A B (λy.λz.y)

   = A A B B (λy.λz.y)

もしかして、ラムダ計算では無理じゃ無いかと思った。というのも、cons に二つ引数を渡したつもりになれる関数が必要という事だからだ。もしかしては forth のようなスタック言語(という事はコンビネータ?)多値を使ったら出来るかも知れないけど、詰まったのでここまでにしておく。

ちなみに、ラムダ計算には Lambda Calculator http://ozark.hendrix.edu/~burch/proj/lambda/ を使った。これのウェブ版があったら便利なのにな。