/mrsekut-p/Sort済みであることを型で示す

generated at 2/21/2025, 7:26:07 PM
Sort済みであることを型で示す

ここに、sortされたリスト同士をmergeする関数がある
hsmergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
mergeBy comp = go
  where
  go [] ys'          = ys'
  go xs' []          = xs'
  go (x:xs') (y:ys') = case comp x y of
    GT -> y : go (x:xs') ys'
    _  -> x : go xs' (y:ys')
第1引数に比較関数 comp 
これを引数に取ることでASC/DESCなどを利用者が決められる
第2,3引数に、同じ comp でsort済みのリスト xs ,  ys を取る
 xs と ys はsort済みであることが要請される
しかし、それは型に現れていない、利用者には伝わらない
こんな感じで使う
hsmain :: IO ()
main = do
  let xs = [1..5]
      ys = reverse [1..5]
      gt = comparing Down
  print (mergeBy' gt xs ys)		-- [5,4,3,2,1,2,3,4,5,1]
この例では ys が正しくsortされていないので、結果が期待しないものになってしまった


改善案1: 返り値を Maybe にする
hsmergeBy' :: (a -> a -> Ordering) -> [a] -> [a] -> Maybe [a]
mergeBy' comp xs ys
  | all (isSorted comp) [xs,ys] = Just $ mergeBy comp xs ys
  | otherwise                   = Nothing

isSorted :: (a -> a -> Ordering) -> [a] -> Bool
isSorted = undefined
第2,3引数が正しくsortされている場合は計算し、そうでない場合は Nothing を返す
確認するためのオーバーヘッドが生じる
「引数はsort済みのものが必要」ということを知っている利用者にとっては、いちいちMaybeのhandlingが必要になるので面倒



改善案2: 引数の型をsort済みリストにする
hsnewtype SortedList a = SortedList [a] deriving (Eq, Ord)
これは mergeBy の改善としては良くないな
 comp と SortedList が同じsortであることを保証していないので
hsnewtype SortedList a = SortedList [a] deriving (Eq, Ord)

mergeBy' :: (forall b. b -> b -> Ordering) -> SortedList a -> SortedList a -> SortedList a
mergeBy' comp xs ys = go (fromSortedList xs) (fromSortedList ys)
  where
  go :: [a] -> [a] -> SortedList a
  go [] ys'          = toSortedList ys'
  go xs' []          = toSortedList xs'
  go (x:xs') (y:ys') = case comp x y of
    GT -> insert y (go (x:xs') ys')
    _  -> insert x (go xs' (y:ys'))

singleton :: a -> SortedList a
insert x = mappend (singleton x)
fromSortedList :: SortedList a -> [a]
toSortedList :: [a] -> SortedList a



改善案3: Ghosts of Departed Proofsを使う
hssortBy :: ((a -> a -> Ordering) ~~ comp)
       -> [a]
       -> SortedBy comp [a]
sortBy comp xs = coerce (L.sortBy (the comp) xs)


mergeBy' :: ((a -> a -> Ordering) ~~ comp)
        -> SortedBy comp [a]
        -> SortedBy comp [a]
        -> SortedBy comp [a]
mergeBy' comp xs ys =
        coerce (mergeBy (the comp) (the xs) (the ys))

main :: IO ()
main = do
  let xs = [1..5]
      ys = reverse [1..5]
  name (comparing Down) $ \gt -> do
    let xs' = sortBy gt xs
        ys' = sortBy gt ys
    print (the (mergeBy' gt xs' ys'))
型安全
元のmergeByを使い回せる
仕様を正しく表現している
利用するコードが、元のもの比べてそこまで煩雑になっていない


参考
『Ghosts of Departed Proofs』 Section 2 Case Study 1: Sorted Lists