Ccmmutty logo
Commutty IT
0 pv4 min read

等しいことが判定できなさそうで判定できる関数の実装

https://picsum.photos/seed/336a205a1a9646d1ad129033976f1062/1200/630
Eq y => (Integer -> Bool) -> y
という型の関数がEqのインスタンスになる、すなわち等号(==)で等しいかどうか判定できることを実装を通して見ていきたいと思います。
以下のコードブロックは下部の再生ボタン▶️を押すと実行できるようになっているので、是非自分で実行してみてこの不思議な挙動を体験してみてください。
まず Integer -> Bool という関数を扱うための便利な演算子を用意しておきます。
haskell
(#) :: Bool -> (Integer -> Bool) -> (Integer -> Bool)
x # a = \i -> if i == 0 then x else a (i-1)

-- ~~~~~~~~~~ Example ~~~~~~~~~~ --
ex1 :: Integer -> Bool
ex1 = True # const False

ex1 0
ex1 1
ex1 2
(#)Integer -> Bool を添え字を取って真偽値を返す無限リストだと思った時、先頭に値を追加する演算子と見做すことができます。コードを実行すると期待通りの挙動になっていることがわかるでしょう。
※関数の引数は Integer ですがこの記事を通して正の範囲の値しか与えられないこととします。つまり実質 Natural として扱います。ただ全ての関数を適切に修正すれば負の範囲も考慮した実装も可能でしょう。
次に中心的な役割を果たす3つの関数を実装していきます。
haskell
find :: ((Integer -> Bool) -> Bool) -> (Integer -> Bool)
find p =
  if forsome (\a -> p (False # a))
    then False # find (\a -> p (False # a))
    else True  # find (\a -> p (True  # a))

forsome :: ((Integer -> Bool) -> Bool) -> Bool
forsome p = p (find p)

forevery :: ((Integer -> Bool) -> Bool) -> Bool
forevery p = not $ forsome (not . p)

-- ~~~~~~~~~~ Example ~~~~~~~~~~ --
ex2 :: Integer -> Bool
ex2 = find (\a -> a 1 && a 3)

ex2 0
ex2 1
ex2 2
ex2 3
ex2 4
find は与えられた条件を満たす Integer -> Bool を1つ返す関数です。この関数は内部でforsomeを呼んでおり、forsomeも内部でfindを呼んでいるので相互再帰になっています。一見複雑ですが、挙動としてはInteger -> Boolの値を前から1つずつ仮置きで定めていき条件に合致するものが見つかったらそれを返すという挙動になっています。そのため述語である (Integer -> Bool) -> Bool という関数は有限時間で決定できるものでなくてはなりません。
findの挙動のもう一つの特徴として以下の例を見てみましょう。
haskell
ex3 :: Integer -> Bool
ex3 = find (const False)

ex3 0
ex3 1
ex3 2
この例ではfindに与える述語は常にFalseを返すようになっているため条件に合致する Integer -> Bool は存在しませんが、それでも find は何らかの値を返します。forsome関数は述語に合致する Integer -> Bool が存在するかどうかを判定する関数ですが、このような find の挙動のため find が値を返したとしてももう一度それが述語に適合するものかどうかを調べているのです。foreveryは全ての Integer -> Bool が与えられた述語を満たすかどうかを調べる関数で、これはドモルガンの法則を用いて forsome を利用して実装されています。
これらの関数を利用していよいよ冒頭に挙げた関数のEqインスタンスを定義してみましょう。
haskell
{-# LANGUAGE FlexibleInstances #-}

instance Eq y => Eq ((Integer -> Bool) -> y) where
  f == g = forevery (\a -> f a == g a)

-- ~~~~~~~~~~ Example ~~~~~~~~~~ --
ex4 :: (Integer -> Bool) -> Bool
ex4 a = a 1 && a 2

ex5 :: (Integer -> Bool) -> Bool
ex5 a = not (not (a 1) || not (a 2))

ex4 == ex5

Discussion

コメントにはログインが必要です。