依存型の表現力と逆問題

Idrisみたいに、函数プログラミングを前提にしている言語には函数を合成する演算が標準で用意されているよね。

(.) : (b -> c) -> (a -> b) -> a -> c

この演算子を使うと、函数を合成してくれる。函数の合成を使えば、プログラムを変数を使わないで書くことができる。

整数を文字列にする : Integer -> String
整数を文字列にする = show

最初の文字を得る : String -> Char
最初の文字を得る = strHead

整数を文字列にして最初の文字を得る : Integer -> Char
整数を文字列にして最初の文字を得る = 最初の文字を得る . 整数を文字列にする

Prologよりも簡単だね。

でも、プログラミングでは、引数を複数持つ函数を使うことはよくあることだ。そして、函数プログラミングを前提にしている言語では、そういう函数は普通カリー化された状態で定義されている。

整数を足し合わせる : Integer -> Integer -> Integer
整数を足し合わせる = (+)

これをくっつけたい。するとどうなるか。

整数を足し合わせて文字列にして最初の文字を得る : Integer -> Integer -> Char
整数を足し合わせて文字列にして最初の文字を得る
    = 最初の文字を得る . 整数を文字列にする . 整数を足し合わせる

これは動かない! コンパイルしようとすると説教される。

Moji.idr:17:Can't unify Integer -> Integer -> Integer with Integer -> Integer

Specifically:
	Can't unify Integer -> Integer with Integer

本当に欲しかった演算はこんなのだ。

(>>>) : function a b -> (b -> c) -> function a c

ここで、functionは次のように定義してある。

function : List Type -> Type -> Type
function [] u = u
function (t :: ts) u = t -> function ts u

最初の引数は「引数の型のリスト」で、2番目の引数は「返り値の型」。つまり、 function は、引数の数を限定しない、一般的な函数を表現している。

この演算 (>>>) は実際に定義することができる。

infixl 1 >>>

(>>>) : function a b -> (b -> c) -> function a c
(>>>) {a = Nil} f g = g f
(>>>) {a = t :: ts} f g = \x => f x >>> g

じゃあ、これを使ってプログラムを書いてみよう。

import Function

整数を文字列にする : Integer -> String
整数を文字列にする = show

最初の文字を得る : String -> Char
最初の文字を得る = strHead

整数を文字列にして最初の文字を得る : Integer -> Char
整数を文字列にして最初の文字を得る = 整数を文字列にする >>> 最初の文字を得る

整数を足し合わせる : Integer -> Integer -> Integer
整数を足し合わせる = (+)

整数を足し合わせて文字列にして最初の文字を得る : Integer -> Integer -> Char
整数を足し合わせて文字列にして最初の文字を得る
    = 整数を足し合わせる >>> 整数を文字列にする >>> 最初の文字を得る

しかし、残念な結果が返ってくる。

Moji.idr:10:Can't unify Integer -> String with function a String

Specifically:
	Can't unify Integer -> String with function a String
Moji.idr:17:Can't unify Integer -> Integer -> Integer with function a Integer

Specifically:
	Can't unify Integer -> Integer -> Integer with function a Integer

エラーメッセージは Integer -> String といった型を function a String と unify できなかったということで、つまり a が自動で求められなかったわけだ。

暗黙の引数 a を与えれば、一応動作するようになる。動作するんだけど、コレジャナイ感が強い。

整数を文字列にして最初の文字を得る : Integer -> Char
整数を文字列にして最初の文字を得る
    = (>>>) {a = [Integer]} 整数を文字列にする 最初の文字を得る

整数を足し合わせて文字列にして最初の文字を得る : Integer -> Integer -> Char
整数を足し合わせて文字列にして最初の文字を得る
    = (>>>) {a = [Integer, Integer]}
      ((>>>) {a = [Integer, Integer]} 整数を足し合わせる 整数を文字列にする)
      最初の文字を得る

思えば、Prologはこの逆問題を解くことができる。Prologだと、functionの定義はこうなる。

function([], U, U).
function([T|TS], U, fn(T, X)) :- function(TS, U, X).

すると、次のようにして A を求められる。

?- function(A, string, fn(integer, string)).
A = [integer] ;
false.

?- function(A, string, fn(integer, fn(integer, string))).
A = [integer, integer] ;
false.

Prologの場合は停止しないプログラムも普通に書くことができるという問題があるのだけれども、何らかの改良を加えれば、このような推論は自動で行うことができるような気もする。